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.