10
$\begingroup$

The following λ-term, here in normal form:

sort = (λabc.(a(λdefg.(f(d(λhij.(j(λkl.(k(λmn.(mhi))l))
       (h(λkl.l)i)))(λhi.(i(λjk.(bd(jhk)))(bd(h(λjk.(j
       (λlm.m)k))c)))))e))(λde.e)(λde.(d(λfg.g)e))c))

Implements a sorting algorithm for church-encoded lists. That is, the result of:

sort (λ c n . (c 3 (c 1 (c 2 n)))) β→ (λ c n . (c 1 (c 2 (c 3 n))))

Similarly,

sort_below = λabcd.a(λef.f(λghi.g(λj.h(λkl.kj(ikl)))(hi))e(λgh.h))
            (λe.d)(λe.b(λf.e(f(λghi.hg)(λgh.cfh))))

Also implements sorting for the same lists as above, except you must provide an additional argument with a limit for the numbers it will consider:

sort_below 4 [5,1,3,2,4] → [1,2,3]

I am trying to determine whether those terms are typeable on elementary affine logic. Since I don't know any EAL type-checker publicly available, this is proving a harder task than I expected. Is there a type for sort in elementary affine logic?

$\endgroup$
  • $\begingroup$ Does it have an "ordinary" type? What happens if you plug it into Haskell? $\endgroup$ – Andrej Bauer Aug 29 '15 at 12:51
  • 1
    $\begingroup$ I agree with Andrej, the terms are unreadable as such. What algorithms do they implement? Some integer sorting not based on comparison? What EAL-based typing system are you considering? The naive one (no subject reduction) or the one by Coppola, Dal Lago and Ronchi? Are they typable in System F, e.g. $sort:\mathsf{NatList}\to\mathsf{NatList}$, where $\mathsf{NatList}:=\forall X.(\mathsf{Nat}\to X\to X)\to X\to X$? If not, then there is no hope they are typable in any EAL-based system. $\endgroup$ – Damiano Mazza Aug 29 '15 at 14:11
  • 1
    $\begingroup$ Yes, this is because there is a forgetful functor $(\cdot)^-$ from EAL to System F (or to simple types, if you do not use polymorphism) such that if $t:A$ in EAL, then $t^-:A^-$ in System F. The fact that your simplified evaluator works is not inconsistent with this: what makes Lamping's algorithm work without brackets and croissants is a stratification property of terms, which is purely structural and independent of types: there are untypable terms (in System F, EAL, Haskell or whatever) which are stratified. I guess your term must fall in this class. $\endgroup$ – Damiano Mazza Aug 29 '15 at 14:55
  • 1
    $\begingroup$ Maybe these comments can be turned into an answer? $\endgroup$ – Andrej Bauer Aug 31 '15 at 10:18
  • 1
    $\begingroup$ While reading through questions. :-) $\endgroup$ – Tayfun Pay Jul 4 '17 at 18:57
3
$\begingroup$

I think sort, as presented there, isn't typeable on EAL. I can't prove that, but it doesn't work on Lamping's Abstract Algorithm without the oracle. Moreover, while the term is somewhat clever and brief, it uses very wacky strategies that are not EAL-friendly.

But behind this question there is a more interesting one: "can a nat-sorting function be implemented in EAL"? That was a very hard question back then, but now it looks pretty trivial. Yes, of course. There are many simpler ways to do it. For an example, one can just fill a Scott-encoded NatSet with Church-encoded Nats, and then convert it to a list. Here is a complete demonstration:

-- sort_example.mel
-- Sorting a list of Church-encoded numbers on the untyped lambda calculus
-- with terms that can be executed by Lamping's Abstract Algorithm without
-- using the Oracle. Test by calling `mel sort_example.mel`, using Caramel,
-- from https://github.com/maiavictor/caramel

-- Constructors for Church-encoded Lists 
-- Haskell: `data List = Cons a (List a) | Nil`
Cons head tail = (cons nil -> (cons head (tail cons nil)))
Nil            = (cons nil -> nil)

-- Constructors for Church-encoded Nats
-- Haskell: `data Nat = Succ Nat | Zero`
Succ pred = (succ zero -> (succ (pred succ zero)))
Zero      = (succ zero -> zero)

---- Constructors for Scott-encoded NatMaps
---- Those work like lists, where `Yep` constructors mean
---- there is a number on that index, `Nah` constructors
---- mean there isn't, and `End` ends the list.
---- Haskell: `data NatMap = Yep NatMap | Nah NatMap | End`
Yep natMap = (yep nah end -> (yep natMap))
Nah natMap = (yep nah end -> (nah natMap))
End        = (yep nah end -> end)

---- insert :: Nat (Church) -> NatMap (Scott) -> NatMap (Scott)
---- Inserts a Church-encoded Nat into a Scott-encoded NatMap.
insert nat natMap    = (nat succ zero natMap)
    succ pred natMap = (natMap yep? nah? end?)
        yep? natMap  = (Yep (pred natMap))
        nah? natMap  = (Nah (pred natMap))
        end?         = (Nah (pred natMap))
    zero natMap      = (natMap Yep Yep (Yep End))

---- toList :: NatMap (Scott) -> List Nat (Church)
---- Converts a Scott-Encoded NatMap to a Church-encoded List
toList natMap        = (go go natMap 0)
    go go natMap nat = (natMap yep? nah? end?)
        yep? natMap  = (Cons nat (go go natMap (Succ nat)))
        nah? natMap  = (go go natMap (Succ nat))
        end?         = Nil

---- sort :: List Nat (Church) -> List Nat (Church)
---- Sorts a Church-encoded list of Nats in ascending order.
sort nats = (toList (nats insert End))

-- Test
main = (sort [1,4,5,2,3])

Here is the bruijn-indexed normal form of a slightly altered version of the sort above, which must receive (x -> (x x)) as the first argument in order to work (otherwise it doesn't have a normal form):

λλ(((1 λλλ(((1 λλλ((1 3) (((((5 5) 2) λλ(1 ((5 1) 0))) 1) 0))) 
λ(((3 3) 0) λλ(1 ((3 1) 0)))) λλ0)) ((0 λλ(((1 λλ(((0 λλλλ(2 (
5 3))) λλλλ(1 (5 3))) λλλ(1 (4 3)))) λ(((0 λλλλ(2 3)) λλλλ(2 3
)) λλλ(2 λλλ0))) 0)) λλλ0)) λλ0)

Pretty simple in retrospect.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.