- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

sav08:simply_typed_lambda_calculus [2008/10/13 08:27] 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. | ||

Line 48: | 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. | ||