DEV Community

林子篆
林子篆

Posted on • Originally published at dannypsnl.github.io on

NOTE: simply typed lambda calculus

Last time I introduce lambda calculus.Lambda calculus is powerful enough for computation. But it’s not good enough for people, compare with below Church Numerals

add:=λm.λn.λs.λz.m  s  (n  s  z) add := \lambda m. \lambda n. \lambda s. \lambda z. m\;s\;(n\;s\;z)

people prefer just + more.

But once we introduce such fundamental operations into the system, validation would be a thing. This is the main reason to have a λ→ system(a.k.a. simply typed lambda calculus). It gets name λ→ is because it introduces one new type: Arrow type, represent as T1→T2 for any abstraction λx.M where x has a type is T1 and M has a type is T2. Therefore we can limit the input to a specified type, without considering how to add two Car together!

To represent this, syntax needs a little change:

term ::= terms
  x variable
  λx: T.term abstraction
  term term application
Enter fullscreen mode Exit fullscreen mode

Abstraction now can describe it’s parameter type. Then we have typing rules:

x:TΓΓx:T        TVariable \frac{ x:T \in \Gamma }{ \Gamma \vdash x:T } \;\;\;\; T-Variable
Γ,x:T1t2:T2Γλx:T1.t2:T1T2        TAbstraction \frac{ \Gamma, x:T_1 \vdash t_2: T_2 }{ \Gamma \vdash \lambda x:T_1.t_2 : T_1 \to T_2 } \;\;\;\; T-Abstraction
Γ,t1:T1T2  Γt2:T1Γt1  t2:T2        TApplication \frac{ \Gamma, t_1:T_1 \to T_2 \; \Gamma \vdash t_2: T_1 }{ \Gamma \vdash t_1 \; t_2 : T_2 } \;\;\;\; T-Application

Here is the explanation:

  • T-Variable: with the premise, term x binds to type T in context Γ is truth. We can make a conclusion, in context Γ, we can judge the type of x is T.
  • T-Abstraction: with the premise, with context Γ and term x binds to type T1 we can judge term t2 has type T2. We can make a conclusion, in context Γ, we can judge the type of λx:T1.t2 is T1→T2.
  • T-Application: with the premise, with context Γ and term t1 binds to type T1→T2 and with context Γ we can judge term t2 has type T1. We can make a conclusion, in context Γ, we can judge the type of t1t2 is T2.

Top comments (1)

Collapse
 
dannypsnl profile image
林子篆

Unfortunately, this kind of article with so many latex symbols, post it to dev.to is so hard. 😭