inria-00335115, version 1
Permissive nominal terms
Gilles Dowek
1Murdoch Gabbay 2Dominic Mulligan a, 2
N° RR-6682 (2008)
Résumé : We present a simplified version of nominal terms with improved properties. Nominal terms are themselves a version of first-order terms, adapted to provide primitive support for names, binding, capturing substitution, and alpha-conversion. Nominal terms lack certain properties of first-order terms; it is always possible to 'choose a fresh variable symbol' for a first-order term and it is always possible to 'alpha-convert a bound variable symbol to a fresh symbol'. This is not the case for nominal terms. Permissive nominal terms preserve the flavour and the basic theory of nominal terms, including two levels of variable symbol, freshness, and permutation - but they recover the 'always fresh' and 'always alpha-rename' properties of first- and higher-order syntax, and they simplify the theory by eliding freshness contexts and by supporting a notion of term-unifier based on substitution alone, rather than the nominal terms' substitution and freshness conditions. No expressivity is lost moving to the permissive case.
- a – Heriot Watt
- 1 : Laboratoire d'informatique de l'école polytechnique (LIX)
- CNRS : UMR7161 – Polytechnique - X
- 2 : School of Mathematics and Computer Science
- Heriot-Watt University
- Domaine : Informatique/Logique en informatique
- Mots-clés : Unification algorithms – nominal techniques – permissive nominal terms
- Référence interne : RR-6682
- inria-00335115, version 1
- http://hal.inria.fr/inria-00335115
- oai:hal.inria.fr:inria-00335115
- Contributeur : Gilles Dowek
- Soumis le : Mardi 28 Octobre 2008, 15:04:36
- Dernière modification le : Lundi 17 Novembre 2008, 10:59:54






Documents associés

Exporter