4

NOTE: simply typed lambda calculus

 2 years ago
source link: https://dannypsnl.github.io/blog/2020/03/08/cs/note-stlc/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
neoserver,ios ssh client

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.ms(nsz)add := \lambda m. \lambda n. \lambda s. \lambda z. m\;s\;(n\;s\;z)add:=λm.λn.λs.λz.ms(nsz)

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 λ→\lambda \toλ→ system(a.k.a. simply typed lambda calculus). It gets name λ→\lambda \toλ→ is because it introduces one new type: Arrow type, represent as T1→T2T_1 \to T_2T1​→T2​ for any abstraction λx.M\lambda x.Mλx.M where xxx has a type is T1T_1T1​ and MMM has a type is T2T_2T2​. 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:TT−VariableΓ,x:T1⊢t2:T2Γ⊢λx:T1.t2:T1→T2T−AbstractionΓ,t1:T1→T2Γ⊢t2:T1Γ⊢t1t2:T2T−Application\frac{ x:T \in \Gamma }{ \Gamma \vdash x:T } \;\;\;\; T-Variable \\ \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 \\ \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Γ⊢x:Tx:T∈Γ​T−VariableΓ⊢λx:T1​.t2​:T1​→T2​Γ,x:T1​⊢t2​:T2​​T−AbstractionΓ⊢t1​t2​:T2​Γ,t1​:T1​→T2​Γ⊢t2​:T1​​T−Application

Here is explaination:

  • T-Variable: with the premise, term xxx binds to type TTT in context Γ\GammaΓ is truth. We can make a conclusion, in context Γ\GammaΓ, we can judge the type of xxx is TTT.
  • T-Abstraction: with the premise, with context Γ\GammaΓ and term xxx binds to type T1T_1T1​ we can judge term t2t_2t2​ has type T2T_2T2​. We can make a conclusion, in context Γ\GammaΓ, we can judge the type of λx:T1.t2\lambda x:T_1.t_2λx:T1​.t2​ is T1→T2T_1 \to T_2T1​→T2​.
  • T-Application: with the premise, with context Γ\GammaΓ and term t1t_1t1​ binds to type T1→T2T_1 \to T_2T1​→T2​ and with context Γ\GammaΓ we can judge term t2t_2t2​ has type T1T_1T1​. We can make a conclusion, in context Γ\GammaΓ, we can judge the type of t1t2t_1 \; t_2t1​t2​ is T2T_2T2​.

report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK