Important Results
- Tait showed in 1967 that -reduction is strongly normalizing. As a corollary -equivalence is decidable. Statman showed in 1977 that the normalisation problem is not elementary recursive. A purely semantic normalisation proof (see normalisation by evaluation) was given by Berger and Schwichtenberg in 1991.
- The unification problem for -equivalence is undecidable. Huet showed in 1973 that 3rd order unification is undecidable and this was improved upon by Baxter in 1978 then by Goldfarb in 1981 by showing that 2nd order unification is already undecidable. Whether higher order matching (unification where only one term contains existential variables) is decidable is still open.
- We can encode natural numbers by terms of the type (Church numerals). Schwichtenberg showed in 1976 that in exactly the extended polynomials are representable as functions over Church numerals; these are roughly the polynomials closed up under a conditional operator.
- A full model of is given by interpreting base types as sets and function types by the set-theoretic function space. Friedman showed in 1975 that this interpretation is complete for -equivalence, if the base types are interpreted by infinite sets. Statman showed in 1983 that -equivalence is the maximal equivalence which is typically ambiguous, i.e. closed under type substitutions (Statman's Typical Ambiguity Theorem). A corollary of this is that the finite model property holds, i.e. finite sets are sufficient to distinguish terms which are not identified by -equivalence.
- Plotkin introduced logical relations in 1973 to characterize the elements of a model which are definable by lambda terms. In 1993 Jung and Tiuryn showed that a general form of logical relation (Kripke logical relations with varying arity) exactly characterizes lambda definability. Plotkin and Statman conjectured that it is decidable whether a given element of a model generated from finite sets is definable by a lambda term (Plotkin-Statman-conjecture). The conjecture was shown to be false by Loader in 1993.
Read more about this topic: Simply Typed Lambda Calculus
Famous quotes containing the words important and/or results:
“Acknowledging separation feelings directly and sympathetically is the best way of coping with them. It is actually helpful to tell a toddler “I’ll miss you,” or “I will think of you during the day,” or “It is hard to say goodbye,” or “I can’t wait to see you at the end of the day.” These messages tell the child that he is important to the parent even when they are not together and that out of sight need not mean out of mind.”
—Alicia F. Lieberman (20th century)
“Different persons growing up in the same language are like different bushes trimmed and trained to take the shape of identical elephants. The anatomical details of twigs and branches will fulfill the elephantine form differently from bush to bush, but the overall outward results are alike.”
—Willard Van Orman Quine (b. 1908)