types - 在研究简单类型的 Lambda 微积分时发现了哪些奇怪的方程

Question

我正在学习简单类型的 Lambda 微积分，但我对这些方程感到困惑。

我想知道它们叫什么以及它们是如何工作的。

谢谢你的帮助！

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

标签： typesfunctional-programminglambda-calculustyped-lambda-calculus

Answer 1

它们通常被称为演绎规则、打字规则，或者，一般来说，推理规则。由于 Gentzen 在自然演绎中的使用，带有推理条的符号是 AFAIK。

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

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

• Whenv2是一个值，则 lambda 应用程序(\x : T2 . t1) v2减少为t1with xint1替换为v2。（那是 Beta 减少）
• 当归t1结为 时t1'，则应用t1 t2归结为t1' t2。
• 当v1是一个值，并t2减少到t2'，然后应用程序v1 t2减少到v1 t2'。

所以在这种情况下，它们实际上不是输入规则，而是评估（减少）如何工作的规则。