Permissive nominal terms - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Reports (Research Report) Year : 2008

Permissive nominal terms

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.
Fichier principal
Vignette du fichier
RR-6682.pdf (271.73 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00335115 , version 1 (28-10-2008)

Identifiers

  • HAL Id : inria-00335115 , version 1

Cite

Gilles Dowek, Murdoch Gabbay, Dominic Mulligan. Permissive nominal terms. [Research Report] RR-6682, INRIA. 2008. ⟨inria-00335115⟩
305 View
68 Download

Share

Gmail Facebook X LinkedIn More