Search code examples
lambdafunctional-programminglambda-calculus

non recursive lambda calculus factorial function


How to write a factorial function without use of recursion using lambda calculus? Meaning just the math notation not implementation in any particular programming language.


Solution

  • If by "without the use of recursion" you mean without general recursion and hence without fixpoints (or self applications), we can simply observe that the factorial function is primitive recursive (that is, iterative, in essence), and there is a very general and simple encoding of primitive recursion by means of iteration (provided by church numerals) and pairs. I will discuss the general case that is quite instructive. Let < M,N > be some encoding of pairs, and let fst and snd be the associated projections. For instance, you can define

    <M,N> = λz. z M N
    fst = λp. p (λxy.x)
    snd = λp. p (λxy.y)
    

    Suppose to have a primitive recursive definition (without parameters, for the sake of simplicity)

    f(0) = a
    f(x+1) = h(x,f(x))
    

    where a and h have been already defined.

    The general idea is to use an auxiliary function f', where

                           f'(x) = <x,f(x)>
    

    So, f'(0) = < 0, a>, and given the pair p = < x,f(x) > = f'(x), we build the next pair < x+1, f(x+1) > by computing the successor on the first component and applying h to the pair of arguments (that, taking advantage of our encoding of pairs, simply amounts to pass the continuation h as input to the pair p).

    Summing up,

    next = λp.< succ (fst p), p h>
    

    Finally, to compute f(n) we need to iterate n times the function next starting from < 0, a>, and then take the second component:

     f = λn. snd (n next <0,a>)