The classical way to represent natural numbers in λ-calculus was invented by Church:

This translates to our C++ embedding as follows:0= λfx.x1= λfx.fx2= λfx.f(fx)

...N= λfx.f^{n}(x)

The corresponding basic arithmetic operations are easy to define:`struct ZERO;`

template<typename F,typename X>

struct apply<apply<ZERO,F>,X>{typedef X type;};

struct ONE;

template<typename F,typename X>

struct apply<apply<ONE,F>,X>:apply<F,X>{};

struct TWO;

template<typename F,typename X>

struct apply<apply<TWO,F>,X>:`apply<F,typename apply<F,X>::type>{};`

...

and to translate to C++:SUCC= λnfx.f(nfx) (successor function)PLUS= λmnfx.nf(mfx)MULT= λmn.m(PLUSn)0

`// syntax sugar to abbreviate notation`

template<typename F,typename G,typename H>

struct apply2{

typedef typename apply<typename apply<F,G>::type,H>::type type;

};

struct SUCC;

template<typename N,typename F,typename X>

struct apply<apply<apply<SUCC,N>,F>,X>:

apply<F,typename apply2<N,F,X>::type>{};

struct PLUS;

template<typename M,typename N,typename F,typename X>

struct apply<apply<apply<apply<PLUS,M>,N>,F>,X>:

apply2<N,F,typename apply2<M,F,X>::type>{};

struct MULT;

template<typename M,typename N>

struct apply<apply<MULT,M>,N>:

apply2<M,typename apply<PLUS,N>::type,ZERO>{};

I've written a little C++ program exercising these ideas (you'll need Boost to compile it). How to test our constructs? That is, how to verify for instance that the type `NINE`

defined as:

`typedef apply<apply<MULT,THREE>::type,THREE>::type NINE;`

actually corresponds to λ*fx*.

*f*(

*f*(

*f*(

*f*(

*f*(

*f*(

*f*(

*f*(

*fx*)))))))))? Well, if we define

then we have thattemplate <int N>struct int_{};

struct succ;

template<int N> struct apply<succ,int_<N> >{

typedef int_<N+1> type;

};

`apply<apply<N,succ>::type,int_<0> >::type`

is the same type as`int_<n>`

as long as `N`

stands for the Church numeral **N**. This verification can be easily done with some metaprogramming machinery. Note that `succ`

is not a proper λ-term even though we have used it inside our `apply`

machinery: this hints at a general technique called λ-calculus *extension*.

One rather nice part of C++11 - variadic templates - allows 'apply' to be expressed in a much more natural (and limitless) fashion:

ReplyDeletetemplate struct apply : apply::type, Z...> { };

template struct apply { typedef apply type; };

One rather nice feature of C++11 - variadic templates - permits a much more natural (and limitless) expression of λ/apply:

ReplyDeletetemplate struct apply : apply::type, Z...> { };

template struct apply { typedef apply type; };