Sort a list of numbers on the λ-calculus

8

1

Write a term on the pure untyped lambda calculus that, when applied to a church-encoded list of numbers, returns it with its numbers sorted in ascending or descending order. Church lists and numbers must be encoded as folds for their usual ADTs:

-- Usual ADTs for Lists and Nats (in Haskell, for example)
data List a = Cons a (List a) | Nil
data Nat a  = Succ (Nat a) | Zero

-- Their respective folds are the λ-calculus representation used on this challenge
church_list = (λ c n . (c ... (c ... (c ... n))))
church_num  = (λ succ zero . (succ (succ (succ ... zero))))

Example input:

(λ cons nil .
    (cons (λ f x . (f x))                         -- 1
    (cons (λ f x . (f (f (f (f (f (f (f x)))))))) -- 7
    (cons (λ f x . (f (f x)))                     -- 2
    (cons (λ f x . (f (f (f x))))                 -- 3
    nil)))))

Example output:

(λ cons nil . 
    (cons (λ f x . (f x))                         -- 1
    (cons (λ f x . (f (f x)))                     -- 2
    (cons (λ f x . (f (f (f x))))                 -- 3
    (cons (λ f x . (f (f (f (f (f (f (f x)))))))) -- 7
    nil)))))

The score of a submission will be calculated as follows:

score(x)    = 1
score(λx.t) = score(t) + 1
score(t s)  = score(t) + score(s) + 1

Lowest score wins.

MaiaVictor

Posted 2015-08-24T05:40:55.840

Reputation: 349

7The linked page provides three different Church encodings for lists, and there's nothing to stop it from changing in the future. In order that the question be unambiguous, you will need to define the particular encoding you have in mind explicitly in the question. (It would also be advisable to define the encoding of the numbers). – Peter Taylor – 2015-08-24T15:19:33.007

1ascending or descending order -- why do we get to pick? – Lynn – 2015-08-24T17:02:52.057

I just didn't find a reason to limit it. Why not? – MaiaVictor – 2015-08-24T17:07:29.317

Answers

3

I've managed to beat my own mark:

sort = λ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))))

There is a caveat, though - this term must receive an additional argument with the maximum size of naturals that are considered. For example, sort 4 [1,7,3,6,5] will return [1,3], ignoring anything above or equal 4. Of course, you could just give infinity (i.e., the Y-combinator):

sort = λbcd.(λfx.f(x x))(λfx.f(x x))(λef.f(λghi.g(λj.h(λkl.kj(ikl)))
       (hi))e(λgh.h))(λe.d)(λe.b(λf.e(f(λghi.hg)(λgh.cfh))))

And it would sort any list of natural numbers, but this term obviously doesn't have a normal form anymore.

MaiaVictor

Posted 2015-08-24T05:40:55.840

Reputation: 349

1

Here's an implementation of an insertion sort:

let nil =       \f x.x in
let cons = \h t.\f x.f h (t f x) in
let 0 =       \f x.x in
let succ = \n.\f x.f (n f x) in
let None =    \a b.b in
let Some = \x.\a b.a x in
let pred = \n.n (\opt.opt (\m.Some(succ m)) (Some 0)) None in
let optpred = \opt.opt pred None in
let - = \m n.n optpred (Some m) in
let < = \m n.\trueval falseval.- m n (\diff.falseval) trueval in
let pair = \x y.\f.f x y in
let snd = \p.p (\x y.y) in
let insert = \n l.snd (l (\h recpair.recpair (\rawtail insertedtail.
  let rawlist = cons h rawtail in
    pair rawlist (< h n (cons h insertedtail) (cons n rawlist))))
  (pair nil (cons n nil))) in
\l.l insert nil

Here, pred n returns an element of option nat: pred 0 is None whereas pred (n+1) is Some n. Then, - m n returns an element of option nat which is Some (m-n) if m>=n or None if m<n; and < m n returns a boolean. Finally, insert uses an internal function returning a pair where f l = (l, insert n l) (a fairly typical method to get the tail of the list to get passed to the recursion along with the recursive value).

Now, some notes for future golfing work: actually nil, 0, None happen to be the same function formally (and it also appears in snd). Then, I would certainly consider doing beta reductions on the let statements (which is of course the usual syntactic sugar where let a = x in y means (\a.y)x and thus has score score(x) + score(y) + 2) to see in which cases doing so would reduce the score - which it most definitely would for the bindings that are only used once.

Then would come trickier things: for example, I just noticed that formally pred = pair (pair (\m.Some(succ m)) (Some 0)) None, optpred = pair pred None, - = \m.pair optpred (Some m), the sort function definition amounts to pair insert nil, etc. which could reduce the score slightly.

Daniel Schepler

Posted 2015-08-24T05:40:55.840

Reputation: 1 001

Please calculate your score and state it in the answer – Nathaniel – 2019-06-10T13:26:46.383

1

121 characters / score 91

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

It is in normal form and could be made shorter by lifting common subexpressions.

MaiaVictor

Posted 2015-08-24T05:40:55.840

Reputation: 349