DEV Community

loading...

NOTE: simply typed lambda calculus

林子篆
I am a programming language theory lover; good at system software like Networking, OS.
Originally published at dannypsnl.github.io on ・2 min read

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

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.

Discussion (1)

Collapse
dannypsnl profile image
林子篆 Author

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