Permissive nominal terms

Gilles Dowek 1, 2 Murdoch Gabbay 3 Dominic Mulligan 3
1 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : 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.
Type de document :
Rapport
[Research Report] RR-6682, INRIA. 2008
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00335115
Contributeur : Gilles Dowek <>
Soumis le : mardi 28 octobre 2008 - 15:04:36
Dernière modification le : mercredi 25 avril 2018 - 10:45:26
Document(s) archivé(s) le : lundi 7 juin 2010 - 22:24:01

Fichiers

RR-6682.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00335115, version 1

Collections

Citation

Gilles Dowek, Murdoch Gabbay, Dominic Mulligan. Permissive nominal terms. [Research Report] RR-6682, INRIA. 2008. 〈inria-00335115〉

Partager

Métriques

Consultations de la notice

530

Téléchargements de fichiers

70