Sort a list of numbers on the λ-calculus

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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.