کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
422262 | 685057 | 2016 | 18 صفحه PDF | دانلود رایگان |
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.
Journal: Electronic Notes in Theoretical Computer Science - Volume 323, 11 July 2016, Pages 57–74