Simply Typed Lambda Calculus
# Judgement
- Premise
- Conclusion
$$\frac{\text{Premise}{1} ~ \text{Premise}{2}..n}{\text{Conclusion}} (\text{Name})$$
# Context
$$\Gamma ~ \text{ctx}$$
# Term
$$\Gamma \vdash M : A$$
$M$ is the term under context $\Gamma$ with type $A$
M 是语境 $\Gamma$ 下类型为 A 的项
# Reduction
- Beta rule
$$
\frac{x: A \vdash M: B \quad N: A}{(\lambda x . M) N \equiv M[x \mapsto N]: B} \beta \text { rule }
$$