lambda shell

这是一个简单的REPL shell，用于无类型lambda表达式。我主要写它是为了稍微玩一下lambda演算。其中一些部分效率很低，但适用于教育目的。

该shell可以评估lambda表达式、赋值和宏。

示例

有内建的项 SUCC 和 NIL，可以用church数来创建自然数

[λ] @usestd
@usestd

[λ] one := SUCC NIL
one := SUCC NIL

[λ] two := SUCC (SUCC NIL)
two := SUCC (SUCC NIL)

[λ] !normalize (ADD one two)
\f . \x . f (f (f x))

您可以在运行时选择不同的归约策略

[λ] @usestd
@usestd

[λ] !vnormalize (AND TRUE FALSE)
AND TRUE FALSE
(\q . TRUE q TRUE) FALSE
(\q . (\y . q) TRUE) FALSE
(\q . q) FALSE
FALSE

[λ] @set strategy normal
@set strategy normal

[λ] !vnormalize (AND TRUE FALSE)
AND TRUE FALSE
(\q . TRUE q TRUE) FALSE
TRUE FALSE TRUE
(\y . FALSE) TRUE
FALSE

功能

• 普通（最左外层）和适用性（最左内层）归约策略
• 避免捕获的替换
• 通过内建提供简单构造
• 用于处理lambda术语的宏

安装

有关安装和从源代码构建的更多信息，请在此处查看。