## Tuesday, December 4, 2007

### λ-fun in metaC++: recursion

Let's implement a recursive numeric function in our C++ embedding of λ-calculus. Before delving into the specific problems of recursion, we remember the standard way of defining basic logical predicates in λ-calculus, as usual courtesy of Alonzo Church:
TRUE = λxy.x
FALSE = λxy.y
AND
= λxpq.p q FALSE
OR = λpq.p TRUE q
NOT = λp.p FALSE TRUE
IFTHENELSE
= λpfg.pfg
whose translation to metaC++ is straightforward. We will also need a predecessor function (we define the succesor in prior entries) and a predicate for testing whether a number is zero (where numbers have been defined via Church numerals):
PRED = λnfx.ngh.h(gf))(λu.x)(λu.u)
ISZERO = λn.nx.FALSE)TRUE
So equipped, we could try to "define" the factorial function as follows:
FAC = λn.IFTHENELSE (ISZERO n) 1 (MULT n (FAC(PRED n)))
which is not a true definition as FAC is both the definiendum and part of the definiens. Such a recursive definition is typically emulated in λ-calculus by parameterizing the recursive call:
FACIMPL = λfn.IFTHENELSE (ISZERO n) 1 (MULT n (f(PRED n)))
and adding the folding part by means of some fixed-point operator FP:
FAC = FP FACIMPL
where FP has the property
FP FACIMPLβ FACIMPL(FP FACIMPL)
so that reducing FP FACIMPL one step "executes" FACIMPL once on the very same FP FACIMPL function:
FP FACIMPLβ
FACIMPL(FP FACIMPL) →β
FACIMPL(FACIMPL(FP FACIMPL)) →β ...
There are many (infinite, actually) universal fixed point operators, i.e. λ-terms that are a fixed-point operator of any arbitrary term. The most famous is the Y combinator:
Y = λf.(λx. f(xx))(λx. f(xx))
Proving that Y is a universal fixed-point operator is trivial:
λf.(λx. f(xx))(λx. f(xx)) →β λf.f((λx. f(xx))(λx. f(xx))) = λf.f(Yf)
At first sight, it looks like we can easily code Y in C++:
`template<typename F>struct YAUX;template<typename F,typename X>struct apply<YAUX<F>,X>:apply<F,typename apply<X,X>::type>{};struct Y;template<typename F>struct apply<Y,F>:apply<YAUX<F>,YAUX<F> >{};`
but we will obtain a compiler error as soon as we try to use this:
`// error 'type' not defined or something similartypedef apply<Y,I>::type type; `
What's happening? The compiler tries to instantiate `apply<YAUX<I>,YAUX<I> >`, which is self-referential because it derives from `apply<F,apply<``YAUX<I>``,``YAUX<I> ``>::type>`. In short, YI has an infinite β-reduction path, which is after all understandable as this is the raison d'être of a fixed-point operator.

The good news is that we can in fact implement recursive functions in our C++ embedding of λ-calculus without using fixed-point operators: Defining a term f translates to specializing `apply` for some contexts of use of the type `F`, and in defining this specialization we can freely use the type `F` itself, which opens up the possibility of recursion. The following is a definition of the factorial function:

`struct FAC;struct FACIF;template<typename N>struct apply<FACIF,N>{typedef ONE type;};struct FACELSE;template<typename N>struct apply<FACELSE,N>:apply2< MULT,N, typename apply<FAC,typename apply<PRED,N>::type>::type>{};template<typename N>struct apply<FAC,N>:apply< typename apply3<   IFTHENELSE,    typename apply<ISZERO,N>::type,    FACIF,    FACELSE >::type, N>{};`
where `FACIF` and `FACELSE` provide a level of indirection to avoid infinite β-reduction inside the expansion of `FAC`. In λ-calculus jargon, this trick corresponds to the so-called η-expansion of the original term.

A program with the full code for this entry is provided.