研究单纯型Lambda微积分时发现的怪异方程是什么

如何解决研究单纯型Lambda微积分时发现的怪异方程是什么

我正在学习单纯型Lambda演算，但是我对这些方程感到困惑。

我想知道它们的名字以及它们的工作方式。

感谢您的帮助！

（图片取自https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html）

解决方法

通常将它们称为推导规则typing rule，或者通常称为推理规则。由于根特森（Gentzen）在自然演绎中的使用，带有推论条的符号为AFAIK。

确切的解释取决于您所描述的系统，但是通常的想法是“顶部的事物暗示/允许底部的事物”。在这种特定情况下，它看起来并不那么正式，但是如果您之前已经看过这种东西的话，就足够了。有关人们通常写的类型理论的更正式的“语义学”，请参见here。

在您的特定情况下，我将规则翻译为：

• 当v2为值时，lambda应用程序(\x : T2 . t1) v2简化为t1，其中x中的t1被v2取代。 （即Beta减少）
• 当t1降为t1'时，应用程序t1 t2降为t1' t2。
• 如果v1是一个值，并且t2减少为t2'，则应用程序v1 t2减少为v1 t2'。

因此，在这种情况下，它们实际上不是键入规则，而是用于评估（归约）工作原理的规则。