简单类型 λ 演算

$A\to B$ 是函数接口：输入须有 $A$ 型，应用结果获得 $B$ 型。推导树把每次变量使用、抽象和应用的接口匹配记录下来；执行前无法构造推导的项被静态排除。

简单类型没有解递归类型方程的机制。给 $xx$ 定型会要求同一声明中的 $x$ 既有某个参数类型 $A$，又有函数类型 $A\to B$，进而需要有限类型满足 $A=A\to B$。右侧比 $A$ 多一个箭头构造子及一个 $B$ 子树，有限语法树不可能与自己的严格扩张相等，所以方程无解。因而循环项 $\mathrm{\Omega }=(\lambda x.xx)(\lambda x.xx)$ 被挡在类型推导之外。

恒等项可由

定型。若上下文含 $f:A\to B$ 与 $x:A$，应用规则得到 $fx:B$，连续两次抽象便有

这棵推导同时展示箭头右结合与上下文中临时假设的解除。顺序不能颠倒：先解除 $x:A$ 得到 $f:A\to B⊢\lambda x:A.fx:A\to B$，再解除 $f$，才得到最外面的 $(A\to B)\to (A\to B)$。

自应用被排除并不表示所有嵌套调用被排除。若 $f:A\to A$ 且 $x:A$，先推出 $fx:A$，再推出 $f(fx):A$；两次调用中的参数类型均为 $A$，没有要求 $A$ 等于箭头类型。类型检查限制的是接口是否一致，而不是应用次数。

类型判断不等于运行结果。开项 $x:A⊢x:A$ 良类型，却在没有环境时不能独立执行；闭项 $(\lambda x:A.x)(\lambda y:B.y)$ 是否良类型取决于实参类型是否正好是 $A$。原始语法相似不能替代推导。

加入固定点常量 $\mathsf{fix}:(T\to T)\to T$ 后，可以写出良类型发散项；进展与保持仍可能成立，强正规化却立即失效。类型安全与终止是不同元定理。

另一种更小的非终止扩充见上下文等价理路上下文等价Contextual equivalence · 程序上下文等价固定类型、语言与观察后，以所有良类型闭合程序上下文能否区分两个部件来定义可替换性。：在含 Bool、布尔常量和条件式的 STLC 扩充上，再增加原始常量 $\mathrm{\Omega }:\mathsf{Bool}$ 及规则 $\mathrm{\Omega }\to \mathrm{\Omega }$，便足以研究严格性和高阶观察。该语言沿用简单类型规则，发散由新增常量及其自环产生；本页纯 STLC 的强正规化定理适用于加入它之前的语言。

STLC 是静态语义与动态语义相互作用的最小实验场。进展与保持定理理路进展与保持定理Progress and preservation · Type safety对按值调用的简单类型 lambda 演算逐层解释规范形、替换、进展与保持，以及类型安全的准确结论。说明良类型闭项不会因类型错误卡住，强正规化定理理路简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个良类型简单 λ 项都强正规化：任意完整 β-归约路径都在有限步后结束。另外证明每条完整 β-归约路径都有限。后者严格强于某个求值策略终止。

在Curry–Howard 对应理路Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。下，箭头类型对应蕴含，项对应自然演绎证明，β-归约对应证明化简。积、和、多态与依赖类型可继续扩展这条对应，但每项扩展都需重新检查类型规则、动态规则与元定理。