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 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.

No comments :

Post a Comment