在lambda演算中按值调用

如何解决在lambda演算中按值调用

| 我正在通过类型和编程语言进行工作，Pierce提出了“减少价值”策略，给出了术语“ 0”的示例。首先将内部redex

id (λz. id z)

还原为

λz. id z

，然后将外部redex还原为正常形式

λz. id z

，这是第一次还原的结果。 但是按值顺序调用被定义为“仅减少最外面的redex”，而“仅当其右手侧已减小为value时才减少redex”。在示例中，“ 1”出现在最外面的redex的右侧，并被简化。这与仅减少最外部的redex的规则如何平方？ “最外层”和“最内层”仅是lambda抽象的答案吗？因此，对于

λz. t

中的

t

而言，

t

不能被还原，但是在redex

s t

中，如果可能的话，

t

被还原为

v

，然后

s v

被还原？     

解决方法

        简短的回答：是的。您永远不能减少lambda项的内部，只能从正确的开始减少外部的项。 按值在lambda演算中的评估上下文的集合定义如下：

E = [ ] | (λ.t)E | Et

E是您可以评估的东西。 例如，按名称命名为lambda演算，评估上下文为：

E = [ ] | Et | fE

因为即使术语不是值，您也可以减少应用程序。 例如，“ 15”卡在按值调用中，但按名称调用中则减为“ 16”，这是正常形式。 在上下文中，语法“ 17”是一种普通形式（按名称调用），其定义为：

f = λx.t | L  
L = x | L f

您可以在Pierce的第19.5.3章中看到上下文的另一种定义。     ,           “最外层”和“最内层”仅是lambda抽象的答案吗？因此对于λz中的项t。 t，t不能被减小，但是在redex s t中，如果可能的话，t被减小到值v，然后s v被减小？ 是的，那是完全正确的。