s'authentifier
version française rss feed

inria-00335115, version 1

Permissive nominal terms

Gilles Dowek () 1, Murdoch Gabbay 2, Dominic Mulligan a2

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.

  • 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
  • oai:hal.inria.fr:inria-00335115
  • Contributeur : 
  • Soumis le : Mardi 28 Octobre 2008, 15:04:36
  • Dernière modification le : Lundi 17 Novembre 2008, 10:59:54
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...