λ-fun in metaC++

Let's embed untyped lambda calculus into the metaprogramming sublanguage of C++. Such embedding consists of two components:

• Syntax: a representation for λ-terms.
• Semantics: a mechanism for β-reduction.

Though in our approach both aspects are inextricably intertwinned: lambda abstraction (the operation that goes from M to λx.M) and its associated β-reduction rule are described operationally rather than syntactically.

A λ-term is represented by one of the following:

• An unanalyzed C++ type,
• A type of the form apply<F,G> for some types F,G,

where the metafunction apply is defined as follows:

template<typename F,typename G>
struct apply{typedef apply type;};

(Note that apply resolves to itself, i.e. apply<F,G>::type is apply<F,G>. The reason for this will be apparent later. )

For instance, if we have types F, G and H standing for λ-terms F, G and H, the derived term

FH(GH)

is represented by the type

apply<apply<F,H>,apply<G,H> >

As we commented before, there is no syntactic facility for expressing lambda abstraction; instead, if a type is to represent an abstraction term we define its behavior under β-reduction by specializing apply. For instance, given the term

I = λx.x

we can represent it like this:

struct I;
template<typename X>
struct apply<I,X>{typedef X type;};

That is, we partially specialize apply so that apply<I,F>::type represents the β-reduction of (λx.x)f, i.e. f. This manner of handling lambda abstraction is particularly appealing in that it dispenses with α-reduction of bound variables by way of simply not representing bound variables at all (their role is played by template parameters).

More examples of representing lambda abstraction:

K = λxy.x

struct K;
template<typename X,typename Y>
struct apply<apply<K,X>,Y>{typedef X type;};

K* = λxy.y

struct KSTAR;
template<typename X,typename Y>
struct apply<apply<KSTAR,X>,Y>{typedef Y type;};

S = λxyz.xz(yz)

struct S;
template<typename X,typename Y,typename Z>
struct apply<apply<apply<S,X>,Y>,Z>{
 typedef typename apply<
  typename apply<X,Z>::type,
  typename apply<Y,Z>::type
 >::type type;
};

Note how currying is used in the specializations of apply for binary K and K* and ternary S. Another important aspect is that the application operation for S is deep in the sense that it not only composes the term XZ(YZ), as the following formulation would have done:

// lazy formulation
template<typename X,typename Y,typename Z>
struct apply<apply<apply<S,X>,Y>,Z>{
 typedef typename apply<
   typename apply<X,Z>,
   typename apply<Y,Z>
 > type;
};

but it also executes XZ(YZ) by invoking the nested ::type of each of the apply components. This amounts to implementing full β-reduction instead of lazy one-step reduction. In general, full reduction is assumed, that is, each λ-term represented in our embedding mechanism is actually in β-normal form. This rules out terms without β-nf as Ω:

ω = λx.xx
Ω = ωω

struct omega;
template<typename X>
struct apply<omega,X>{typedef typename apply<X,X>::type type;};

typedef apply<omega,omega>::type OMEGA; // compile-time error

Now, when a type X is "primitive" in the sense that it does not have any associated specialization of apply, apply<X,Y>::type evaluates to apply itself. So, if we have some term F and apply it to a succesion of primitive types X, Y, Z,... until no more active reductions remain, what we obtain is a syntactic description of the β-nf of F in the form of a composite apply expression with X, Y,... as terminals. For instance:

S →_β λxyz.xz(yz)

apply<apply<apply<S,X>::type,Y>::type,Z>::type evaluates to
apply<apply<X,Z>,apply<Y,Z> >

KI →_β λxy.y (= K*)

apply<apply<apply<K,I>::type,X>::type,Y>::type evaluates to Y

SKK →_β λx.x (= I)

apply<apply<apply<S,K>::type,K>::type,X>::type evaluates to X

This technique can be used to determine whether two λ-terms (as represented in our C++ embedding) are β-convertible.

In later entries we will play some more with our lambda calculus embedding.