σ τ (στ) ι στ (στ) σ_{1}σ_{2}σ_{3}

σ_{1}(σ_{2}σ_{3}) σ σ_{1} … σ_{n}ι type con- texts Γ ≡ x_{1} : σ_{1}, …, x_{n} : σ_{n}

σ_{i} x_{i} x_{i} : σ_{i} Γ Γ Γ′ x_{i} : σ_{i}

Γ ⊢ M : σ(MσΓ)

?? Γ, x : σ, Δ ⊢ x : σ  Γ, x : σ ⊢ M : τΓ ⊢ (λx:σ. M) : στ

Γ ⊢ M : στΓ ⊢ N : σΓ ⊢ M(N) : τΓ ⊢ M : σσΓ ⊢_{σ} (M) : σ

Γ ⊢:  Γ ⊢ M : Γ ⊢ (M) :

Γ ⊢ M : Γ ⊢ (M) :  Γ ⊢ M_{i} : (i=1, 2, 3)Γ ⊢ (M_{1}, M_{2}, M_{3}) :

Γ ⊢ M : σ π(Γ) ⊢

M : σ π Γ σ Γ ⊢ M : σ Γ M type

checking

M Γ σ Γ ⊢ M : σ MN (MN)

M(N) M_{1} … M_{n} (… (M_{1}M_{2}) … M_{n}) M_{1}(M_{2}) … (M_{n}) λ α– conversion N x M M N lambda capture– free substitution^{1} M :: = x | (λx:σ.M) | M(M) |_{σ} (M) |

These are the same conventions as usually employed for the quantifiers ∀ and ∃. The only difference is that quantifiers turn formulas into for-

| (M) | (M) | (M, M, M)

λx:.x(x) x x(x)

(?? \underline{n}) / (nu-) meral n \underline{0} ≡

\underline{k+1} ≡

(\underline{k}) k^{2}

\begin{matrix}x x & λx:σ.M λx:σ.M \\ M λx:σ.EE[N/x] V M(N) V & M(_{σ}(M)) V_{σ}(M) V \\ \underline{0} \underline{0} & M \underline{n}(M) \underline{n+1} \\ M \underline{0}(M) \underline{0} & M \underline{n+1}(M) \underline{n} \\ M \underline{0}M_{1} V (M, M_{1}, M_{2}) V & M \underline{n+1}M_{2} V (M, M_{1}, M_{2}) V \end{matrix}

EV V λ EV V E E EV V λ val- ues V V V V MV M λx:σ.M M

determinstic MV MW V ≡ W MV

Subject Reduction

(Subject Reduction)

⊢ M : σ MV ⊢ V : σ MV

M MV V ≡ (\underline{n}) / (n M στ) MV V ≡ λx:σ.E E x : σ ⊢ E : τ

Γ ⊢:Γ ⊢:

Γ ⊢ M : Γ ⊢ M_{1} : σΓ ⊢ M_{2} : σ(σ ∈ {, })Γ ⊢_{σ} (M, M_{1}, M_{2}) : σ

M M_{1} V_{σ}(M, M_{1}, M_{2}) V M M_{2} V_{σ}(M, M_{1}, M_{2}) V

isz isz(M)

M isz(M)

M\underline{0}

M\underline{n+1} n isz (M, M_{1}, M_{2}) ≡_{(}

isz(M), M_{1}, M_{2})

(\underline{0}) / (\underline{1})

MN M N ??

?? leftmost outermost

M_{1}M_{2}E[M_{1}]E[M_{2}]

E evaluation contexts

E := [ ] | E(M) | (E) | (E) | (E, M_{1}, M_{2})

M E M ≡ E[N]

N NN′

∗

MV M^{∗}V V

mulas whereas λ– abstraction turns terms into terms. Notice that in the literature one finds variants of

where instead of

there are constants

(\underline{n}) / (for)

every natural number n. However, the same rules can be used for defining

inductively (al-