Completeness in PVS of a Nominal Unification Algorithm

Nominal systems are an alternative approach for the treatment of variables in computational systems. In the nominal approach variable bindings are represented using techniques that are close to first-order logical techniques, instead of using a higher-order metalanguage. Functional nominal computation can be modelled through nominal rewriting, in which α-equivalence, nominal matching and nominal unification play an important role. Nominal unification was initially studied by Urban, Pitts and Gabbay and then formalised by Urban in the proof assistant Isabelle/HOL and by Kumar and Norrish in HOL4. In this work, we present a new specification of nominal unification in the language of PVS and a formalisation of its completeness. This formalisation is based on a natural notion of nominal α-equivalence, avoiding in this way the use of the intermediate auxiliary weak α-relation considered in previous formalisations. Also, in our specification, instead of applying simplification rules to unification and freshness constraints, we recursively build solutions for the original problem through a straightforward functional specification, obtaining a formalisation that is closer to algorithmic implementations. This is possible by the independence of freshness contexts guaranteed by a series of technical lemmas.