Abstract: Lambda calculi with algebraic data types lie at the core of functional programming languages and proof assistants, but conceal at least two fundamental theoretical problems already in the presence of the simplest non-trivial data type, the sum type. First, we do not know of an explicit and implemented algorithm for deciding the beta-eta-equality of terms—-and this in spite of the first decidability results proven two decades ago. Second, it is not clear how to decide when two types are essentially the same, i.e. isomorphic, in spite of the meta-theoretic results on decidability of the isomorphism.
In this paper, we present the exp-log normal form of types—-derived from the representation of exponential polynomials via the unary exponential and logarithmic functions—-that any type built from arrows, products, and sums, can be isomorphically mapped to. The type normal form can be used as a simple heuristic for deciding type isomorphism, thanks to the fact that it is a systematic application of the high-school identities.
We then show that the type normal form allows to reduce the standard beta-eta equational theory of the lambda calculus to a specialized version of itself, while preserving the completeness of equality on terms. We end by describing an alternative representation of normal terms of the lambda calculus with sums, together with a Coq-implemented converter into/from our new term calculus. The difference with the only other previously implemented heuristic for deciding interesting instances of eta-equality by Balat, Di Cosmo, and Fiore, is that we exploit the type information of terms substantially and this often allows us to obtain a canonical representation of terms without performing sophisticated term analyses.
Abstract: Logical incarnations of type isomorphism include the notions of constructive cardinality of sets and strong intuitionistic equivalence of formulas. These are challenging to study in simultaneous presence of functions (exponentials) and sums (disjoint unions, disjunction). In this talk, I will present a quasi-normal form of types that arises from the decomposition of binary exponentiation into the unary exponentiation and logarithm. This normal form can be applied for disentangling the equational theory (beta-eta) of the lambda calculus with sums. By an extension of the normal form from simple types (propositional logic) to quantifiers, one can also retrieve an “arithmetical” hierarchy for intuitionistic first order logic. Finally, this suggests a sequent calculus for intuitionistic logic that uses the notation of exponential polynomials and removes the need for most of the invertible proof rules of usual sequent calculi.
In presence of sum types, the lambda calculus does not enjoy uniqueness of eta-long normal forms. The canonicity
problem also appears for proof trees of intuitionistic logic. In
this talk, I will show how the problem becomes easier if, before
choosing a canonical representative from a class of
beta-eta-equal terms, one coerces the term into the exp-log
normal form of its type. This type normal form arises from the
one for exponential polynomials.
On March 9, I am giving a talk at the Gallium seminar. Abstract: In this talk, I will present some recent results from Proof
Theory that might also be interesting to Programming Languages Theory.
First, I will present work on isomorphisms of types in presence of sums,
as well as the implications for canonicity of eta-long normal forms of
lambda calculus with sums. Second, I will show how one can use a
normalization-by-evaluation proof (written in CPS style) to compile away
control operators from System T; this could be used as a compiler
technique for a side-effect-free fragment of a program.
On January 21st, I am giving a talk at GdT Théorie des types et réalisabilité. Abstract: The traditional method to extract programs from proofs of classical Analysis (Peano Arithmetic + Axiom of Choice) is to use an extension of Gödel's System T with bar recursion. An alternative method is to use an approach based on computational side-effects (control operators, quote/clock instructions) like in the works of Krivine or Herbelin. By classic results of Kreisel and Schwichtenberg, for the fragment of Analysis that makes sense computationally, the Π₂-fragment, we know that bar recursion is essentially primitive recursive — leaving open the question of how to actually avoid using it. In this talk, I will present some recent work (http://arxiv.org/abs/1301.5089) showing how realizers of System T can be extracted directly from proofs of the Σ₂-fragment of classical Analysis. Control operators are essential, but only at the meta-theoretical level: control operators can be compiled away from System T, at any simple type.