# 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**

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:

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$.

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

category:*cs*

tag:*note**plt**stlc*