人间正自有赖 嬉戏、无邪与过剩的花朵, 否则世界就太小, 生趣就太枯涸。

1

# Untyped Lambda Calculus

Definition (The Set Λ\Lambda of Untyped λ-Terms)

  • Variable: If xVx\in V, then xΛx\in\Lambda.
  • Application: If M,NΛM,N\in\Lambda, then (M  N)Λ(M\;N)\in\Lambda.
  • Abstraction: If xVx\in V and MΛM\in\Lambda, then (λx.M)Λ(\lambda x.M)\in\Lambda.

Notation(Terms)

  • Lowercase latin letters x,y,z,...x,y,z,... denote term variables.
  • Uppercase latin letters L,M,N,...L,M,N,... denote λ-terms.
  • Syntactical identity will be denoted with \equiv.

Notation(Parentheses)

  • Outer most parentheses may be omitted: (λx.(M))=λx.M(\lambda x.(M))=\lambda x.M.
  • Application is left-associative: (M  N)  LM  N  L(M\;N)\;L\equiv M\;N\;L.
  • Abstraction is right-associative: λx.(λy.M)λx.λy.M\lambda x.(\lambda y.M)\equiv \lambda x.\lambda y.M.
  • Application takes precedence over abstraction: λx.(M  N)=λx.M  N\lambda x.(M\;N)=\lambda x.M\;N.

Definition(The Set of Free Variables FV of a λ-Term)

  • Variable: FV(x)={x}FV(x)=\{x\}.
  • Application: FV(M  N)=FV(M)FV(N)FV(M\;N)=FV(M)\cup FV(N).
  • Abstraction: FV(λx.M)=FV(M)/{x}FV(\lambda x.M)=FV(M)/\{x\}.

Definition(α-Conversion)

Two λ-terms M,NΛM,N\in\Lambda are α-convertible, denoted by MNM\equiv N, if and only if they differ only by the names of their bound variables.

Definition(Barendregt Conversion)

All bound variables in a λ-term MΛM\in\Lambda should be pairwise different and chosen such that they differ from the free variables in the term.

Definition(Substitution)

  • Variable: x[x:=N]Nx[x:=N]\equiv N. y[x:=N]yy[x:=N]\equiv y if xyx\neq y.
  • Application: (P  Q)[x:=N](P[x:=N])  (Q[x:=N])(P\;Q)[x:=N]\equiv (P[x:=N])\;(Q[x:=N]).
  • Abstraction: (λy.P)[x:=N]λy.(P[x:=N])(\lambda y.P)[x:=N]\equiv\lambda y.(P[x:=N]), if yFV(N)y\notin FV(N).

Definition(One-step β-Reduction β\rightarrow_\beta)

  • Basis: (λx.M)  NβM[x:=N](\lambda x.M)\;N\rightarrow_\beta M[x:=N].
  • Compatibility: If MβNM\rightarrow_\beta N, then M  LβN  LM\;L\rightarrow_\beta N\;L, L  MβL  NL\;M\rightarrow_\beta L\; N and λx.Mβλx.N\lambda x.M\rightarrow_\beta \lambda x.N.

Definition(Many-step β-Reduction β\rightarrow^*_\beta)

MβNM\rightarrow^*_\beta N if there is an n0n\geq 0 and terms M0,...,MnΛM_0,...,M_n\in\Lambda such that M0M,MnNM_0\equiv M,M_n\equiv N and for all 1in1\leq i\leq n:

MiβMi+1M_i\rightarrow_\beta M_{i+1}

Definition(β-Conversion =β=_\beta)

M=βNM=_\beta N if there is an n0n\geq 0 and terms M0,...,MnΛM_0,...,M_n\in\Lambda such that M0M,MnNM_0\equiv M,M_n\equiv N and for all 1in1\leq i\leq n:

MiβMi+1Mi+1βMiM_i\rightarrow_\beta M_{i+1}\vee M_{i+1}\rightarrow_\beta M_i

Definition(β-Normal Form)

  • MM is in β-normal form if MM does not contain any redex.
  • MM has a β-normal form if there is an NΛN\in\Lambda in β-normal form such that M=βNM=_\beta N.

For example, (λx.(λy.x  y)  z)  v(\lambda x.(\lambda y.x\;y)\;z)\;v has a β-normal form v  zv\;z.

Ω=(λx.x  x)(λx.x  x)\Omega=(\lambda x.x\;x)(\lambda x.x\;x) does not have a β-normal form.

But (λv.u)  Ωβu(\lambda v.u)\;\Omega\rightarrow_\beta u or get into infinite reduction chain.

Definition(Weak Normalization, Strong Normalization)

  • MM is weakly normalizing if there is an NΛN\in\Lambda in β-normal form such that MβNM\rightarrow^*_\beta N.
  • MM is strongly normalizing if every chain of reductions starting from MM reaches the β-normal form.

Definition(Normalization of Systems)

A rewrite system is strongly/weakly normalizing if every term in the system is strongly/weakly normalizing. Otherwise it is not normalizing.

Theorem:

Let M,N1,N2ΛM,N_1,N_2\in\Lambda be λ-terms with MβN1M\rightarrow^*_\beta N_1 and MβN2M\rightarrow^*_\beta N_2.

Then there is a λ-term N3ΛN_3\in\Lambda such that N1βN3N_1\rightarrow^*_\beta N_3 and N2βN3N_2\rightarrow^*_\beta N_3.


Definition(Natural Numbers N\mathbb{N})

  • Zero: 0N0\in\mathbb{N}.
  • Successor: If nNn\in\mathbb{N}, then succ(n)Nsucc(n)\in\mathbb{N}.

Definition(Church Numerals cnc_n)

0=λf.λx.xsucc(succ(...succ(0)))ntimes=λf.λx.f  (f  ...(f  x))ntimes0=\lambda f.\lambda x.x\\ \underbrace {succ(succ(...succ(0)))}_{n-times}=\lambda f.\lambda x.\underbrace {f\;(f\;...(f\;x))}_{n-times}

succλm.λf.λx.f  (m  f  x)predλn.λf.λx.n  (λg.λh.h  (g  f))  (λu.x)  (λu.u)addλm.λn.λf.λx.m  f  (n  f  x)subλm.λn.(n  pred)  mmulλm.λn.λf.λx.m  (n  f)  xsucc\equiv \lambda m.\lambda f.\lambda x.f\;(m\;f\;x)\\ pred\equiv \lambda n.\lambda f.\lambda x.n\;(\lambda g.\lambda h.h\;(g\;f))\;(\lambda u.x)\;(\lambda u.u)\\ add\equiv \lambda m.\lambda n.\lambda f.\lambda x.m\;f\;(n\;f\;x)\\ sub\equiv \lambda m.\lambda n.(n\;pred)\;m\\ mul\equiv\lambda m.\lambda n.\lambda f.\lambda x.m\;(n\;f)\;x

Definition(Church Booleans)

  • True: T=λx.λy.xT=\lambda x.\lambda y.x.
  • False: F=λx.λy.yF=\lambda x.\lambda y.y.

λx.λy.x  y  Fλx.λy.x  T  y¬λx.x  F  T\wedge\equiv \lambda x.\lambda y.x\;y\;F\\ \vee\equiv \lambda x.\lambda y.x\;T\;y\\ \neg\equiv \lambda x.x\;F\;T

“if B then M else N” B  M  N\equiv B\;M\;N.

What’s more:

isZeroλn.n  (λx.F)  Tleqλm.λn.isZero  (sub  m  n)eqλm.λn.(leq  m  n)(leq  n  m)isZero\equiv\lambda n.n\;(\lambda x.F)\;T\\ leq\equiv\lambda m.\lambda n.isZero\;(sub\;m\;n)\\ eq\equiv \lambda m.\lambda n.(leq\;m\;n)\wedge(leq\;n\;m)


Theorem(Fixed Point Theorem):

For all MΛM\in\Lambda there exists PΛP\in\Lambda such that M  P=βPM\;P=_\beta P.

P(λx.M  (x  x))  (λx.M  (x  x))P\equiv (\lambda x.M\;(x\;x))\;(\lambda x.M\;(x\;x)). PβM  PP\rightarrow^*_\beta M\;P.

Definition(Combinator)

A combinator is a term without any free variables.

Definition(Fixed Point Combinator - Mathematics)

A fixed point combinator is a higher-order function that takes a function as argument and returns the fixed point of that function.

Definition(Y - Combinator)

Yλf.(λx.f  (x  x))  (λx.f  (x  x))Y\equiv\lambda f.(\lambda x.f\;(x\;x))\;(\lambda x.f\;(x\;x))

We have g  (Y  g)=βY  gg\;(Y\;g)=_\beta Y\;g. So Y  gY\;g returns a fixed point of gg.

Now we can compute recursive functions:

fact=λf.λx.(isZero  x)  1  (mult  x  (f  (pred  x)))fact=βY  fact=βfact  (Y  fact)=βλx.(isZero  x)  1  (mult  x  ((Y  fact)  (pred  x)))λx.(isZero  x)  1  (mult  x  (fact  (pred  x)))fact'=\lambda f.\lambda x.(isZero\;x)\;1\;(mult\;x\;(f\;(pred\;x)))\\ -----------------------------\\ fact=_\beta Y\;fact'\\ =_\beta fact'\;(Y\;fact')\\ =_\beta \lambda x.(isZero\;x)\;1\;(mult\;x\;((Y\;fact')\;(pred\;x)))\\ \equiv \lambda x.(isZero\;x)\;1\;(mult\;x\;(fact\;(pred\;x)))

Obviously it’s a weakly normalizing term.

# Simple Typed Lambda Calculus(λ\lambda_\rightarrow)

Definition(The Set T\mathbb{T} of Simple Types)

  • Variable Type: If αV\alpha\in\mathbb{V}, then αT\alpha\in\mathbb{T}.
  • Arrow Type: If σ,τT\sigma,\tau\in\mathbb{T}, then (στ)T(\sigma\rightarrow\tau)\in\mathbb{T}.

Noticing that VV is the set of variables and V\mathbb{V} is the set of types named variable types.

Notation

  • α,β,γ,...\alpha,\beta,\gamma,... denote type variables.
  • σ,τ,ρ,...\sigma,\tau,\rho,... denote arbitrary types.
  • Syntactical identity will be denoted with \equiv.
  • Outermost parentheses may be omitted.
  • Arrow types are right-associative: σ(τρ)στρ\sigma\rightarrow(\tau\rightarrow\rho)\equiv\sigma\rightarrow\tau\rightarrow\rho.

Definition(The Set Λ\Lambda^\rightarrow of Pre-Typed λ\lambda_\rightarrow-Terms)

  • Variable: If xVx\in V, then xΛx\in\Lambda^\rightarrow.
  • Application: If M,NΛM,N\in\Lambda^\rightarrow, then (M  N)Λ(M\;N)\in\Lambda^\rightarrow.
  • Abstraction: If xV,σTx\in V,\sigma\in\mathbb{T} and MΛM\in\Lambda^\rightarrow, then (λx:σ.M)Λ(\lambda x:\sigma.M)\in\Lambda^\rightarrow.

Definition

  • A statement is of the form M:σM:\sigma, MM is called the subject and σ\sigma the type.
  • A declaration is a statement x:σx:\sigma.
  • A context Γ\Gamma is a set of declarations with different subjects.
  • A judgement is of the form ΓM:σ\Gamma\vdash M:\sigma.
  • A term MM is called legal if there exists Γ\Gamma and σ\sigma such that ΓM:σ\Gamma\vdash M:\sigma.

Derivation Rules:

Γx:σif  x:σΓ(var)ΓM:στΓN:σΓM  N:τ(appl)Γ,x:σM:τΓλx:σ.M:στ(abst)\Gamma\vdash x:\sigma\quad if\;x:\sigma\in\Gamma\quad(var)\\ \frac{\Gamma\vdash M:\sigma\rightarrow\tau\quad\Gamma\vdash N:\sigma}{\Gamma\vdash M\;N:\tau}\quad(appl)\\ \frac{\Gamma,x:\sigma\vdash M:\tau}{\Gamma\vdash\lambda x:\sigma.M:\sigma\rightarrow\tau}\quad(abst)

Type Checking: Given a context Γ\Gamma, term MM and type σ\sigma, to check whether ΓM:σ\Gamma\vdash M:\sigma

Well-typedness: Given a term MM, to find whether ?M:??\vdash M:?.

Type Assignment: Given a context Γ\Gamma and a term MM, to find whether ΓM:?\Gamma\vdash M:?.

Inhabitation: Given a context Γ\Gamma and a type σ\sigma, to find whether Γ?:σ\Gamma\vdash ?:\sigma.

λ\lambda_\rightarrow is poly-time decidable!

Definition(Domain)

The domain of a context Γ=x1:σ1,..,xn:σn\Gamma=x_1:\sigma_1,..,x_n:\sigma_n is dom(Γ)={x1,...,xn}dom(\Gamma)=\{x_1,...,x_n\}.

Lemma: If ΓM:σ\Gamma\vdash M:\sigma, then FV(M)dom(Γ)FV(M)\subseteq dom(\Gamma).

Lemma(Thinning): Let Γ1,Γ2\Gamma_1,\Gamma_2 be contexts with Γ1Γ2\Gamma_1\subseteq\Gamma_2. If Γ1M:σ\Gamma_1\vdash M:\sigma, then also Γ2M:σ\Gamma_2\vdash M:\sigma.

Lemma(Subterm): If MM is a legal term, then all subterms of MM are also legal terms.

Lemma(Uniqueness): If ΓM:σ\Gamma\vdash M:\sigma and ΓM:τ\Gamma\vdash M:\tau, then στ\sigma\equiv\tau.

Definition(β-Reduction) (only for legal terms)

  • Basis: (λx:σ.M)  NβM[x:=N](\lambda x:\sigma.M)\;N\rightarrow_\beta M[x:=N].
  • Compatibility: If MβNM\rightarrow_\beta N, then M  LβN  LM\;L\rightarrow_\beta N\;L, L  MβL  NL\;M\rightarrow_\beta L\; N and λx:σ.Mβλx:σ.N\lambda x:\sigma.M\rightarrow_\beta \lambda x:\sigma.N.

Lemma (Subject Reduction): If ΓM1:σ\Gamma\vdash M_1:\sigma and M1βM2M_1\rightarrow^*_\beta M_2, then ΓM2:σ\Gamma\vdash M_2:\sigma.

Theorem (Church-Rosser Theorem):

Let M,N1,N2ΛM,N_1,N_2\in\Lambda^\rightarrow be simply typed λ-terms with MβN1M\rightarrow^*_\beta N_1 and MβN2M\rightarrow^*_\beta N_2. Then there is a simply typed λ-term N3ΛN_3\in\Lambda^\rightarrow such that N1βN3N_1\rightarrow^*_\beta N_3 and N2βN3N_2\rightarrow^*_\beta N_3.

strongly/weakly normalizing and many steps reduction are just similar to untyped ones.

Theorem (Strong Normalization Theorem):

Every legal term in λ\lambda_\rightarrow is strongly normalizing.

Noticing that Self-application is not typable in λ\lambda_\rightarrow.

# The Extension λ2\lambda_2

Definition(The Set T2\mathbb{T}_2 of λ2\lambda_2 Types)

  • Variable Type: If αV\alpha\in\mathbb{V}, then αT2\alpha\in\mathbb{T}_2.
  • Arrow Type: If σ,τT2\sigma,\tau\in\mathbb{T}_2, then (στ)T2(\sigma\rightarrow\tau)\in\mathbb{T}_2.
  • Π\Pi-type: If αV\alpha\in\mathbb{V} and σT2\sigma\in\mathbb{T}_2, then (Πα:.σ)T2(\Pi\alpha:*.\sigma)\in\mathbb{T}_2.

Definition(The Set Λ2\Lambda_2 of Pre-Typed λ2\lambda_2-Terms)

  • Variable: If xVx\in V, then xΛ2x\in\Lambda_2.

  • Application: If M,NΛ2M,N\in\Lambda_2, then (M  N)Λ2(M\;N)\in\Lambda_2.

    ​ If MΛ2,σT2M\in\Lambda_2,\sigma\in\mathbb{T}_2, then (M  σ)Λ2(M\;\sigma)\in\Lambda_2.

  • Abstraction: If xV,σT2x\in V,\sigma\in\mathbb{T}_2 and MΛ2M\in\Lambda_2, then (λx:σ.M)Λ2(\lambda x:\sigma.M)\in\Lambda_2.

    ​ If σV,MΛ2\sigma\in\mathbb{V},M\in\Lambda_2 then (λσ:.M)Λ2(\lambda\sigma:*.M)\in\Lambda_2.

Definition(β-Reduction) (only for legal terms)

  • Basis: (λx:σ.M)  NβM[x:=N](\lambda x:\sigma.M)\;N\rightarrow_\beta M[x:=N].

    (λα:.M)  σβM[α:=σ](\lambda\alpha:*.M)\;\sigma\rightarrow_\beta M[\alpha:=\sigma].

  • Compatibility: If MβNM\rightarrow_\beta N, then M  LβN  LM\;L\rightarrow_\beta N\;L, L  MβL  NL\;M\rightarrow_\beta L\; N and λx:σ.Mβλx:σ.N\lambda x:\sigma.M\rightarrow_\beta \lambda x:\sigma.N.

Definition

  • A statement is of the form M:σM:\sigma, MM is called the subject and σ\sigma the type.
  • A term declaration is a statement x:σx:\sigma.
  • A type declaration is of the form σ:\sigma:*.
  • A context Γ\Gamma is a set of declarations with different subjects.
  • A judgement is of the form ΓM:σ\Gamma\vdash M:\sigma.
  • A term MM is called legal if there exists Γ\Gamma and σ\sigma such that ΓM:σ\Gamma\vdash M:\sigma.

Notice! In a valid λ2\lambda_2-context every type variable σ\sigma is declared (σ:)(\sigma:*) before it is used (M:σ)(M:\sigma).

Derivation Rules:

Γx:σif  x:σΓ(var)ΓM:στΓN:σΓM  N:τ(appl)Γ,x:σM:τΓλx:σ.M:στ(abst)ΓB:if  BT2  and  all  free  type  variables  inB  are  declared  in  Γ(form)Γ,α:M:AΓ(λα:.M):(Πα:.A)(abst2)ΓM:(Πα:.A)ΓB:ΓM  B:A[α:=B](appl2)\Gamma\vdash x:\sigma\quad if\;x:\sigma\in\Gamma\quad(var)\\ \frac{\Gamma\vdash M:\sigma\rightarrow\tau\quad\Gamma\vdash N:\sigma}{\Gamma\vdash M\;N:\tau}\quad(appl)\\ \frac{\Gamma,x:\sigma\vdash M:\tau}{\Gamma\vdash\lambda x:\sigma.M:\sigma\rightarrow\tau}\quad(abst)\\ \Gamma\vdash B:*\quad if\; B\in\mathbb{T}_2\;and\;all\;free\;type\;variables\;in\\ B\;are\;declared\;in\;\Gamma\quad(form)\\ \frac{\Gamma,\alpha:*\vdash M:A}{\Gamma\vdash(\lambda\alpha:*.M):(\Pi\alpha:*.A)}\quad(abst_2)\\ \frac{\Gamma\vdash M:(\Pi\alpha:*.A)\quad\Gamma\vdash B:*}{\Gamma\vdash M\;B:A[\alpha:=B]}\quad(appl_2)

Definition(Type of Church Numerals)

CΠα:.(αα)αα\mathcal{C}\equiv\Pi\alpha:*.(\alpha\rightarrow\alpha)\rightarrow\alpha\rightarrow\alpha

Definition(Pair of Church Numerals)

M,Nλz:CCC.z  M  N:(CCC)Cpair(CCC)Cfstλp:pair.p  (λx:C.λy:C.x)sndλp:pair.p  (λx:C.λy:C.y)\langle M,N\rangle\equiv\lambda z:\mathcal{C}\rightarrow\mathcal{C}\rightarrow\mathcal{C}.z\;M\;N:(\mathcal{C}\rightarrow\mathcal{C}\rightarrow\mathcal{C})\rightarrow\mathcal{C}\\ pair\equiv(\mathcal{C}\rightarrow\mathcal{C}\rightarrow\mathcal{C})\rightarrow\mathcal{C}\\ fst\equiv\lambda p:pair.p\;(\lambda x:\mathcal{C}.\lambda y:\mathcal{C}.x)\\ snd\equiv\lambda p:pair.p\;(\lambda x:\mathcal{C}.\lambda y:\mathcal{C}.y)

Now we can reconsider the factorial function:

next  n,fact  nn+1,fact  n+1next\;\langle n,fact\;n\rangle\rightarrow\langle n+1,fact\;n+1\rangle

where

next=λp:pair.succ  (fst  p),mult  (succ  (fst  p))  (snd  p)next:pairpairnext=\lambda p:pair.\langle succ\;(fst\;p),mult\;(succ\;(fst\;p))\;(snd\;p)\rangle\\ next:pair\rightarrow pair

So n,fact(n)=βnextn  0,1\langle n,fact(n)\rangle=_\beta next^n\;\langle 0,1\rangle. It comes back to the form:

λα:.λf:αα.λx:α.fn  x:Πα:.(αα)αα\lambda\alpha:*.\lambda f:\alpha\rightarrow\alpha.\lambda x:\alpha.f^n\;x:\Pi\alpha:*.(\alpha\rightarrow\alpha)\rightarrow\alpha\rightarrow\alpha

What’s interesting, the type is church numerical type! so

cn  pair  next  0,1=βcn,fact  cnc_n\;pair\;next\;\langle 0,1\rangle=_\beta\langle c_n,fact\;c_n\rangle

where cnc_n is church numerical. So

factλn:C.snd  (n  pair  next  0,1):CCfact\equiv \lambda n:\mathcal{C}.snd\;(n\;pair\;next\;\langle 0,1\rangle):\mathcal{C}\rightarrow\mathcal{C}

Church numbers can represent loop somehow.

# The Extension λω\lambda\underline{\omega} (Lambda Weak Omega)

Definition(The Set K\mathbb{K} of All Kinds)

K=    (KK)\mathbb{K}=*\;|\;(\mathbb{K}\rightarrow\mathbb{K}).

term:type:kind:sort:term:type:kind:sort:\Box.

Noticing that λω\lambda\underline{\omega} doesn’t support polymorphism, as a matter of fact, such type Πα:.α\Pi\alpha:*.\alpha is illegal.

However, if we want to combine polymorphism into lambda weak omega, we need to noticing the difference between *\rightarrow * and Πα:,αα\Pi\alpha:*,\alpha\rightarrow\alpha:

we can write:

(λα:.λx:α.x):(Πα:.αα):(\lambda\alpha:*.\lambda x:\alpha.x):(\Pi\alpha:*.\alpha\rightarrow\alpha):*

since Πα:.αα\Pi\alpha:*.\alpha\rightarrow \alpha is a specific type, so its kind is *.

while λα:.αα:\lambda\alpha:*.\alpha\rightarrow\alpha:*\rightarrow *, it’s considered as the type constructor.

(λα:.λx:α.x):(λα:.αα)(\lambda \alpha:*.\lambda x:\alpha.x):(\lambda \alpha:*.\alpha\rightarrow\alpha) is wrong!

(λα:.λx:α.x):(\lambda \alpha:*.\lambda x:\alpha.x):*\rightarrow * is wrong!

Derivation Rules:

:(sort)ΓA:sΓ,x:Ax:Aif  xΓ(var)ΓA:BΓC:sΓ,x:CA:Bif  xΓ(weak)ΓA:sΓB:sΓAB:s(form)ΓM:ABΓN:AΓM  N:B(appl)Γ,x:AM:BΓAB:sΓλx:A.M:AB(abst)ΓA:BΓB:sΓA:Bif  B=βB(conv)\empty\vdash *:\Box\quad(sort)\\ \frac{\Gamma\vdash A:s}{\Gamma,x:A\vdash x:A}if\;x\notin\Gamma\quad(var)\\ \frac{\Gamma\vdash A:B\quad\Gamma\vdash C:s}{\Gamma,x:C\vdash A:B}if\;x\notin\Gamma\quad (weak)\\ \frac{\Gamma\vdash A:s\quad\Gamma\vdash B:s}{\Gamma\vdash A\rightarrow B:s}\quad(form)\\ \frac{\Gamma\vdash M:A\rightarrow B\quad \Gamma\vdash N:A}{\Gamma\vdash M\;N:B}\quad(appl)\\ \frac{\Gamma,x:A\vdash M:B\quad\Gamma\vdash A\rightarrow B:s}{\Gamma\vdash \lambda x:A.M:A\rightarrow B}\quad (abst)\\ \frac{\Gamma\vdash A:B\quad \Gamma\vdash B':s}{\Gamma\vdash A:B'}if\;B=_\beta B'\quad(conv)

L1 L2 L3 L4
λx:α.x\lambda x:\alpha.x(terms) αα\alpha\rightarrow\alpha(type) *(kind) \Box(sort)
λα:.α\lambda \alpha:*.\alpha(type constructor) *\rightarrow *(kind) \Box(sort)

The derivation rules seem strange in that the only axiom is :*:\Box, which is the relation between L3 and L4.

And we can derive:

:σ:σ:(var)\frac{\empty\vdash *:\Box}{\sigma:*\vdash\sigma:*}\quad(var)

it’s the relation between L2 and L3.

And we can derive:

σ:σ:σ:,x:σx:σ(var)\frac{\sigma:*\vdash\sigma:*}{\sigma:*,x:\sigma\vdash x:\sigma}\quad (var)

it’s the relation between L1 and L2.

So we can discover that the derivation rule var can be applied between any two adjacent layers.

Similarly, In weak derivation rule, xx can be types or terms.

In form rules, AA can be types or kinds.

In appl rules, MM can be terms or type constructors.

In abst rules, AA can be types or kinds.

Γσ:\Gamma \vdash\sigma:* means σ\sigma is a well-formed type. Γλα:.α:\Gamma\vdash\lambda \alpha:*.\alpha:*\rightarrow * means λα:.α\lambda \alpha:*.\alpha is a well-formed type constructor. Γ:\Gamma\vdash *\rightarrow *:\Box means *\rightarrow * is a well-formed kind.

# The Extension λP\lambda_P (Lambda P)

Derivation Rules:

:(sort)ΓA:sΓ,x:Ax:Aif  xΓ(var)ΓA:BΓC:sΓ,x:CA:Bif  xΓ(weak)ΓA:Γ,x:AB:sΓΠx:A.B:s(form)ΓM:Πx:A.BΓN:AΓM  N:B[x:=N](appl)Γ,x:AM:BΓAB:sΓλx:A.M:AB(abst)ΓA:BΓB:sΓA:Bif  B=βB(conv)\empty\vdash *:\Box\quad(sort)\\ \frac{\Gamma\vdash A:s}{\Gamma,x:A\vdash x:A}if\;x\notin\Gamma\quad(var)\\ \frac{\Gamma\vdash A:B\quad\Gamma\vdash C:s}{\Gamma,x:C\vdash A:B}if\;x\notin\Gamma\quad (weak)\\ \frac{\Gamma\vdash A:*\quad\Gamma,x:A\vdash B:s}{\Gamma\vdash\Pi x:A.B:s}\quad(form)\\ \frac{\Gamma\vdash M:\Pi x:A.B\quad \Gamma\vdash N:A}{\Gamma\vdash M\;N:B[x:=N]}\quad(appl)\\ \frac{\Gamma,x:A\vdash M:B\quad\Gamma\vdash A\rightarrow B:s}{\Gamma\vdash \lambda x:A.M:A\rightarrow B}\quad (abst)\\ \frac{\Gamma\vdash A:B\quad \Gamma\vdash B':s}{\Gamma\vdash A:B'}if\;B=_\beta B'\quad(conv)

# Propositions as Types

PAT: Propositions As Types and Proofs As Terms

M:σM:\sigma, MM corresponds to a proof and σ\sigma corresponds to a proposition.

σ\sigma is inhabited \Leftrightarrow PP is proved.