Polarised intermediate representation of lambda calculus with sums

authors: Guillaume Munch-Maccagnoni, Gabriel Scherer
year: 2015
url: http://dx.doi.org/10.1109/LICS.2015.22
publisher: IEEE
abstract: The theory of the λ-calculus with extensional sums is more complex than with only pairs and functions. We propose an untyped representation-an intermediate calculus-for the λ-calculus with sums, based on the following principles: 1) Computation is described as the reduction of pairs of an expression and a context; the context must be represented inside-out, 2) operations are represented abstractly by their transition rule, 3) Positive and negative expressions are respectively eager and lazy; this polarity is an approximation of the type. We offer an introduction from the ground up to our approach, and we review the benefits. A structure of alternating phases naturally emerges through the study of normal forms, offering a reconstruction of focusing. Considering further purity assumption, we obtain maximal multifocusing. As an application, we can deduce a syntax-directed algorithm to decide the equivalence of normal forms in the simply-typed λ-calculus with sums, and justify it with our intermediate calculus.