Last active
December 31, 2024 05:11
-
-
Save Trebor-Huang/895ec18ccb819334a5011d7c68df1df4 to your computer and use it in GitHub Desktop.
Evaluator for lambda calculus in Typst
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// *** Jump to the bottom for example usage *** | |
#set page(paper: "a5") | |
#let Lam(var, body) = ("Lam", var, body) | |
#let App(fun, arg) = ("App", fun, arg) | |
// An elaborate pretty printer because I'm bored | |
#let print-var(str) = if str.starts-with("@") { | |
$x_#str.slice(1)$ // generated variable name | |
} else {$#str$} | |
#let print(expr, prec) = if type(expr) == str { | |
print-var(expr) | |
} else if expr.at(0) == "Lam" { | |
let vars = $lambda$ | |
while type(expr) == array and expr.at(0) == "Lam" { | |
vars = vars + print-var(expr.at(1)) | |
expr = expr.at(2) | |
} | |
let r = vars + $.$ + print(expr, 0) | |
if prec > 0 { | |
math.lr("(" + r + ")") | |
} else { | |
r | |
} | |
} else { | |
let r = print(expr.at(1), 1) + print(expr.at(2), 2) | |
if prec > 1 { | |
math.lr("(" + r + ")") | |
} else { | |
r | |
} | |
} | |
// *** Begin dark magic *** | |
#let reflect(prog) = () => ( | |
() => prog, | |
(x) => reflect(App(reflect(prog), x)) | |
) | |
#let reify(sem) = { | |
let body = sem().at(0)() | |
if body.at(0) == "Lam" { | |
Lam(body.at(1), reify(body.at(2))) | |
} else if body.at(0) == "App" { | |
App(reify(body.at(1)), reify(body.at(2))) | |
} else { | |
body | |
} | |
} | |
#let interpret(prog, env, fresh) = { | |
if type(prog) == str { | |
env.at(prog) | |
} else if prog.at(0) == "Lam" { | |
/* If fresh is a counter, we only need to make an increment here | |
and nothing else in the other branch. */ | |
let name = "@" + str(fresh) | |
let body(x) = { | |
let _env = (: ..env) | |
_env.insert(prog.at(1), x) | |
interpret(prog.at(2), _env, fresh * 3) | |
} | |
() => ( | |
() => Lam(name, body(reflect(name))), | |
body | |
) | |
} else { | |
interpret(prog.at(1), env, fresh * 3 + 1)().at(1)( | |
interpret(prog.at(2), env, fresh * 3 + 2) | |
) | |
} | |
} | |
#let evaluate(prog) = reify(interpret(prog, (:), 1)) | |
// *** End dark magic *** | |
// Some quick test cases | |
#let zero = Lam("f", Lam("x", "x")) | |
#let one = Lam("f", Lam("x", App("f", "x"))) | |
#let two = Lam("f", Lam("x", App("f", App("f", "x")))) | |
#let three = Lam("f", Lam("x", App("f", App("f", App("f", "x"))))) | |
#let add(m, n) = Lam("f", Lam("x", | |
App(App(m, "f"), App(App(n, "f"), "x")))) | |
#let mul(m, n) = Lam("f", Lam("x", | |
App(App(m, App(n, "f")), "x"))) | |
#let expr = mul(three, two) | |
The Church numeral encoding of $3 times 2$ is | |
$ #print(expr, 0) $ | |
and the evaluation result is | |
$ #print(evaluate(expr), 0) $ | |
which is $6$. | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment