×

zbMATH — the first resource for mathematics

Completeness in PVS of a nominal unification algorithm. (English) Zbl 1394.68348
Benevides, Mario (ed.) et al., Proceedings of the 10th workshop on logical and semantic frameworks, with applications (LSFA 2015), Natal, Brazil, August 31 – September 1, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 323, 57-74 (2016).
Summary: 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 \(\alpha\)-equivalence, nominal matching and nominal unification play an important role. Nominal unification was initially studied by C. Urban et al. [Theor. Comput. Sci. 323, No. 1–3, 473–497 (2004; Zbl 1078.68140)] and then formalised by C. Urban [J. Autom. Reasoning 40, No. 4, 327–356 (2008; Zbl 1140.68061)] in the proof assistant Isabelle/HOL and by R. Kumar and M. Norrish [Lect. Notes Comput. Sci. 6172, 51–66 (2010; Zbl 1291.68356)] 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 \(\alpha\)-equivalence, avoiding in this way the use of the intermediate auxiliary weak \(\alpha\)-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.
For the entire collection see [Zbl 1342.68007].

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
68Q42 Grammars and rewriting systems
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aydemir, B.; Bohannon, A.; Weihrich, S., Nominal reasoning techniques in coq (extended abstract), Electronic Notes in Theoretical Computer Science, 174, 5, 69-77, (2007) · Zbl 1278.68248
[2] Avelar, A. B.; Galdino, A. L.; de Moura, F. L.C.; Ayala-Rincón, M., First-order unification in the PVS proof assistant, Logic Journal of the IGPL, 22, 5, 758-789, (2014)
[3] Ayala-Rincón, M.; Kamareddine, F., Unification via the λs e-style of explicit substitution, Logic Journal of the IGPL, 9, 4, 489-523, (2001) · Zbl 0987.03012
[4] Calvès, C., Unifying nominal unification, (24 th International Conference on Rewriting Techniques and Applications, RTA 2013, LIPIcs, vol. 21, (2013)), 143-157 · Zbl 1356.68119
[5] Calvès, C.; Fernández, M., The first-order nominal link, (Logic-Based Program Synthesis and Transformation - 20 th International Symposium, LOPSTR 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6564, (2010), Springer), 234-248 · Zbl 1326.68083
[6] Cheney, J., Relating nominal and higher-order pattern unification, (Proceedings of the 19 th International Workshop on Unification (UNIF 2005), (2005)), 104-119
[7] Constable, R.; Moczydlowski, W., Extracting the resolution algorithm from a completeness proof for the propositional calculus, Annals of Pure and Applied Logic, 161, 3, 337-348, (2009) · Zbl 1221.03015
[8] Dowek, G.; Hardin, T.; Kirchner, C., Higher-order unification via explicit substitutions, Information and Computation, 157, 1/2, 183-235, (2000) · Zbl 1005.03016
[9] Fernández, M.; Gabbay, M. J., Nominal rewriting, Information and Computation, 205, 6, 917-965, (June 2007)
[10] Fernández, M.; Rubio, A., Nominal completion for rewrite systems with binders, (Automata, Languages, and Programming, 39th International Colloquium, ICALP 2012, Lecture Notes in Computer Science, vol. 7392, (2012)), 201-213, Part II · Zbl 1367.68130
[11] Galdino, A. L.; Ayala-Rincón, M., A formalization of the Knuth-bendix(-huet) critical pair theorem, Journal of Automated Reasoning, 45, 3, 301-325, (2010) · Zbl 1207.68338
[12] Huet, G. P., A unification algorithm for typed λ-calculus, Theoretical Computer Science, 1, 27-57, (1975) · Zbl 0332.02035
[13] Kumar, R.; Norrish, M., (nominal) unification by recursive descent with triangular substitutions, (Interactive Theorem Proving, First International Conference, ITP 2010, Lecture Notes in Computer Science, vol. 6172, (2010), Springer), 51-66 · Zbl 1291.68356
[14] Levy, J.; Villaret, M., An efficient nominal unification algorithm, (Proceedings of the 21 st International Conference on Rewriting Techniques and Applications, RTA 2010, LIPIcs, vol. 6, (2010)), 209-226 · Zbl 1236.68138
[15] Levy, J.; Villaret, M., Nominal unification from a higher-order perspective, ACM Transactions on Computational Logic, 13, 2, 10, (2012) · Zbl 1352.03017
[16] Paulson, L. C., Verifying the unification algorithm in LCF, Science of Computer Programming, 5, 2, 143-169, (1985) · Zbl 0567.68054
[17] Shankar, N.; Owre, S.; Rushby, J. M.; Stringer-Calvert, D. W.J., PVS prover guide, (2001), SRI International, Technical report
[18] Urban, C.; Pitts, A. M.; Gabbay, M., Nominal unification, Theoretical Computer Science, 323, 1-3, 473-497, (2004) · Zbl 1078.68140
[19] Urban, C., Formalisation of nominal unification in isabelle/HOL, (2004), TU Munich, last visited April 2015
[20] Urban, C., Nominal techniques in isabelle/HOL, Journal of Automated Reasoning, 40, 4, 327-356, (2008) · Zbl 1140.68061
[21] Urban, C., Nominal unification revisited, Proceedings 24 th International Workshop on Unification, UNIF 2010, Electronic Proceedings in Theoretical Computer Science, 42, 1-11, (2010)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.