我正在学习简单类型的 Lambda 微积分,但我对这些方程感到困惑。
我想知道它们叫什么以及它们是如何工作的。
谢谢你的帮助!
(图片取自https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html)
我正在学习简单类型的 Lambda 微积分,但我对这些方程感到困惑。
我想知道它们叫什么以及它们是如何工作的。
谢谢你的帮助!
(图片取自https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html)
它们通常被称为演绎规则、打字规则,或者,一般来说,推理规则。由于 Gentzen 在自然演绎中的使用,带有推理条的符号是 AFAIK。
确切的解释取决于您所描述的系统,但总体思路是“顶部的事物暗示/允许底部的事物”。在这种特定情况下,它看起来并不那么正式,但如果您以前见过这种东西就足够了。有关人们通常编写的类型理论的更正式的“语义”,请参见此处。
在您的特定情况下,我会将规则翻译为:
v2
是一个值,则 lambda 应用程序(\x : T2 . t1) v2
减少为t1
with x
int1
替换为v2
。(那是 Beta 减少)t1
结为 时t1'
,则应用t1 t2
归结为t1' t2
。v1
是一个值,并t2
减少到t2'
,然后应用程序v1 t2
减少到v1 t2'
。所以在这种情况下,它们实际上不是输入规则,而是评估(减少)如何工作的规则。