Sum of list elements and length of list in lambda calculus

Question

I am trying to make function for computing sum of list elements and length of list in lambda calculus.
Example of a list: a := [1, 2, 3] = λcn.c 1 (c 2 (c 3 n))
sum a should return 6 and len a should return 3.

I wrote recursive versions:

len = λl.if (empty l) 0 (plus 1 (len (tail l)))
sum = λl.if (empty l) 0 (plus (head l) (sum (tail l)))

where if, empty, plus, tail are other lamda functions.

Then I did some trick with fixed-point combinator:

len = λl.if (empty l) 0 (plus 1 (len (tail l))) 
len = λfl.if (empty l) 0 (plus 1 (f (tail l))) len
len = Y λfl.if (empty l) 0 (plus 1 (f (tail l)))

where Y = λf.(λx.f(x x))(λx.f(x x))
Just the same for sum. So now I have non-recursive versions. But I can't get beta normal form using beta reduction here.
I wonder if there is beta normal forms of these functions and how they look like.

Answer 1

These can be implemented much more easily given that a list is encoded by its own iterator:

a := [1, 2, 3] = λcn.c 1 (c 2 (c 3 n))

means that a list is a function of two arguments: one to use on cons nodes and one to use at the end on the nil constructor.

As a consequence you can implement length by saying:

• ignore the value stored in a cons node and return +1
• replace nil with 0

which translates to:

length := λl. l (λ_. plus 1) 0

which would expand to (at each line the expression in bold is being either unfolded or reduced):

length a
(λl. l (λ_. plus 1) 0) a
(λl. l (λ_. plus 1) 0) (λcn.c 1 (c 2 (c 3 n)))
(λcn. c 1 (c 2 (c 3 n))) (λ_. plus 1) 0
(λn. (λ_. plus 1) 1 ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))) 0
(λ_. plus 1) 1 ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))
(plus 1) ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))
(plus 1) ((plus 1) ((λ_. plus 1) 3 0))
(plus 1) ((plus 1) ((plus 1) 0))
(plus 1) ((plus 1) 1)
(plus 1) 2
= 3

Similarly, you can implement sum by saying:

• use + to combine the value stored in a cons and the result of evaluating the tail
• replace nil by 0

which translates to:

sum := λl. l plus 0

which would expand to

sum a
(λl. l plus 0) a
(λl. l plus 0) (λcn.c 1 (c 2 (c 3 n)))
(λcn. c 1 (c 2 (c 3 n))) plus 0
(λn. plus 1 (plus 2 (plus 3 n))) 0
plus 1 (plus 2 (plus 3 0))
plus 1 (plus 2 3)
plus 1 5
= 6