Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:simply_typed_lambda_calculus [2009/03/05 12:32] vkuncak |
sav08:simply_typed_lambda_calculus [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 11: | Line 11: | ||
The set of simple types are defined by grammar | The set of simple types are defined by grammar | ||
- | \[ | + | \begin{equation*} |
\tau ::= B \mid (\tau \Rightarrow \tau) | \tau ::= B \mid (\tau \Rightarrow \tau) | ||
- | \] | + | \end{equation*} |
The type $\tau_1 \doublerightarrow \tau_2$ is meant to denote functions from $\tau_1$ to $\tau_2$ (whether it denotes total or partial or computable functions, depends on particular semantics). | The type $\tau_1 \doublerightarrow \tau_2$ is meant to denote functions from $\tau_1$ to $\tau_2$ (whether it denotes total or partial or computable functions, depends on particular semantics). | ||
Line 29: | Line 29: | ||
Notation using type rules: | Notation using type rules: | ||
- | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
\displaystyle | \displaystyle | ||
\frac{}{x :: \tau}, \mbox{ i{}f } x \in V_\tau \\ | \frac{}{x :: \tau}, \mbox{ i{}f } x \in V_\tau \\ | ||
Line 38: | Line 38: | ||
\displaystyle | \displaystyle | ||
\frac{t_1 :: (\sigma \Rightarrow \tau),\ t_2 :: \sigma}{(t_1 t_2) :: \tau} | \frac{t_1 :: (\sigma \Rightarrow \tau),\ t_2 :: \sigma}{(t_1 t_2) :: \tau} | ||
- | \end{array}\] | + | \end{array}\end{equation*} |
Note that there is no way to assign a type to $x$ such that the term $\lambda x. x x$ is well typed. Therefore, $\lambda x.xx$ is not a term of simply typed lambda calculus. | Note that there is no way to assign a type to $x$ such that the term $\lambda x. x x$ is well typed. Therefore, $\lambda x.xx$ is not a term of simply typed lambda calculus. |