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`

,

`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

is represented by the type

we can represent it like this:

`F`

, `G`

and `H`

standing for λ-terms *F*,*G*and*H*, the derived termFH(GH)

`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 termI= λx.x

`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**)

This technique can be used to determine whether two λ-terms (as represented in our C++ embedding) are β-convertible.`apply<apply<apply<S,K>::type,K>::type,X>::type`

evaluates to`X`

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

## No comments :

## Post a Comment