[boost] PP: Beta-reducer for closed lambda-terms (save content as lambda.cpp)

From: Vesa Karvonen (vesa_karvonen_at_[hidden])
Date: 2003-04-11 11:06:24

#*****************************************************************************
#
# This is an applicative order beta-reducer for closed lambda-terms
# implemented using the C preprocessor.
#
# Usage:
#
#   cpp lambda.cpp '-DTERM=<term>' |tail -n1|sed 's# ##g'
#
# The syntax of lambda-terms:
#
#   <term> : LAMBDA(<symbol-or-_>,<term>)
#          | (<term>,<term>)
#          | <symbol>
#
#   <symbol> : A | B | C | ... | Z
#   <symbol-or-_> : <symbol> | _
#
# As you can see, underscores should only appear in the variable position of 
a
# LAMBDA. This convention makes it possible to use the underscore as a dummy
# variable in macros. Consider, for example, the IF(c,t,e) macro below, 
which
# must wrap the `t' and `e' terms inside a LAMBDA to prevent their 
evaluation.
#
# For example:
#
#   cpp lambda.cpp '-DTERM=(LAMBDA(X,X),LAMBDA(Y,Y))' |tail -n1|sed 's# ##g'
#
# Prints:
#
#   LAMBDA(Y,Y)
#
# Terms given to the evaluator must be closed, which means that terms must 
not
# contain free variables. The reason for this restriction is that this 
reducer
# does not perform alpha-conversion. The reducer also does not verify that
# terms are closed. For example, the term `LAMBDA(X,Y)' is not closed, 
because
# `Y' is not bound. On the other hand, `LAMBDA(Y,LAMBDA(X,Y))' is closed.
#
# This reducer has been tested on GNU CPP (3.2) and should work on any
# sufficiently standards conforming C preprocessor.
#
#*****************************************************************************
#
# The motivation for implementing this beta-reducer was twofold. The primary
# motivation was fun. It was quite fun to find a way to implement the 
reducer
# (much more fun than implementing a similar reducer in some more expressive
# language). A secondary motivation was to show that it might be possible to
# make preprocessor metaprogramming significantly easier than it is today.
#
# The design of contemporary C++ metaprogramming facilities are based on
# directly using the underlying evaluator (the C preprocessor or the C++
# template mechanism) in metaprograms. Metaprogramming libraries try to make
# programming easier by providing facilities that emulate features that the
# underlying evaluator does not directly support. For example, the Boost
# Preprocessor library implements the WHILE primitive, which makes it 
possible
# to use iteration, which is not directly supported by the C preprocessor, 
in
# programs.
#
# In other words, the idea of current metaprogramming libraries is to 
enhance
# the capabilities of the underlying evaluator by essentially building
# abstractions directly on top of the underlying "assembly language" towards
# the desired high-level language. Unfortunately, the limitations of the
# underlying evaluator are often fundamental and can not be completely fixed
# using such an bottom-up approach. For example, it can be rather difficult 
to
# implement "recursive" macros.
#
# The approach demonstrated by this beta-reducer is the opposite, top-down,
# strategy. Instead of enhancing the underlying evaluator towards the 
desired
# language, an evaluator for the high-level language is implemented 
directly.
#
# The top-down strategy has one clear benefit: the resulting language is not
# crippled (at least not as much) by the limitations of the underlying
# evaluator. For example, it is relatively easy to build recursive functions
# in the lambda calculus (by using the fixed-point combinator).
#
# The top-down strategy also has one major problem: the resulting evaluator 
is
# much slower than the underlying evaluator. How much slower such an 
evaluator
# would have to be is an open question. I would estimate that a nearly 
optimal
# evaluator could be "just" 2x-10x slower than the preprocessor. The 
reduction
# technique used by this evaluator is extremely slow (and simple). Faster
# evaluators would probably compile the lambda-terms and then execute the
# compiled terms using a suitable virtual machine (like the stack machine
# below).
#
# This beta-reducer implements only the core lambda-calculus. It should not 
be
# difficult to extend the language to include arithmetic, lists, conditional
# expressions, etc... This way a fairly expressive language could be built
# making it easy to express algorithms using the preprocessor.
#*/
#/***************************************************************************/
#
#/* Auxiliary primitives */
#
#define PP_CAT(x,y) PP_PRIMITIVE_CAT(x,y)
#define PP_PRIMITIVE_CAT(x,y) x##y
#
#define PP_CAR(a,d) a
#define PP_CDR(a,d) d
#define PP_CAAR(a,d) PP_CAR a
#define PP_CADR(a,d) PP_CAR d
#define PP_CDAR(a,d) PP_CDR a
#define PP_CDDR(a,d) PP_CDR d
#
#/***************************************************************************/
#
#/* A stack machine (can do 2^30-1 iterations - more than you want to wait) 
*/
#
#define PP_SM(s,p) PP_CADR(_,PP_SM_0((s,p)))
#
#define PP_SM_OVER(s,p) PP_CAT(PP_SM_OVER_,PP_SM_OVER_IS_PAIR p)
#define PP_SM_OVER_PP_SM_OVER_IS_PAIR
#define PP_SM_OVER_IS_PAIR(f,s) 1
#
#define PP_SM_OVER_1(i) PP_SM_B##i
#define PP_SM_STOP(i)
#
#define PP_SM_CAR_OP(a,d) a##_OP
#
#define PP_SM_0(sp) PP_SM_OVER sp(0)sp
#define PP_SM_1(sp) PP_SM_OVER sp(1)sp
#define PP_SM_2(sp) PP_SM_OVER sp(2)sp
#define PP_SM_3(sp) PP_SM_OVER sp(3)sp
#define PP_SM_4(sp) PP_SM_OVER sp(4)sp
#define PP_SM_5(sp) PP_SM_OVER sp(5)sp
#define PP_SM_6(sp) PP_SM_OVER sp(6)sp
#define PP_SM_7(sp) PP_SM_OVER sp(7)sp
#define PP_SM_8(sp) PP_SM_OVER sp(8)sp
#define PP_SM_9(sp) PP_SM_OVER sp(9)sp
#define PP_SM_10(sp) PP_SM_OVER sp(10)sp
#define PP_SM_11(sp) PP_SM_OVER sp(11)sp
#define PP_SM_12(sp) PP_SM_OVER sp(12)sp
#define PP_SM_13(sp) PP_SM_OVER sp(13)sp
#define PP_SM_14(sp) PP_SM_OVER sp(14)sp
#define PP_SM_15(sp) PP_SM_OVER sp(15)sp
#define PP_SM_16(sp) PP_SM_OVER sp(16)sp
#define PP_SM_17(sp) PP_SM_OVER sp(17)sp
#define PP_SM_18(sp) PP_SM_OVER sp(18)sp
#define PP_SM_19(sp) PP_SM_OVER sp(19)sp
#define PP_SM_20(sp) PP_SM_OVER sp(20)sp
#define PP_SM_21(sp) PP_SM_OVER sp(21)sp
#define PP_SM_22(sp) PP_SM_OVER sp(22)sp
#define PP_SM_23(sp) PP_SM_OVER sp(23)sp
#define PP_SM_24(sp) PP_SM_OVER sp(24)sp
#define PP_SM_25(sp) PP_SM_OVER sp(25)sp
#define PP_SM_26(sp) PP_SM_OVER sp(26)sp
#define PP_SM_27(sp) PP_SM_OVER sp(27)sp
#define PP_SM_28(sp) PP_SM_OVER sp(28)sp
#define PP_SM_29(sp) PP_SM_OVER sp(29)sp
#
#define PP_SM_B0(s,p) PP_SM_1(PP_SM_1(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B1(s,p) PP_SM_2(PP_SM_2(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B2(s,p) PP_SM_3(PP_SM_3(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B3(s,p) PP_SM_4(PP_SM_4(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B4(s,p) PP_SM_5(PP_SM_5(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B5(s,p) PP_SM_6(PP_SM_6(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B6(s,p) PP_SM_7(PP_SM_7(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B7(s,p) PP_SM_8(PP_SM_8(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B8(s,p) PP_SM_9(PP_SM_9(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B9(s,p) PP_SM_10(PP_SM_10(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B10(s,p) PP_SM_11(PP_SM_11(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B11(s,p) PP_SM_12(PP_SM_12(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B12(s,p) PP_SM_13(PP_SM_13(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B13(s,p) PP_SM_14(PP_SM_14(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B14(s,p) PP_SM_15(PP_SM_15(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B15(s,p) PP_SM_16(PP_SM_16(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B16(s,p) PP_SM_17(PP_SM_17(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B17(s,p) PP_SM_18(PP_SM_18(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B18(s,p) PP_SM_19(PP_SM_19(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B19(s,p) PP_SM_20(PP_SM_20(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B20(s,p) PP_SM_21(PP_SM_21(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B21(s,p) PP_SM_22(PP_SM_22(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B22(s,p) PP_SM_23(PP_SM_23(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B23(s,p) PP_SM_24(PP_SM_24(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B24(s,p) PP_SM_25(PP_SM_25(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B25(s,p) PP_SM_26(PP_SM_26(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B26(s,p) PP_SM_27(PP_SM_27(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B27(s,p) PP_SM_28(PP_SM_28(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B28(s,p) PP_SM_29(PP_SM_29(PP_SM_CAR_OP p(s,PP_CDR p)))
#define PP_SM_B29(s,p) PP_SM_CAR_OP p(s,PP_CDR p)
#
#/***************************************************************************/
#
#/* Auxiliary macros for dealing with lambda-terms */
#
#define PP_SAME(x,y) PP_SAME_(x,y)
#define PP_SAME_(x,y) PP_CAT(PP_SAME_,PP_SAME_##x(PP_CDR,PP_SAME_##y))
#define PP_SAME_1(a,d) d
#define PP_SAME_PP_SAME_A(c,y) PP_CAR
#define PP_SAME_PP_SAME_B(c,y) PP_CAR
#define PP_SAME_PP_SAME_C(c,y) PP_CAR
#define PP_SAME_PP_SAME_D(c,y) PP_CAR
#define PP_SAME_PP_SAME_E(c,y) PP_CAR
#define PP_SAME_PP_SAME_F(c,y) PP_CAR
#define PP_SAME_PP_SAME_G(c,y) PP_CAR
#define PP_SAME_PP_SAME_H(c,y) PP_CAR
#define PP_SAME_PP_SAME_I(c,y) PP_CAR
#define PP_SAME_PP_SAME_J(c,y) PP_CAR
#define PP_SAME_PP_SAME_K(c,y) PP_CAR
#define PP_SAME_PP_SAME_L(c,y) PP_CAR
#define PP_SAME_PP_SAME_M(c,y) PP_CAR
#define PP_SAME_PP_SAME_N(c,y) PP_CAR
#define PP_SAME_PP_SAME_O(c,y) PP_CAR
#define PP_SAME_PP_SAME_P(c,y) PP_CAR
#define PP_SAME_PP_SAME_Q(c,y) PP_CAR
#define PP_SAME_PP_SAME_R(c,y) PP_CAR
#define PP_SAME_PP_SAME_S(c,y) PP_CAR
#define PP_SAME_PP_SAME_T(c,y) PP_CAR
#define PP_SAME_PP_SAME_U(c,y) PP_CAR
#define PP_SAME_PP_SAME_V(c,y) PP_CAR
#define PP_SAME_PP_SAME_W(c,y) PP_CAR
#define PP_SAME_PP_SAME_X(c,y) PP_CAR
#define PP_SAME_PP_SAME_Y(c,y) PP_CAR
#define PP_SAME_PP_SAME_Z(c,y) PP_CAR
#define PP_SAME_PP_SAME__(c,y) PP_CAR
#define PP_SAME_A(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_B(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_C(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_D(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_E(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_F(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_G(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_H(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_I(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_J(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_K(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_L(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_M(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_N(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_O(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_P(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_Q(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_R(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_S(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_T(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_U(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_V(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_W(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_X(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_Y(c,y) c(1,y(PP_CAR,1))
#define PP_SAME_Z(c,y) c(1,y(PP_CAR,1))
#define PP_SAME__(c,y) c(1,y(PP_CAR,1))
#
#define PP_DISPATCH(prefix,ts) PP_CAT(prefix,PP_TYPE(PP_CAR ts))
#
#define PP_TYPE(t) PP_CAT(PP_TYPE_,PP_CAT(PP_TYPE_,PP_TYPE_APPLY t))
#define PP_TYPE_APPLY(t0,t1) PP_TYPE_A0
#define PP_TYPE_PP_TYPE_APPLY
#define PP_TYPE_PP_TYPE_A0 PP_TYPE_A1
#define PP_TYPE_PP_TYPE_A1 APPLY
#define PP_TYPE_LAMBDA(s,t) LAMBDA
#define PP_TYPE_A SYMBOL
#define PP_TYPE_B SYMBOL
#define PP_TYPE_C SYMBOL
#define PP_TYPE_D SYMBOL
#define PP_TYPE_E SYMBOL
#define PP_TYPE_F SYMBOL
#define PP_TYPE_G SYMBOL
#define PP_TYPE_H SYMBOL
#define PP_TYPE_I SYMBOL
#define PP_TYPE_J SYMBOL
#define PP_TYPE_K SYMBOL
#define PP_TYPE_L SYMBOL
#define PP_TYPE_M SYMBOL
#define PP_TYPE_N SYMBOL
#define PP_TYPE_O SYMBOL
#define PP_TYPE_P SYMBOL
#define PP_TYPE_Q SYMBOL
#define PP_TYPE_R SYMBOL
#define PP_TYPE_S SYMBOL
#define PP_TYPE_T SYMBOL
#define PP_TYPE_U SYMBOL
#define PP_TYPE_V SYMBOL
#define PP_TYPE_W SYMBOL
#define PP_TYPE_X SYMBOL
#define PP_TYPE_Y SYMBOL
#define PP_TYPE_Z SYMBOL
#define PP_TYPE__ SYMBOL
#
#define PP_VAR(t) PP_PRIMITIVE_CAT(PP_VAR_,t)
#define PP_VAR_LAMBDA(s,t) s
#
#define PP_TERM(t) PP_PRIMITIVE_CAT(PP_TERM_,t)
#define PP_TERM_LAMBDA(s,t) t
#
#/***************************************************************************/
#
#/* The beta-reducer (implemented using the stack machine) */
#
#define PP_EVAL(t) PP_CADR(_,PP_SM((t,_),(PP_EVAL,PP_SM_STOP)))
#define PP_EVAL_OP(t_ts,ps) PP_DISPATCH(PP_EVAL_,t_ts)(PP_CAR t_ts,PP_CDR 
t_ts,ps)
#define PP_EVAL_LAMBDA(t,ts,ps) ((t,ts),ps)
#define PP_EVAL_APPLY(t,ts,ps) ((PP_CDR t,(PP_CAR 
t,ts)),(PP_EVAL,(PP_SWAP,(PP_EVAL,(PP_APPLY,(PP_EVAL,ps))))))
#define PP_EVAL_SYMBOL(t,ts,ps) ((FREE VARIABLE: t,_),PP_SM_STOP)
#define PP_SWAP_OP(ts,ps) ((PP_CADR ts,(PP_CAR ts,PP_CDDR ts)),ps)
#define PP_APPLY_OP(t0_t1_ts,ps) ((PP_TERM(PP_CAR t0_t1_ts),PP_CDDR 
t0_t1_ts),(PP_SUBST,(PP_VAR(PP_CAR t0_t1_ts),(PP_CADR t0_t1_ts,ps))))
#define PP_SUBST_OP(t_ts,x_tx_ps) PP_DISPATCH(PP_SUBST_,t_ts)(PP_CAR 
t_ts,PP_CDR t_ts,PP_CAR x_tx_ps,PP_CADR x_tx_ps,PP_CDDR x_tx_ps)
#define PP_SUBST_SYMBOL(t,ts,x,tx,ps) ((PP_SAME(t,x)(tx,t),ts),ps)
#define PP_SUBST_LAMBDA(t,ts,x,tx,ps) 
PP_SAME(PP_VAR(t),x)(((t,ts),ps),((PP_TERM(t),ts),(PP_SUBST,(x,(tx,(PP_MK_LAMBDA,(PP_VAR(t),ps)))))))
#define PP_SUBST_APPLY(t,ts,x,tx,ps) ((PP_CDR t,(PP_CAR 
t,ts)),(PP_SUBST,(x,(tx,(PP_SWAP,(PP_SUBST,(x,(tx,(PP_MK_APPLY,ps)))))))))
#define PP_MK_APPLY_OP(t0_t1_ts,ps) (((PP_CAR t0_t1_ts,PP_CADR 
t0_t1_ts),PP_CDDR t0_t1_ts),ps)
#define PP_MK_LAMBDA_OP(t_ts,x_ps) ((LAMBDA(PP_CAR x_ps,PP_CAR t_ts),PP_CDR 
t_ts),PP_CDR x_ps)
#
#/***************************************************************************/
#
#/* Definitions for common lambda-terms */
#
#/* Identity */
#define ID LAMBDA(X,X)
#
#/* Church-booleans */
#define TRUE LAMBDA(T,LAMBDA(F,T))
#define FALSE LAMBDA(T,LAMBDA(F,F))
#define AND LAMBDA(A,LAMBDA(B,((A,B),FALSE)))
#define TEST LAMBDA(L,LAMBDA(M,LAMBDA(N,((L,M),N))))
#
#/* Pairs */
#define PAIR LAMBDA(F,LAMBDA(S,LAMBDA(B,((B,F),S))))
#define FST LAMBDA(P,(P,TRUE))
#define SND LAMBDA(P,(P,FALSE))
#
#/* Church-numerals */
#define ZERO LAMBDA(S,LAMBDA(Z,Z))
#define ONE LAMBDA(S,LAMBDA(Z,(S,Z)))
#define TWO LAMBDA(S,LAMBDA(Z,(S,(S,Z))))
#define THREE LAMBDA(S,LAMBDA(Z,(S,(S,(S,Z)))))
#define SUCC LAMBDA(N,LAMBDA(S,LAMBDA(Z,(S,((N,S),Z)))))
#define ZZ LAMBDA(B,((B,ZERO),ZERO))
#define SS LAMBDA(P,LET(F,(P,FALSE),LET(S,(SUCC,F),LAMBDA(B,((B,F),S)))))
#define PRED LAMBDA(M,(((M,SS),ZZ),TRUE))
#define PLUS LAMBDA(M,LAMBDA(N,LAMBDA(S,LAMBDA(Z,((M,S),((N,S),Z))))))
#define TIMES LAMBDA(M,LAMBDA(N,((M,(PLUS,N)),ZERO)))
#define IS_ZERO LAMBDA(M,((M,LAMBDA(_,FALSE)),TRUE))
#
#/* Fixed-point combinator */
#define FIX LAMBDA(F,LET(G,LAMBDA(X,(F,LAMBDA(Y,((X,X),Y)))),(G,G)))
#
#/* Factorial */
#define FACT 
(FIX,LAMBDA(F,LAMBDA(N,IF((IS_ZERO,N),ONE,((TIMES,N),(F,(PRED,N)))))))
#
#/* Some syntactic sugar */
#define LET(s,i,t) (LAMBDA(s,t),i)
#define IF(c,t,e) (((c,LAMBDA(_,t)),LAMBDA(_,e)),ID)
#
#/***************************************************************************/
#
#/* Invokes the beta-reducer */
#
#ifndef TERM
#define TERM ((AND,FALSE),TRUE)
#endif
#
PP_EVAL(TERM)

_________________________________________________________________
Protect your PC - get McAfee.com VirusScan Online 
http://clinic.mcafee.com/clinic/ibuy/campaign.asp?cid=3963