Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:simply_typed_lambda_calculus [2008/10/13 08:27] vkuncak |
sav08:simply_typed_lambda_calculus [2009/03/05 12:32] vkuncak |
||
|---|---|---|---|
| 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. | ||