Wednesday, November 14, 2007

λ-fun in metaC++: Church numerals

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

0 = λfx.x
1 = λfx.fx
2 = λfx.f(fx)
...
N = λfx.fn(x)
This translates to our C++ embedding as follows:
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>{};
...
The corresponding basic arithmetic operations are easy to define:
SUCC = λnfx.f(nfx) (successor function)
PLUS = λmnfx.nf(mfx)
MULT = λmn.m(PLUS n) 0
and to translate to C++:
// 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
template <int N>struct int_{};
struct succ;
template<int N> struct apply<succ,int_<N> >{
typedef int_<N+1> type;
};
then we have that
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.


2 comments :

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

    template struct apply : apply::type, Z...> { };
    template struct apply { typedef apply type; };

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

    template struct apply : apply::type, Z...> { };
    template struct apply { typedef apply type; };

    ReplyDelete