A quantitative model for simply typed lambda-calculus

Hofmann, Martin und Ledent, Jeremy (2022): A quantitative model for simply typed lambda-calculus. In: Mathematical Structures in Computer Science, Bd. 32, Nr. 6, PII S0960129521000256: S. 777-793

Abstract

We use a simplified version of the framework of resource monoids, introduced by Dal Lago and Hofmann, to interpret simply typed lambda-calculus with constants zero and successor. We then use this model to prove a simple quantitative result about bounding the size of the normal form of lambda-terms. While the bound itself is already known, this is to our knowledge the first semantic proof of this fact. Our use of resource monoids differs from the other instances found in the literature, in that it measures the size of lambda-terms rather than time complexity.

• Dokumententyp: Zeitschriftenartikel
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISSN: 0960-1295
• Sprache: Englisch