×

A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols. (English) Zbl 1401.68273

Nigam, Vivek (ed.) et al., Proceedings of the 11th workshop on logical and semantic frameworks, with applications (LSFA 2016), Porto, Portugal, 2016. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 332, 21-38 (2017).
Summary: A formalisation of soundness of the notion of \(\alpha\)-equivalence in nominal abstract syntax modulo associative (A) and associative-commutative (AC) equational theories is described. Initially, the notion of \(\alpha\)-equivalence is specified based on a so called “weak” nominal relation as suggested by C. Urban [J. Autom. Reasoning 40, No. 4, 327–356 (2008; Zbl 1140.68061)] in his nominal development in Isabelle/HOL. Then, it is formalised in Coq that this equality is indeed an equivalence relation. After that, general \(\alpha\)-equivalence with A and AC function symbols is specified and formally proved to be an equivalence relation. As corollaries, the soundness \(\alpha\)-equivalence modulo A and modulo AC is obtained. Finally, an algorithm for checking \(\alpha\)-equivalence modulo A and AC is proposed. General \(\alpha\)-equivalence problems are log-linearly solved while AC and the combination of A and AC \(\alpha\)-equivalence problems have the same complexity as standard first-order approaches. This development is a first step towards verification of nominal matching, unification and narrowing algorithms modulo equational theories in general.
For the entire collection see [Zbl 1375.68023].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B70 Logic in computer science
68Q25 Analysis of algorithms and problem complexity

Citations:

Zbl 1140.68061
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ayala-Rincón, M.; Fernández, M.; Nantes-Sobrinho, D., Nominal narrowing, (LIPIcs Proc. 1st Int. Conf. on Formal Structures for Computation and Deduction (FSCD), vol. 52 (2016)), 11:1-11:17 · Zbl 1387.68142
[2] Ayala-Rincón, M.; Fernández, M.; Rocha-oliveira, A. C., Completeness in PVS of a Nominal Unification Algorithm, (Logical and Semantic Frameworks with Appl. 2015 (LSFA). Logical and Semantic Frameworks with Appl. 2015 (LSFA), ENTCS, vol. 323 (2016)), 57-74 · Zbl 1394.68348
[3] Aydemir, B.; Bohannon, A.; Weirich, S., Nominal Reasoning Techniques in Coq, Electronic Notes in Theoretical Computer Science, 174, 5, 69-77 (2007) · Zbl 1278.68248
[5] Barendregt, H., The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103 (1984) · Zbl 0551.03007
[6] Benanav, D.; Kapur, D.; Narendran, P., Complexity of Matching Problems, J. Symb. Comput., 3, 1/2, 203-216 (1987) · Zbl 0638.68036
[7] Boudet, A.; Contejean, E.; Devie, H., A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations, Fifth Annual IEEE Symposium on Logic in Computer Science(LICS), 289-299 (1990)
[8] Byrd, W. E.; Friedman, D. P., \(α\) Kanren: A Fresh Name in Nominal Logic Programming, (Proc. of the Workshop on Scheme and Functional Programming (2007)), 79-90
[9] Calvès, C. F.; Fernández, M., Implementing Nominal Unification, ENTCS, 176, 1, 25-37 (2007) · Zbl 1278.68118
[10] Calvès, C. F.; Fernández, M., Matching and alpha-equivalence check for nominal terms, Journal of Computer and System Sciences, 76, 5, 283-301 (2010) · Zbl 1206.68159
[12] Copello, E.; Tasistro, Á.; Szasz, N.; Bove, A.; Fernández, M., Principles of Alpha-Induction and Recursion for the Lambda Calculus in Constructive Type Theory, (Logical and Semantic Frameworks with Applications 2015 (LSFA). Logical and Semantic Frameworks with Applications 2015 (LSFA), ENTCS, vol. 323 (2016)), 109-124 · Zbl 1395.68085
[13] Cormen, T. H.; Leiserson, C. E.; Rivest, R.; Stein, C., Introduction to Algorithms (2009), MIT Press · Zbl 1187.68679
[14] Cortier, V.; Delaune, S.; Lafourcade, P., A survey of algebraic properties used in cryptographic protocols, Journal of Computer Security, 14, 1, 1-43 (2006)
[15] Escobar, S.; Meadows, C.; Maude-npa, J. Meseguer, Cryptographic protocol analysis modulo equational properties, Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009, 5705, 1-50 (2007) · Zbl 1252.94061
[16] Fernández, M.; Gabbay, M. J., Nominal rewriting, Information and Comp., 205, 6, 917-965 (2007) · Zbl 1118.68075
[17] Fernández, M.; Gabbay, M. J., Closed nominal rewriting and efficiently computable nominal algebra equality, Elect. Proc. in Theoretical Computer Science, 34, 37-51 (2010)
[18] Fernández, M.; Gabbay, M. J.; Mackie, I., Nominal rewriting systems, Int. conference on Principles and practice of declarative programming, 108-119 (2004)
[19] Kumar, R.; Norrish, M., (Nominal) Unification by Recursive Descent with Triangular Substitutions, Interactive Theorem Proving, 51-66 (2010) · Zbl 1291.68356
[20] Pitts, A. M., Nominal Logic: A First Order Theory of Names and Binding, Int. Symposium on Theoretical Aspects of Computer Software, 2215, 219-242 (2001) · Zbl 1087.03510
[21] Schmidt-Schauß, M.; Kutsia, T.; Levy, J.; Villaret, M., Nominal Unification of Higher Order Expressions with Recursive Let (2016), Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz: Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz Austria, RISC Report Series TR no. 16-03
[22] Shinwell, M. R., The Fresh Approach: functional programming with names and binders (2005), University of Cambridge, Technical report
[23] Shinwell, M. R.; Pitts, A. M.; Gabbay, M. J., FreshML: Programming with binders made simple, Int. Conference on Functional Programming, 263-274 (2003) · Zbl 1315.68058
[24] Urban, C., Nominal Techniques in Isabelle/HOL, Journal of Automated Reasoning, 40, 4, 327-356 (2008) · Zbl 1140.68061
[25] Urban, C., Nominal Unification Revisited, Int. Work. on Unification, 513-527 (2010) · Zbl 1116.03322
[26] Urban, C.; Pitts, A. M.; Gabbay, M. J., Nominal unification, Theoretical Computer Science, 323, 1-3, 473-497 (2004) · Zbl 1078.68140
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.