λ-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.n(λgh.h(gf))(λu.x)(λu.u)
ISZERO = λn.n(λx.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 similar
typedef 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.