Differences

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

--- sav08:simply_typed_lambda_calculus [2008/05/27 21:14]
vkuncak
+++ sav08:simply_typed_lambda_calculus [2008/05/27 23:08]
vkuncak
@@ Line 11: / Line 11: @@
 The set of simple types are defined by grammar
 \[
-   \tau ::= \beta \mid (\tau \doublerightarrow \tau)
+   \tau ::= \beta \mid (\tau \Rightarrow \tau)
 \]
 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).
 In simply typed lambda calculus, each variable is assigned one type from $\tau$.
@@ Line 32: / Line 33: @@
 \ \\
 \displaystyle
-\frac{t :: \tau}{(\lambda x.t) :: (\sigma \doublerightarrow \tau)} \mbox{ i{}f } {x \in V_\sigma} \\
+\frac{t :: \tau}{(\lambda x.t) :: (\sigma \Rightarrow \tau)} \mbox{ i{}f } {x \in V_\sigma} \\
 \ \\
 \displaystyle
-\frac{t_1 :: (\sigma \doublerightarrow \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}\]
+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 annotate e.g. term $\lambda x. x x$ to have concrete types in the simply typed system.
 ===== Hindley-Milner Type Inference =====