Sort a list of numbers on the λ-calculus 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.
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.