Monday, December 24, 2007

λ-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;};
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>:
typename apply<FAC,typename apply<pred,N>::type>::type

template<typename N>
struct apply<FAC,N>:
typename apply3<
typename apply<iszero,N>::type,
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.

No comments :

Post a Comment