type synthesis など

論理 Lean 用語法

https://www.cs.vu.nl/~jbe248/lv2017/10x4.pdf より：

the {type checking | proof verification} problem

  • Γ |-? t:A

the {typability | type {synthesis | inference}} problem

  • Γ |- t:?

the {{type | proposition} inhabitation | proposition provability} problem

  • Γ |- ?:A

還元性〈reduction〉

subject reduction

// タイピングはβ変換で保存される

if Γ |- t:A and t -β→ s
then Γ |- s:A

unique normal forms

// 計算の結果は合流により一意である。CR性
// 計算が止まることは保証されない。

if M -β→ N and M -β→ P,
then 
exists Q, N -β→ Q and P -β→ Q

termination (strong normalization)

すべての計算は、正規形で終了する。