# Functional Pearl: The Distributive $\lambda$-Calculus

1 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We introduce a simple extension of the $\lambda$-calculus with pairs—called the distributive $\lambda$-calculus—obtained by adding a computational interpretation of the valid distributivity isomorphism A⇒(B∧C) ≡ (A⇒B)∧(A⇒C) 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 straight forward 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.
Keywords :
Document type :
Conference papers

https://hal.inria.fr/hal-03089254
Contributor : Beniamino Accattoli Connect in order to contact the contributor
Submitted on : Monday, December 28, 2020 - 11:13:21 AM
Last modification on : Wednesday, November 3, 2021 - 9:54:27 AM

### Citation

Beniamino Accattoli, Alejandro Díaz-Caro. Functional Pearl: The Distributive $\lambda$-Calculus. FLOPS 2020 - 15th International Symposium on Functional and Logic Programming, Sep 2020, Akita, Japan. pp.33-49, ⟨10.1007/978-3-030-59025-3_3⟩. ⟨hal-03089254⟩

Record views