LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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.