问题描述
我正在学习单纯型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'。
因此，在这种情况下，它们实际上不是键入规则，而是用于评估（归约）工作原理的规则。