Deciding simply-typed equivalence with sums and the empty type

Carte non disponible

Date/heure
Date(s) - 26/01/2017
11 h 00 min - 12 h 00 min

Catégories Pas de Catégories


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.

http://gallium.inria.fr/~scherer/

Olivier CHABROL
Posts created 14

Deciding simply-typed equivalence with sums and the empty type

Carte non disponible

Date/heure
Date(s) - 26/01/2017
11 h 00 min - 12 h 00 min

Catégories Pas de Catégories


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.

http://gallium.inria.fr/~scherer/

Olivier CHABROL
Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange