Lambda 演算 (λa.b)((λx.xx)(λx.xx)) [关闭]答案

【问题标题】：Lambda Calculus (λa.b)((λx.xx)(λx.xx)) [closed]Lambda 演算 (λa.b)((λx.xx)(λx.xx)) [关闭]
【发布时间】：2014-01-09 12:37:46
【问题描述】：

我正在寻找弱归一化 lambda 项的示例。我这样说对吗：

(λa.b)((λx.xx)(λx.xx))

减少到：

或：

不会终止（如果您尝试减少 (λx.xx)(λx.xx)）

我不确定第一次减少是否正确，所以需要澄清一下，谢谢。

【问题讨论】：

【解决方案1】：

如果你首先评估正确的术语并且不断地那么它永远不会达到一个范式，因此它不是强归一化的。如果您首先评估左项，它将立即达到范式，因此它是可归一化的，并证明该项是弱归一化的。这也是无类型 lambda 演算不合流的一个例子。

请注意，与特定术语相比，您更有可能想要谈论重写系统是如何规范化的。因此，该术语是无类型 lambda 演算的强归一化特性的反例，但不能提供 ULC 弱归一化（而且不是）的积极证据。

【讨论】：