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.

## No comments :

## Post a Comment