A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols. (English) Zbl 1423.68405
Summary: This paper describes a formalisation in Coq of nominal syntax extended with associative (A), commutative (C) and associative-commutative (AC) operators. This formalisation is based on a natural notion of nominal \(\alpha\)-equivalence, avoiding the use of an auxiliary weak \({\alpha}\)-relation used in previous formalisations of nominal AC equivalence. A general \(\alpha\)-relation between terms with A, C and AC function symbols is specified and formally proved to be an equivalence relation. As corollaries, one obtains the soundness of \(\alpha\)-equivalence modulo A, C and AC operators. General \(\alpha\)-equivalence problems with A operators are log-linearly bounded in time while if there are also C operators they can be solved in \(O(n^2 \log n)\); nominal \(\alpha\)-equivalence problems that also include AC operators can be solved with the same running time complexity as in standard first-order AC approaches.
This development is a first step towards verification of nominal matching, unification and narrowing algorithms modulo equational theories in general.
This development is a first step towards verification of nominal matching, unification and narrowing algorithms modulo equational theories in general.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B70 | Logic in computer science |
| 68Q25 | Analysis of algorithms and problem complexity |
References:
| [1] | Barendregt, H., The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103 (1984), North-Holland · Zbl 0551.03007 |
| [2] | Pitts, A. M., Nominal logic, a first order theory of names and binding, Inform. and Comput., 186, 2, 165-193 (2003) · Zbl 1056.03014 |
| [3] | Calvès, C. F.; Fernández, M., Implementing nominal unification, Electron. Notes Theor. Comput. Sci., 176, 1, 25-37 (2007) · Zbl 1278.68118 |
| [4] | Kumar, R.; Norrish, M., (Nominal) unification by recursive descent with triangular substitutions, (Proc. of the 1st Int. Conf. of Interactive Theorem Proving. Proc. of the 1st Int. Conf. of Interactive Theorem Proving, ITP. Proc. of the 1st Int. Conf. of Interactive Theorem Proving. Proc. of the 1st Int. Conf. of Interactive Theorem Proving, ITP, LNCS, vol. 6172 (2010), Springer), 51-66 · Zbl 1291.68356 |
| [5] | Ayala-Rincón, M.; Fernández, M.; Rocha-oliveira, A. C., Completeness in PVS of a nominal unification algorithm, Electron. Notes Theor. Comput. Sci., 323, 57-74 (2016) · Zbl 1394.68348 |
| [6] | Urban, C., Nominal unification revisited, (Proc. of the 24th Int. Work. on Unification. Proc. of the 24th Int. Work. on Unification, UNIF. Proc. of the 24th Int. Work. on Unification. Proc. of the 24th Int. Work. on Unification, UNIF, EPTCS, vol. 42 (2010)), 1-11 |
| [7] | Urban, C.; Pitts, A. M.; Gabbay, M. J., Nominal unification, Theoret. Comput. Sci., 323, 1-3, 473-497 (2004) · Zbl 1078.68140 |
| [8] | Fernández, M.; Gabbay, M. J., Nominal rewriting, Inform. and Comput., 205, 6, 917-965 (2007) · Zbl 1118.68075 |
| [9] | Fernández, M.; Gabbay, M. J., Closed nominal rewriting and efficiently computable nominal algebra equality, (Proc. of the 5th Int. Work. on Logical Frameworks and Meta-Languages: Theory and Practice. Proc. of the 5th Int. Work. on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP. Proc. of the 5th Int. Work. on Logical Frameworks and Meta-Languages: Theory and Practice. Proc. of the 5th Int. Work. on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP, EPTCS, vol. 34 (2010)), 37-51 |
| [10] | Fernández, M.; Gabbay, M. J.; Mackie, I., Nominal rewriting systems, (Proc. of the 6th Int. Conf. on Principles and Practice of Declarative Programming. Proc. of the 6th Int. Conf. on Principles and Practice of Declarative Programming, PPDP (2004), ACM Press), 108-119 |
| [11] | Cheney, J., \(α\) Prolog user’s guide - version 0.3 DRAFT (2003), available at |
| [12] | 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 |
| [13] | Shinwell, M. R., The Fresh Approach: Functional Programming with Names and Binders (2005), University of Cambridge, available at |
| [14] | Shinwell, M. R.; Pitts, A. M.; Gabbay, M. J., FreshML: programming with binders made simple, (Proc. of the Int. Conference on Functional Programming (ICFP). Proc. of the Int. Conference on Functional Programming (ICFP), ICFP’03 (2003), ACM Press), 263-274 · Zbl 1315.68058 |
| [15] | Aydemir, B.; Bohannon, A.; Weirich, S., Nominal reasoning techniques in Coq, Electron. Notes Theor. Comput. Sci., 174, 5, 69-77 (2007) · Zbl 1278.68248 |
| [16] | Urban, C., Nominal techniques in Isabelle/HOL, J. Automat. Reason., 40, 4, 327-356 (2008) · Zbl 1140.68061 |
| [17] | Ayala-Rincón, M.; de Carvalho Segundo, W.; Fernández, M.; Nantes-Sobrinho, D., A formalisation of nominal \(α\)-equivalence with A and AC function symbols, Electron. Notes Theor. Comput. Sci., 332, 21-38 (2017) · Zbl 1401.68273 |
| [18] | Calvès, C. F.; Fernández, M., Matching and alpha-equivalence check for nominal terms, J. Comput. System Sci., 76, 5, 283-301 (2010) · Zbl 1206.68159 |
| [19] | Benanav, D.; Kapur, D.; Narendran, P., Complexity of matching problems, J. Symbolic Comput., 3, 1/2, 203-216 (1987) · Zbl 0638.68036 |
| [20] | Sozeau, M., Equations: a dependent pattern-matching compiler, (Proc. of the 1st Int. Conf. of Interactive Theorem Proving. Proc. of the 1st Int. Conf. of Interactive Theorem Proving, ITP. Proc. of the 1st Int. Conf. of Interactive Theorem Proving. Proc. of the 1st Int. Conf. of Interactive Theorem Proving, ITP, LNCS, vol. 6172 (2010), Springer), 419-434 · Zbl 1291.68369 |
| [21] | Sozeau, M., Subset coercions in Coq, (Proc. of the Int. Work. on Types for Proofs and Programs. Proc. of the Int. Work. on Types for Proofs and Programs, TYPES. Proc. of the Int. Work. on Types for Proofs and Programs. Proc. of the Int. Work. on Types for Proofs and Programs, TYPES, LNCS, vol. 4502 (2006), Springer), 237-252 · Zbl 1178.68531 |
| [22] | Larchey-Wendling, D.; Monin, J.-F., Simulating induction-recursion for partial algorithms (2018), accepted to TYPES, available at |
| [23] | Cormen, T. H.; Leiserson, C. E.; Rivest, R.; Stein, C., Introduction to Algorithms (2009), The MIT Press · Zbl 1187.68679 |
| [24] | Baader, F.; Snyder, W.; Narendran, P.; Schmidt-Schauß, M.; Schulz, K. U., Unification theory, (Handbook of Automated Reasoning (2001), MIT Press and North Holand), 445-454, (in 2 volumes) · Zbl 0964.00020 |
| [25] | Fages, F., Associative-commutative unification, J. Symbolic Comput., 3, 257-275 (1987) · Zbl 0638.68103 |
| [26] | Nipkow, T., Equational reasoning in isabelle, Sci. Comput. Program., 12, 2, 123-149 (1989) · Zbl 0683.68081 |
| [27] | Contejean, E., A certified AC matching algorithm, (Proc. of the 15th Int. Conf. on Rewriting Techniques and Applications. Proc. of the 15th Int. Conf. on Rewriting Techniques and Applications, RTA. Proc. of the 15th Int. Conf. on Rewriting Techniques and Applications. Proc. of the 15th Int. Conf. on Rewriting Techniques and Applications, RTA, LNCS, vol. 3091 (2004), Springer), 70-84 · Zbl 1187.68524 |
| [28] | Braibant, T.; Pous, D., Tactics for reasoning modulo AC in Coq, (Proc. of the 1st. Int. Conf. on Certified Programs and Proofs. Proc. of the 1st. Int. Conf. on Certified Programs and Proofs, CPP. Proc. of the 1st. Int. Conf. on Certified Programs and Proofs. Proc. of the 1st. Int. Conf. on Certified Programs and Proofs, CPP, LNCS, vol. 7086 (2011), Springer), 167-182 · Zbl 1350.68227 |
| [29] | Copello, E.; Tasistro, E.; Szasz, N.; Bove, A.; Fernández, M., Principles of alpha-induction and recursion for the lambda calculus in constructive type theory, Electron. Notes Theor. Comput. Sci., 323, 109-124 (2016) · Zbl 1395.68085 |
| [30] | Ayala-Rincón, M.; Carvalho-Segundo, W.; Fernández, M.; Nantes-Sobrinho, D., Nominal C-unification, (Proc. of the 27th Int. Symp. Logic-Based Program Synthesis and Transformation. Proc. of the 27th Int. Symp. Logic-Based Program Synthesis and Transformation, LOPSTR. Proc. of the 27th Int. Symp. Logic-Based Program Synthesis and Transformation. Proc. of the 27th Int. Symp. Logic-Based Program Synthesis and Transformation, LOPSTR, LNCS, vol. 10855 (2017), Springer), 235-251 · Zbl 1502.68144 |
| [31] | Ayala-Rincón, M.; Fernández, M.; Nantes-Sobrinho, D., Nominal narrowing, (Proc. of the 1st Int. Conf. on Formal Structures for Computation and Deduction. Proc. of the 1st Int. Conf. on Formal Structures for Computation and Deduction, FSCD. Proc. of the 1st Int. Conf. on Formal Structures for Computation and Deduction. Proc. of the 1st Int. Conf. on Formal Structures for Computation and Deduction, FSCD, SDLZI LIPIcs, vol. 52 (2016)), 11:1-11:17 · Zbl 1387.68142 |
| [32] | Kutsia, T.; Levy, J.; Schmidt-Schauß, M.; Villaret, M., Nominal unification of higher order expressions with recursive let, (Proc. of the 26th Int. Symp. on Logic-Based Program Synthesis and Transformation. Proc. of the 26th Int. Symp. on Logic-Based Program Synthesis and Transformation, LOPSTR. Proc. of the 26th Int. Symp. on Logic-Based Program Synthesis and Transformation. Proc. of the 26th Int. Symp. on Logic-Based Program Synthesis and Transformation, LOPSTR, LNCS, vol. 10184 (2016), Springer), 328-344 · Zbl 1485.68074 |
| [33] | Ayala-Rincón, M.; Carvalho-Segundo, W.; Fernández, M.; Nantes-Sobrinho, D., On solving nominal fixpoint equations, (Proc. of the 11th Int. Symp. on Frontiers of Combining Systems. Proc. of the 11th Int. Symp. on Frontiers of Combining Systems, FroCoS. Proc. of the 11th Int. Symp. on Frontiers of Combining Systems. Proc. of the 11th Int. Symp. on Frontiers of Combining Systems, FroCoS, LNCS, vol. 10483 (2017), Springer), 209-226 · Zbl 1495.68108 |
| [34] | Ayala-Rincón, M.; Fernández, M.; Nantes-Sobrinho, D., Fixed-point constraints for nominal equational unification, (Proc. of the 3rd Int. Conf. on Formal Structures for Computation and Deduction. Proc. of the 3rd Int. Conf. on Formal Structures for Computation and Deduction, FSCD. Proc. of the 3rd Int. Conf. on Formal Structures for Computation and Deduction. Proc. of the 3rd Int. Conf. on Formal Structures for Computation and Deduction, FSCD, SDLZI LIPIcs, vol. 108 (2018)), 7:1-7:16 · Zbl 1462.68089 |
| [35] | Cortier, V.; Delaune, S.; Lafourcade, P., A survey of algebraic properties used in cryptographic protocols, J. Comput. Secur., 14, 1, 1-43 (2006) |
| [36] | Escobar, S.; Meadows, C.; Meseguer, J., Maude-NPA: cryptographic protocol analysis modulo equational properties, (Foundations of Security Analysis and Design, vol. 5705 (2007)), 1-50 · Zbl 1252.94061 |
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.
