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 ⊢M:A$
$M$ is the term under context $\Gamma$ with type $A$
M 是语境 $\Gamma$ 下类型为 A 的项

Reduction

• Beta rule

$$\frac{x:A⊢M:BN:A}{(\lambda x.M)N\equiv M[x\mapsto N]:B}\beta \text{ rule }$$

Typing Rules

Links

• Alonzo Church - Wikipedia
• Haskell Curry - Wikipedia
• Curry–Howard correspondence - Wikipedia
• Anonymous Function
• Lambda Calculus