#/**************************************************************************** # # Copyright (C) 2003 Vesa Karvonen # # Permission to copy, use, modify, sell and distribute this software is # granted provided this copyright notice appears in all copies. This software # is provided "as is" without express or implied warranty, and with no claim # as to its suitability for any purpose. # #***************************************************************************** # # This is an applicative order beta-reducer for closed lambda-terms # implemented using the C preprocessor. # # Usage: # # cpp lambda.cpp '-DTERM=' |tail -n1|sed 's# ##g' # # The syntax of lambda-terms: # # : LAMBDA(,) # | (,) # | # # : A | B | C | ... | Z # : | _ # # 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)