如何解决SKS 是否等于 SKK?
背景
昨晚我开始自学 lambda 演算,我试图确定我目前所理解的是否正确。
了解
SKK 相当于标识组合子 I。
其中 L 代表 lambda:
S = LxLyLz((xz)(yz))
K = LxLy(x)
K 本质上采用接下来的 2 个 (lambda) 项并返回其中的第一个。 S 在无类型 lambda 演算中似乎更复杂一些。
我的解释
SK(any-lambda-term) 也等价于 I。
即将 S 对 K 的应用应用到 Any-lambda-term 等价于 Identity 组合子:
((S K)(Any)) = I = S K K = ((S K)(K))
如果有帮助的话,我在上面的符号中使用了“左关联”的约定(并且我试图在上面的第四项中用括号说明这一点。到目前为止我读到的所有内容似乎都使用了这个约定) .
推理
S K = LyLz((K z)(y z))
下一个 lambda 项将替换 y,让项为 Y。
S K Y = Lz((K z)(Y z))
(Y z) 是 Y 到 z 的应用,也是一个 lambda 项。 (K z) 返回返回 z 的常量函数,给定另一个项输入:(Y z)。
我的解释是真的吗?如果不是,你能解释一下吗?我将不胜感激。特别是如果可以解释某种操作顺序——我经常发现自己在考虑何时评估时感到困惑。也许这会随着实践而完善。
解决方法
你的直觉是正确的,但直觉证明不了任何事情(唉......)
那么,我们如何证明您的陈述?只需表明 SKK 和 SKS 具有相同的行为即可。 “行为”是一个非正式的概念,它被“语义”正式捕获:如果 SKK 和 SKS 相等,那么根据 SKI 演算语义,它们应该总是归约为相同的术语。
现在,有一个很深的问题,那就是:什么是 SKI 演算?实际上,没有一种方法可以回答这个问题。你在你的问题中隐含地做的是,你根据λ项表达SKI,并且你依赖λ演算的语义。这是完全正确的。另一种方法可能是直接定义 SKI 语义。例如,如果您查看 wikipedia page,您可以看到语义不是用 lambda 术语定义的(并且它对应于 lambda 术语的事实是(好的和预期的)副作用)。在本答案的其余部分中,我将采用与您相同的方法,并将 SKI 术语转换为 λ 术语。一个很好的练习是使用正确的 SKI 语义重做证明。
那么,让您的问题正式化:您的问题是,对于任何滑雪术语 t
,SKKt = SKSt
是否?嗯...让我们看看。
SKKt
在 λ 演算中被编码为 (λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.x)t
。我们现在只需要将其简化为正常形式(我详细说明了每一步,每次我减少最左边的 λ,即使这不是最快的策略):
(λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.x)t
= (λy.λz.((λx.λy.x)z)(yz))(λx.λy.x)t
= (λz.((λx.λy.x)z)((λx.λy.x)z))t
= ((λx.λy.x)t)((λx.λy.x)t)
= (λy.t)((λx.λy.x)t)
= t
因此,λ演算中SKKt
的编码简化为t
(作为旁注,我们刚刚在这里证明了SKK
等价于I
)。为了总结我们的证明,我们必须减少 SKSt
,看看它是否也减少到 t
。
SKSt
被编码为 (λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.λz.(xz)(yz))t
。让我们减少它。 (这次就不详细说了)
(λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.λz.(xz)(yz))t
= ((λx.λy.x) t)((λx.λy.λz.(xz)(yz)) t))
= (λy.t)((λx.λy.λz.(xz)(yz)) t))
= t
万岁!它也减少到 t
,所以实际上,SKS
和 SKK
是等价的。第三个组合子似乎并不重要:只要你有SK?
,它就等价于I
。作为练习,您可以轻松证明它(相同的策略,如果是这种情况,则对于任何术语 t
和 s
,SKts = s
)。如上所述,另一个很好的练习是在不使用 λ 语义的情况下重做证明,而是使用适当的 SKI 语义。
最后,我的回答应该向您提出一个新问题:我们有两种语义,一种将 SKI 术语编码为 λ 术语,另一种则没有。您可能会遇到的问题是:这两种语义是否等价?两个语义等价是什么意思?如果您刚开始自学 λ 演算,现在尝试回答这些问题可能有点早,但是您可以将它保留在您的脑海中,以便您更熟悉正式语言时。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。