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.xwhose 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):

FALSE = λxy.y

AND = λxpq.p q FALSE

OR = λpq.p TRUE q

NOT = λp.p FALSE TRUE

IFTHENELSE = λpfg.pfg

PRED = λnfx.n(λgh.h(gf))(λu.x)(λu.u)So equipped, we could try to "define" the factorial function as follows:

ISZERO = λn.n(λx.FALSE)TRUE

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 FACIMPLwhere FP has the property

FP FACIMPL →so that reducing FP FACIMPL one step "executes" FACIMPL once on the very same FP FACIMPL function:_{β}FACIMPL(FP 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:_{β}

FACIMPL(FP FACIMPL) →_{β}

FACIMPL(FACIMPL(FP FACIMPL)) →_{β}...

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)) →At first sight, it looks like we can easily code Y in C++:_{β}λf.f((λx. f(xx))(λx. f(xx))) = λf.f(Yf)

`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