LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:simply_typed_lambda_calculus [2008/05/27 23:14]
vkuncak
sav08:simply_typed_lambda_calculus [2015/04/21 17:30] (current)
Line 4: Line 4:
   * foundation of modern functional programming languages (when extended with recursion)   * foundation of modern functional programming languages (when extended with recursion)
   * particularly suitable as a foundation of logic: due to termination properties   * particularly suitable as a foundation of logic: due to termination properties
 +
  
 ===== Simple Types ===== ===== Simple Types =====
Line 10: Line 11:
  
 The set of simple types are defined by grammar The set of simple types are defined by grammar
-\[ +\begin{equation*} 
-   \tau ::= \beta \mid (\tau \Rightarrow \tau) +   \tau ::= \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 28: 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 37: 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.
Line 47: Line 48:
  
 In some cases, such as $\lambda x.x$, there is an infinite family of possible concrete types. ​ In such cases, Hindley-Milner inference computes the most-general unifier of constraints,​ which gives polymorphic type.  For simplicity we assume that we have obtained some concrete types for variables and therefore for lambda terms. In some cases, such as $\lambda x.x$, there is an infinite family of possible concrete types. ​ In such cases, Hindley-Milner inference computes the most-general unifier of constraints,​ which gives polymorphic type.  For simplicity we assume that we have obtained some concrete types for variables and therefore for lambda terms.
 +
  
 ===== Strong Normalization ===== ===== Strong Normalization =====
  
-Unlike beta reduction on typed terms, beta reduction on typed terms always terminates and the result does not depend on the order of applying beta reductions in the term.  (Proof requires some work, and there are several variants; there are some short and elegant proofs that interpret based oset theory, see Barendregt'​s chapter.)+Unlike beta reduction on typed terms, beta reduction on typed terms always terminates and the result does not depend on the order of applying beta reductions in the term.  (Proof requires some work, and there are several variants; there are some short and elegant proofs that interpret based on set theory, see Barendregt'​s chapter.)
  
 The consequence is that for each term in simply typed lambda calculus we can compute a normal form where all beta reductions were applied. The consequence is that for each term in simply typed lambda calculus we can compute a normal form where all beta reductions were applied.