λ演算的β-约化子和速记表示
lc的Python项目详细描述
这个工具通过提供一个 回复：
λ> (λc.c(λx.λy.x))((λx.λy.λf.fxy)(λf.λx.f(fx))(λf.λx.f(f(fx)))) INPUT (λc.c(λx.λy.x))((λx.λy.λf.fxy)(λf.λx.f(fx))(λf.λx.f(f(fx)))) β ==> (λx.λy.λf.fxy)(λf.λx.f(fx))(λf.λx.f(f(fx)))(λx.λy.x) β ==> (λy.λf.f(λf.λx.f(fx))y)(λf.λx.f(f(fx)))(λx.λy.x) β ==> (λf.f(λf.λx.f(fx))(λf.λx.f(f(fx))))(λx.λy.x) β ==> (λx.λy.x)(λf.λx.f(fx))(λf.λx.f(f(fx))) β ==> (λy.λf.λx.f(fx))(λf.λx.f(f(fx))) β ==> λf.λx.f(fx) Potential shorthand representations: -> As Church numeral 2
输入
注意输入中漂亮的unicodeλ：这个REPL使用Readline输入 当您键入反斜杠（\）时，λ。
速记
You can start any ‘Monty Python’ routine and people finish it for you. Everyone knows it like shorthand.
—Robin Williams
上面的通知输入被转换成相应的速记教会 最后是数字。这个口译员有速记符号的概念：
- 速记是用大括号（{}）写的，并且不区分大小写。
- 教会数字，以及许多其他常见的速记，是预先定义的 你
- 大括号可以省略在教会的数字，因为数字是不允许的 用作变量。
- 使用=运算符定义速记。
λ> {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)
错误
None. Mutts have fleas, not bugs.
—Mutt Manual Page
- {pred}（因此，{sub}）似乎有某种问题。
- 当应用程序导致变量冲突时，它们将显示为 相同的变量，但是解释器仍然将它们视为单独的 变量。需要做的是在 会发生这种情况，并自动对变量进行α-重命名
如果你解决了这两个问题，公关是非常感谢！
欢迎加入QQ群-->： 979659372
