https://github.com/Hirrolot/metalang99/blob/master/examples/lambda_calculus.c Skip to content Sign up * Why GitHub? Features - + Mobile - + Actions - + Codespaces - + Packages - + Security - + Code review - + Issues - + Integrations - + GitHub Sponsors - + Customer stories- * Team * Enterprise * Explore + Explore GitHub - Learn and contribute + Topics - + Collections - + Trending - + Learning Lab - + Open source guides - Connect with others + The ReadME Project - + Events - + Community forum - + GitHub Education - + GitHub Stars program - * Marketplace * Pricing Plans - + Compare plans - + Contact Sales - + Education - [ ] * # In this repository All GitHub | Jump to | * No suggested jump to results * # In this repository All GitHub | Jump to | * # In this user All GitHub | Jump to | * # In this repository All GitHub | Jump to | Sign in Sign up {{ message }} Hirrolot / metalang99 Public * Notifications * Star 378 * Fork 12 * * Code * Issues 2 * Pull requests 0 * Discussions * Actions * Projects 0 * Wiki * Security * Insights More * Code * Issues * Pull requests * Discussions * Actions * Projects * Wiki * Security * Insights Permalink master Switch branches/tags [ ] Branches Tags Could not load branches Nothing to show {{ refName }} default View all branches Could not load tags Nothing to show {{ refName }} default View all tags metalang99/examples/lambda_calculus.c Go to file * Go to file T * Go to line L * * Copy path * Copy permalink @Hirrolot Hirrolot Use the same naming convention across the examples Latest commit 2fc9c6c Oct 10, 2021 History 1 contributor Users who have contributed to this file 209 lines (154 sloc) 8.1 KB Raw Blame * Open with Desktop * View raw * * View blame /* * An untyped lambda calculus [1] interpreter using De Bruijn indices [2] and normal order * evaluation strategy [3]. * * [1]: https://en.wikipedia.org/wiki/Lambda_calculus * [2]: https://en.wikipedia.org/wiki/De_Bruijn_index * [3]: https://en.wikipedia.org/wiki/Evaluation_strategy# Normal_order */ #include // Syntactic terms { #define var(i) ML99_call(var, i) #define appl(M, N) ML99_call(appl, M, N) #define lam(M) ML99_call(lam, M) #define var_IMPL(i) v(VAR(i)) #define appl_IMPL(M, N) v(APPL(M, N)) #define lam_IMPL(M) v(LAM(M)) #define VAR(i) ML99_CHOICE(var, i) #define APPL(M, N) ML99_CHOICE(appl, M, N) #define LAM(M) ML99_CHOICE(lam, M) // } (Syntactic terms) // Variable substitution: `M[1=x]` { #define subst(M, x) ML99_call(subst, M, x) #define subst_IMPL(M, x) substAux_IMPL(M, x, 1) #define substAux_IMPL(M, x, depth) ML99_callUneval (ML99_matchWithArgs, M, substAux_, x, depth) #define substAux_var_IMPL(i, x, depth) \ ML99_IF( \ ML99_NAT_EQ(i, depth), \ v(x), \ ML99_call(ML99_if, ML99_callUneval(ML99_greater, i, depth), v(VAR (ML99_DEC(i)), VAR(i)))) #define substAux_appl_IMPL(M, N, x, depth) \ appl(substAux_IMPL(M, x, depth), substAux_IMPL(N, x, depth)) #define substAux_lam_IMPL(M, x, depth) \ lam(ML99_call(substAux, v(M), incFreeVars_IMPL(x), v(ML99_INC (depth)))) // } (Variable substitution) // Increment free variables in `M` { #define incFreeVars(M) ML99_call(incFreeVars, M) #define incFreeVars_IMPL(M) incFreeVarsAux_IMPL(M, 1) #define incFreeVarsAux_IMPL(M, depth) ML99_callUneval (ML99_matchWithArgs, M, incFreeVarsAux_, depth) #define incFreeVarsAux_var_IMPL(i, depth) \ ML99_call(ML99_if, ML99_callUneval(ML99_greaterEq, i, depth), v(VAR (ML99_INC(i)), VAR(i))) #define incFreeVarsAux_appl_IMPL(M, N, depth) \ appl(incFreeVarsAux_IMPL(M, depth), incFreeVarsAux_IMPL(N, depth)) #define incFreeVarsAux_lam_IMPL(M, depth) lam(incFreeVarsAux_IMPL(M, ML99_INC(depth))) // } (Increment free variables) // Evaluation { #define eval(M) ML99_call(eval, M) #define eval_IMPL(M) ML99_callUneval(ML99_match, M, eval_) #define eval_var_IMPL(i) v(VAR(i)) #define eval_appl_IMPL(M, N) ML99_callUneval(ML99_matchWithArgs, M, eval_appl_, N) #define eval_lam_IMPL(M) lam(eval_IMPL(M)) #define eval_appl_var_IMPL(i, N) appl(v(VAR(i)), eval_IMPL(N)) #define eval_appl_appl_IMPL(M, N, N1) \ ML99_call(ML99_matchWithArgs, eval(appl_IMPL(M, N)), v (eval_appl_appl_, N1)) #define eval_appl_lam_IMPL(M, N) eval(subst_IMPL(M, N)) #define eval_appl_appl_var_IMPL eval_appl_var_IMPL #define eval_appl_appl_appl_IMPL(M, N, N1) appl(appl_IMPL(M, N), eval_IMPL(N1)) #define eval_appl_appl_lam_IMPL eval_appl_lam_IMPL // } (Evaluation) // Syntactical equality { #define termEq(lhs, rhs) ML99_matchWithArgs(lhs, v(termEq_), rhs) #define termEq_var_IMPL(i, rhs) termEqPropagate(var, rhs, i) #define termEq_appl_IMPL(M, N, rhs) termEqPropagate(appl, rhs, M, N) #define termEq_lam_IMPL(M, rhs) termEqPropagate(lam, rhs, M) #define termEqPropagate(term_kind, rhs, ...) \ ML99_IF( \ ML99_IDENT_EQ(TERM_, ML99_CHOICE_TAG(rhs), term_kind), \ ML99_matchWithArgs(v(rhs), v(termEq_##term_kind##_), v (__VA_ARGS__)), \ ML99_false()) #define termEq_var_var_IMPL(j, i) v(ML99_NAT_EQ(i, j)) #define termEq_appl_appl_IMPL(M, N, M1, N1) ML99_and(termEq(v(M), v (M1)), termEq(v(N), v(N1))) #define termEq_lam_lam_IMPL(M, M1) termEq(v(M), v(M1)) #define TERM_var_var () #define TERM_appl_appl () #define TERM_lam_lam () // } (Syntactical equality) #define ASSERT_REDUCES_TO(lhs, rhs) \ /* Use two interpreter passes: one for `eval(lhs)`, one for `termEq `. Thereby we achieve more \ * Metalang99 reduction steps available. */ \ ML99_ASSERT_UNEVAL(ML99_EVAL(termEq(v(ML99_EVAL(eval(v(lhs)))), v (ML99_EVAL(eval(v(rhs))))))) // The identity combinator { #define I LAM(VAR(1)) ASSERT_REDUCES_TO(APPL(I, VAR(5)), VAR(5)); // } (The identity combinator) // The K, S combinators { #define K LAM(LAM(VAR(2))) #define S LAM(LAM(LAM(APPL(APPL(VAR(3), VAR(1)), APPL(VAR(2), VAR(1 )))))) ASSERT_REDUCES_TO(APPL(APPL(S, K), K), I); ASSERT_REDUCES_TO(APPL(APPL(APPL(S, K), S), K), K); ASSERT_REDUCES_TO(APPL(APPL(APPL(S, K), VAR(5)), VAR(6)), VAR(6)); ASSERT_REDUCES_TO(APPL(APPL(K, VAR(5)), VAR(6)), VAR(5)); // } (The K, S combinators) // Church booleans { #define T LAM(LAM(VAR(2))) #define F LAM(LAM(VAR(1))) #define NOT LAM(APPL(APPL(VAR(1), F), T)) #define AND LAM(LAM(APPL(APPL(VAR(2), VAR(1)), VAR(2)))) #define OR LAM(LAM(APPL(APPL(VAR(2), VAR(2)), VAR(1)))) #define XOR LAM(LAM(APPL(APPL(VAR(2), APPL(NOT, VAR(1))), VAR(1)))) #define IF LAM(LAM(LAM(APPL(APPL(VAR(3), VAR(2)), VAR(1))))) ASSERT_REDUCES_TO(APPL(NOT, T), F); ASSERT_REDUCES_TO(APPL(NOT, F), T); ASSERT_REDUCES_TO(APPL(NOT, APPL(NOT, T)), T); ASSERT_REDUCES_TO(APPL(NOT, APPL(NOT, F)), F); ASSERT_REDUCES_TO(APPL(APPL(AND, T), T), T); ASSERT_REDUCES_TO(APPL(APPL(AND, T), F), F); ASSERT_REDUCES_TO(APPL(APPL(AND, F), T), F); ASSERT_REDUCES_TO(APPL(APPL(AND, F), F), F); ASSERT_REDUCES_TO(APPL(APPL(OR, T), T), T); ASSERT_REDUCES_TO(APPL(APPL(OR, T), F), T); ASSERT_REDUCES_TO(APPL(APPL(OR, F), T), T); ASSERT_REDUCES_TO(APPL(APPL(OR, F), F), F); ASSERT_REDUCES_TO(APPL(APPL(XOR, T), T), F); ASSERT_REDUCES_TO(APPL(APPL(XOR, T), F), T); ASSERT_REDUCES_TO(APPL(APPL(XOR, F), T), T); ASSERT_REDUCES_TO(APPL(APPL(XOR, F), F), F); ASSERT_REDUCES_TO(APPL(APPL(APPL(IF, T), VAR(5)), VAR(6)), VAR(5)); ASSERT_REDUCES_TO(APPL(APPL(APPL(IF, F), VAR(5)), VAR(6)), VAR(6)); // } (Church booleans) // Church numerals { #define ZERO LAM(LAM(VAR(1))) #define SUCC LAM(LAM(LAM(APPL(VAR(2), APPL(APPL(VAR(3), VAR(2)), VAR (1)))))) #define ONE APPL(SUCC, ZERO) #define TWO APPL(SUCC, ONE) #define THREE APPL(SUCC, TWO) #define FOUR APPL(SUCC, THREE) #define ADD LAM(LAM(LAM(LAM(APPL(APPL(VAR(4), VAR(2)), APPL(APPL(VAR (3), VAR(2)), VAR(1))))))) #define MUL LAM(LAM(LAM(LAM(APPL(APPL(VAR(4), APPL(VAR(3), VAR(2))), VAR(1)))))) ASSERT_REDUCES_TO(APPL(APPL(ADD, ZERO), ZERO), ZERO); ASSERT_REDUCES_TO(APPL(APPL(ADD, ZERO), ONE), ONE); ASSERT_REDUCES_TO(APPL(APPL(ADD, ONE), ZERO), ONE); ASSERT_REDUCES_TO(APPL(APPL(ADD, ONE), TWO), THREE); ASSERT_REDUCES_TO(APPL(APPL(MUL, ZERO), ZERO), ZERO); ASSERT_REDUCES_TO(APPL(APPL(MUL, ZERO), ONE), ZERO); ASSERT_REDUCES_TO(APPL(APPL(MUL, ONE), ZERO), ZERO); ASSERT_REDUCES_TO(APPL(APPL(MUL, TWO), TWO), FOUR); // } (Church numerals) // Church pairs { #define PAIR LAM(LAM(LAM(APPL(APPL(VAR(1), VAR(3)), VAR(2))))) #define FST LAM(APPL(VAR(1), T)) #define SND LAM(APPL(VAR(1), F)) ASSERT_REDUCES_TO(APPL(FST, APPL(APPL(PAIR, VAR(5)), VAR(6))), VAR(5 )); ASSERT_REDUCES_TO(APPL(SND, APPL(APPL(PAIR, VAR(5)), VAR(6))), VAR(6 )); // } (Church pairs) // Church lists { #define NIL F #define CONS PAIR #define IS_NIL LAM(APPL(APPL(VAR(1), LAM(LAM(LAM(F)))), T)) #define LIST_1_2_3 APPL(APPL(CONS, VAR(1)), APPL(APPL(CONS, VAR(2)), APPL(APPL(CONS, VAR(3)), NIL))) ASSERT_REDUCES_TO(APPL(IS_NIL, NIL), T); ASSERT_REDUCES_TO(APPL(IS_NIL, LIST_1_2_3), F); // } (Church lists) // Recursion via self-application (or the Y combinator) is perfectly expressible, though when // executed, it exhausts the Metalang99 recursion engine limit. int main(void) {} * Copy lines * Copy permalink * View git blame * Reference in new issue * Reference in new discussion [ ] Go * (c) 2021 GitHub, Inc. * Terms * Privacy * Security * Status * Docs * Contact GitHub * Pricing * API * Training * Blog * About You can't perform that action at this time. You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.