λ-fun in metaC++: extensions and term rewriting

So-called λδ-calculi involve the addition to λ-calculus of some set C of external terms along with δ rules describing the reductions by which terms involving entities of C behave, additionally to those of standard λ-calculus. For instance, instead of relying on the cumbersome and computationally expensive Church numerals we can embed natural numbers directly:

• C = {succ,pred,+,*,iszero}+{0,1,2,...}.
• succ n →_δ (n+1) for any natural n.
• pred n →_δ (n-1) for any natural n>0.
• + n m →_δ (n+m) for any natural n, m.
• * n m →_δ (nm) for any natural n, m.
• iszero 0 →_δ TRUE, iszero n →_δ FALSE for natural n>0.

Many nice properties of λ-calculus, like the Church-Rosser Property, are retained in λδ-calculi.

Our translation of λ-calculus to metaC++ allows us to easily accomodate δ extensions: we only have to supply δ-reductions as additional specializations of the apply metafunction:

template <int N> struct int_;

struct succ;
template<int N>
struct apply<succ,int_<N> >{typedef int_<N+1> type;};

struct pred;
template<int N>
struct apply<pred,int_<N> >{typedef int_<N-1> type;};

struct plus;
template<int M,int N>
struct apply<apply<plus,int_<M> >,int_<N> >{typedef int_<M+N> type;};

struct mult;
template<int M,int N>
struct apply<apply<mult,int_<M> >,int_<N> >{typedef int_<M*N> type;};

struct iszero;
template<int N>
struct apply<iszero,int_<N> >{typedef FALSE type;};
template<>
struct apply<iszero,int_<0> >{typedef TRUE type;};

Our former FAC function using Church numerals can be adapted to work with these by simply replacing the original set of numerical operations and constants with the new ones:

struct FAC;

struct FACIF;
template<typename N>
struct apply<FACIF,N>{typedef int_<1> 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
>
{};

The complete program is provided.

Why it was so easy to accomodate δ-reductions in our C++ rendition of λ-calculus? Well, a basic premise of the embedding procedure is that there is no explicit representation for λ-abstractions and these are rather described operationally according to their reduction behavior: what we really have is a term rewriting engine, which is what C++ template partial specialization ultimately boils down to, and what δ-reduction is all about.

In the end λ-calculus itself is nothing but a kind of Term Rewriting System, where allowable rewritings are described in terms of λ-abstractions. In a way, the theory of TRSs captures the basic essence of λ-calculus and allows for a more general treatment of the subject.