Normalization by realizability also evaluates
Résumé
For those of us that generally live in the world of syntax, semantic
proof methods such as realizability or logical relations /
parametricity sometimes feel like magic. Why do they work? At which
point in the proof is "the real work" done?
Bernardy and Lasson express realizability and parametricity models as
syntactic model -- but the abstraction/adequacy theorems are still
explained as meta-level proofs. Hoping to better understand the proof
technique, we look at those theorems as programs themselves. How does
a normalization proof using realizability actually computes those
normal forms?
This detective work is an early stage and we propose a first attempt
in a simple setting. Instead of arbitrary Pure Type Systems, we use
the minimal negative propositional logic (arrows only). Instead of
starting from the simply-typed lambda-calculus, we work on
sequent-style terms in a simple subset of the Curien-Herbelin
L calculus.
Pour ceux d'entre nous qui vivent dans le monde de la syntaxe, les techniques de preuve sémantiques, comme la réalisabilité, les relations logiques ou la paramétricité ont parfois un arrière-goût de méthode magique. Pourquoi fonctionnent-elles ? Quel est le point clé de la preuve ? Bernardy et Lasson expriment la parametricité comme une construction de modèle syntaxique, par traduction bien typée, mais leurs théorèmes d'abstracion et adéquation restent des résultats au méta-niveau. Dans l'espoir de mieux comprendre ces résultats, nous étudiont leurs preuves comme des programmes. Les preuves de normalization par réalisabilité calculent-elles effectivement des formes normales, comment et à quel moment ? Ce travail de détective est encore à ses débuts, et nous proposons une première tentative dans un cadre très simple : au lieu de Pure Type Systems (PTS), nous utilisons le lambda-calcul simplement typé.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...