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 := \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 \[T_1 \to T_2\] for any abstraction \[\lambda x.M\] where
\[x\] has a type is \[T_1\] and \[M\] has a type is \[T_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:
\[ \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 \[x\] binds to type \[T\] in context \[\Gamma\] is truth. We can make a conclusion, in context \[\Gamma\], we can judge the type of \[x\] is \[T\].
- T-Abstraction: with the premise, with context \[\Gamma\] and term \[x\] binds to type \[T_1\] we can judge term \[t_2\] has type \[T_2\]. We can make a conclusion, in context \[\Gamma\], we can judge the type of \[\lambda x:T_1.t_2\] is \[T_1 \to T_2\].
- T-Application: with the premise, with context \[\Gamma\] and term \[t_1\] binds to type \[T_1 \to T_2\] and with context \[\Gamma\] we can judge term \[t_2\] has type \[T_1\]. We can make a conclusion, in context \[\Gamma\], we can judge the type of \[t_1 \; t_2\] is \[T_2\].