A Complete Normal-Form Bisimilarity for State
Résumé
We present a sound and complete bisimilarity for an untyped \(\lambda \)-calculus with higher-order local references. Our relation compares values by applying them to a fresh variable, like normal-form bisimilarity, and it uses environments to account for the evolving store. We achieve completeness by a careful treatment of evaluation contexts comprising open stuck terms. This work improves over Stovring and Lassen’s incomplete environment-based normal-form bisimilarity for the \(\lambda \rho \)-calculus, and confirms, in relatively elementary terms, Jaber and Tabareau’s result, that the state construct is discriminative enough to be characterized with a bisimilarity without any quantification over testing arguments.
Nous définissons une bisimilarité correcte et complète pour un λ-calcul non typé avec des références locales d’ordre supérieur. Notre relation compare les valeurs en leur passant comme argument une variable fraîche, comme la bisimilarité de forme normale, et utilise des environnements pour prendre en compte l’ évolution de la mémoire. Nous obtenons la complétude par un traîtement méticuleux des contextes d’ évaluation qui englobent les termes bloqués.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...