Deciding simply-typed equivalence with sums and the empty type
Gabriel Scherer
Parsifal team at INRIA Saclay
http://gallium.inria.fr/~scherer/
Date(s) : 26/01/2017 iCal
11h00 - 12h00
The simply-typed λ-calculus, with only function types, is strongly normalizing, and its program equivalence relation is decidable: unlike in more advanced type system with polymorphism or effects, the natural « syntactic » equivalence (βη-equivalence) corresponds to natural « semantic » equivalence (observational or contextual equivalence), and is decidable. Adding product types (pairs) is easy and preserves these properties, but sums (disjoint unions) are, surprisingly, harder. It is only in 1995 that Neil Ghani proved that the equivalence in presence of sums is decidable, and the situation in presence of the empty type (zero-ary sum) was unknown.
We propose an equivalence algorithm for sums and the empty type that takes inspiration from a proof-theoretic technique, named « focusing »,designed for proof search. The exposition will be introductory; I will present the difficulties caused by sums and the empty type, present some of the existing approaches for sums in the literature, introduce focusing, and give a high-level intuition of our saturation-based algorithm and its termination argument.
Catégories
