Friday, November 2, 2007

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

No comments :

Post a Comment