complete playground for lambda-calculus (still not ideal though)

Rratic · Rratic · commit 238b2e89be3f · 2026-03-23T00:43:41.000+08:00
diff --git a/content/posts/lambda_calculus.md b/content/posts/lambda_calculus.md
@@ -2,7 +2,7 @@
 title = "无类型 λ 演算"
 description = "最经典的类型论例子：无类型 λ 演算的规则、使用和合流性。"
 date = 2025-03-22
-updated = 2025-04-12
+updated = 2026-03-23
 
 [extra]
 math = true
@@ -20,7 +20,7 @@ tags = ["笔记", "数学", "计算机", "函数式编程", "可运行"]
 
 本节讨论的是 Alonzo Church 发明的 lambda calculus **无类型 λ 演算**。[^paper-invention]
 
-本站提供了一个[在线演绎器](/playground/lambda_calculus.html)。
+本站提供了一个[在线演绎器](/playground/lambda_calculus.html)，其中使用 `@eval` 命令做正则次序的求值并尝试简化，输出使用 de Brujin 无名表示（`#i` 表示从里到外第 $i$ 层函数声明对应的参数）。想要自行编写解释器的读者可参考其仓库 [Rratic/my-lam](https://github.com/Rratic/my-lam).
 
 ## 语法 {#grammar}
 Lambda 演算的语法形式极其简单。一种可理解的形式文法如下：
diff --git a/static/playground/lambda_calculus.html b/static/playground/lambda_calculus.html
@@ -13,45 +13,46 @@
 <body>
 	<div id="terminal">
 		<div class="output stream"></div>
-		<div class="line input"><span id="to-click" class="prompt">>>> </span><span id="to-input" class="command" contenteditable="true">// ===== Standard Library =====
-// SK Pack
+		<div class="line input"><span id="to-click" class="prompt">>>> </span><span id="to-input" class="command" contenteditable="true"># ===== Standard Library =====
+# SK Pack
 S = λx. λy. λz. x z (y z)
 K = λx. λy. x
 I = S K K
 ι = λf. (f S) K
 
-// Boolean Pack
+# Boolean Pack
 T = λx. λy. x
 F = λx. λy. y
 IfThenElse = λe. λu. λv.e u v
 
-// List Pack
+# List Pack
 Nil = λc. λn. n
 Cons = λh. λt. λc. λn. c h (t c n)
 
-// Natural Number Pack
+# Natural Number Pack
 0 = λf. λs. s
 1 = λf. λs. f s
 2 = λf. λs. f (f s)
 3 = λf. λs. f (f (f s))
 
 IsZero = λn. n (λx. F) T
 Succ = λn. λf. λs. f (n f s)
-Plus = λn. λm. λf. λx. n f (m f x)
-Mul = λn. λm. λf. λx. n (m f) x
+Plus = λn. λm. n Succ m
+Mul = λn. λm. n (Plus m) 0
 
-// High Order Functions
-// TODO
+Prev = λn. λf. λx. n (λg. λh. h (g f)) (λu. x) λu. u
 
-// Recursion
+# High Order Functions
+# TODO
+
+# Recursion
 Ω = λx. x x
 Y = λf. (λx. f (x x)) λx. f (x x)
 Z = λf. (λx. f (λy. (x x) y)) (λx. f (λy. (x x) y))
 
-P = λn. λf. λx. n (λg. λh. h (g f)) (λu. x) λu. u
-Fact = λf. λn. IsZero n 1 (Mul n (f (P n)))
+Fact = λf. λn. IfThenElse (IsZero n) 1 (Mul n (f (Prev n)))
 
-// ===== Test =====
+# ===== Test =====
 @eval write_your_expr_here</span>
 		</div>
 	</div>
@@ -82,7 +83,10 @@
 				else {
 					let span = document.createElement("span");
 					span.innerText = token;
-					if (token == "λ") {
+					if (token[0] == "#") {
+						span.style.color = "green";
+					}
+					else if (token == "λ") {
 						span.style.color = "purple";
 					}
 					else if (token == "@") {
diff --git a/static/script/lambda/stt_bg.wasm b/static/script/lambda/stt_bg.wasm
