Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
verfasst von : Alexis Bernadet, Stéphane Lengrand
Erschienen in: Foundations of Software Science and Computational Structures
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present a typing system for the
λ
-calculus, with non-idempotent intersection types. As it is the case in (some) systems with idempotent intersections, a
λ
-term is typable if and only if it is strongly normalising. Non-idempotency brings some further information into typing trees, such as a bound on the longest
β
-reduction sequence reducing a term to its normal form.
We actually present these results in Klop’s extension of
λ
-calculus, where the bound that is read in the typing tree of a term is refined into an exact measure of the longest reduction sequence.
This complexity result is, for longest reduction sequences, the counterpart of de Carvalho’s result for linear head-reduction sequences.