NOTE: simply typed lambda calculus

Dan's
Blog

Programming Language Theory • System Programming

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 λ\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 T1T2T_1 \to T_2 for any abstraction λx.M\lambda x.M where xx has a type is T1T_1 and MM has a type is T2T_2. 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Γ,x:T1t2:T2Γλx:T1.t2:T1T2        TAbstractionΓ,t1:T1T2  Γt2:T1Γt1  t2:T2        TApplication\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

Here is explaination:

  • T-Variable: with the premise, term xx binds to type TT in context Γ\Gamma is truth. We can make a conclusion, in context Γ\Gamma, we can judge the type of xx is TT.
  • T-Abstraction: with the premise, with context Γ\Gamma and term xx binds to type T1T_1 we can judge term t2t_2 has type T2T_2. We can make a conclusion, in context Γ\Gamma, we can judge the type of λx:T1.t2\lambda x:T_1.t_2 is T1T2T_1 \to T_2.
  • T-Application: with the premise, with context Γ\Gamma and term t1t_1 binds to type T1T2T_1 \to T_2 and with context Γ\Gamma we can judge term t2t_2 has type T1T_1. We can make a conclusion, in context Γ\Gamma, we can judge the type of t1  t2t_1 \; t_2 is T2T_2.

author: Lîm Tsú-thuàn/林子篆/Danny

category:cs

tag:notepltstlc

Similar Articles

Buy Me A CoffeeCreative Commons Attribution-NonCommercial-NoDerivatives 4.0 InternationalAll works in this site is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
©2021 dannypsnl(林子篆)