lc 0.1

输入

注意输入中的漂亮Unicode λ：此REPL使用Readline在输入时按反斜杠 (\) 输入一个 λ。

缩写

你可以开始任何“蒙提·派森”常规操作，人们会为你完成它。每个人都像缩写一样知道它。

——罗宾·威廉姆斯

注意输入在末尾被转换为相应的Church数字。此解释器具有缩写符号的概念

1. 缩写用花括号 ({}) 表示，并且是 不区分大小写 的。

2. Church数字以及许多其他常见缩写都是为您预定义的。

3. 在Church数字上可以省略花括号，因为数字不允许用作变量。

4. 使用 = 运算符定义缩写。

λ> {ABC}=λf.λx.x
λ> {ABC}
INPUT λf.λx.x

Potential shorthand representations:
-> As Church numeral 0
-> As {FALSE}
-> As {ABC}
λ> {IF}{FALSE}1{ABC}
INPUT (λp.λa.λb.pab)(λx.λy.y)(λf.λx.fx)(λf.λx.x)
β ==> (λa.λb.(λx.λy.y)ab)(λf.λx.fx)(λf.λx.x)
β ==> (λb.(λx.λy.y)(λf.λx.fx)b)(λf.λx.x)
β ==> (λx.λy.y)(λf.λx.fx)(λf.λx.x)
β ==> (λy.y)(λf.λx.x)
β ==> λf.λx.x

Potential shorthand representations:
-> As Church numeral 0
-> As {FALSE}
-> As {ABC}

{succ}=λn.λf.λx.f(nfx)
{add}=λm.λn.(m{succ}n)
{mult}=λm.λn.(m({add}n)0)
{true}=λx.λy.x
{false}=λx.λy.y
{and}=λp.λq.pqp
{or}=λp.λq.ppq
{not}=λp.p{false}{true}
{if}=λp.λa.λb.pab
{cons}=λx.λy.λf.fxy
{car}=λc.c{true}
{cdr}=λc.c{false}
{nil}=λx.{true}
{pred}=λn.λf.λx.n(λg.λh.h(gf))(λu.x)(λu.u)
{sub}=λm.λn.n{pred}m
{zero?}=λn.n(λx.{false}){true}
{nil?}=λp.p(λx.λy.{false})
{lte?}=λm.λn.{zero?}({sub}mn)

错误

无。狗有跳蚤，没有错误。

——Mutt手册页

• {pred}（以及由此产生的 {sub}）似乎有一些问题。

• 当变量因为应用冲突而相同时，它们将显示为相同的变量，但解释器仍然将它们视为不同的变量。需要做的是在发生这种情况时检测到某种机制，并对变量进行自动α重命名。

如果您解决了这些问题中的任何一个，我们非常欢迎您提交一个PR！