We introduce a simple extension of the calculus with pairs—called the distributive calculus—obtained by adding a computational interpretation of the valid distributivity isomorphism of simple types. We study the calculus both as an untyped and as a simply typed setting. Key features of the untyped calculus are confluence, the absence of clashes of constructs, that is, evaluation never gets stuck, and a leftmost-outermost normalization theorem, obtained with straightforward proofs. With respect to simple types, we show that the new rules satisfy subject reduction if types are considered up to the distributivity isomorphism. The main result is strong normalization for simple types up to distributivity. The proof is a smooth variation over the one for the calculus with pairs and simple types.
CITATION STYLE
Accattoli, B., & Díaz-Caro, A. (2020). Functional Pearl: The Distributive$$\lambda $$ -Calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12073 LNCS, pp. 33–49). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-59025-3_3
Mendeley helps you to discover research relevant for your work.