Nominal unification and matching of higher order expressions with recursive let. (English) Zbl 1540.68114
Summary: A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. We also provide a nominal unification algorithm for higher-order expressions with recursive let and atom-variables, where we show that it also runs in nondeterministic polynomial time. In addition we prove that there is a guessing strategy for nominal unification with letrec and atom-variable that is a trade-off between exponential growth and non-determinism. Nominal matching with variables representing partial letrec-environments is also shown to be in NP.
Keywords:
nominal unification; lambda-calculus; higher-order expressions; recursive let; atom variablesReferences:
| [1] | Schmidt-Schauß M, Kutsia T, Levy J, Villaret M. Nominal Unification of Higher Order Expressions with Recursive Let. In: Hermenegildo MV, López-García P (eds.), Logic-Based Program Synthesis and Transformation -26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers, volume 10184 of Lecture Notes in Computer Science. Springer, 2016 pp. 328-344. doi:10.1007/978-3-319-63139-4 19. · Zbl 1485.68074 · doi:10.1007/978-3-319-63139-419 |
| [2] | Baader F, Snyder W. Unification Theory. In: Robinson JA, Voronkov A (eds.), Handbook of Automated Reasoning, pp. 445-532. Elsevier and MIT Press, 2001. · Zbl 1011.68126 |
| [3] | Huet GP. A Unification Algorithm for Typed lambda-Calculus. Theor. Comput. Sci., 1975. 1(1):27-57. doi:10.1016/0304-3975(75)90011-0. · Zbl 0332.02035 · doi:10.1016/0304-3975(75)90011-0 |
| [4] | Goldfarb WD. The Undecidability of the Second-Order Unification Problem. Theor. Comput. Sci., 1981. 13:225-230. doi:10.1016/0304-3975(81)90040-2. · Zbl 0457.03006 · doi:10.1016/0304-3975(81)90040-2 |
| [5] | Levy J, Veanes M. On the Undecidability of Second-Order Unification. Inf. Comput., 2000. 159(1-2):125-150. doi:10.1006/inco.2000.2877. · Zbl 1005.03007 · doi:10.1006/inco.2000.2877 |
| [6] | Urban C, Pitts AM, Gabbay M. Nominal Unification. In: 17th CSL, 12th EACSL, and 8th KGC, volume 2803 of LNCS. Springer, 2003 pp. 513-527. doi:10.1007/978-3-540-45220-1 41. · Zbl 1116.03322 · doi:10.1007/978-3-540-45220-141 |
| [7] | Urban C, Pitts AM, Gabbay MJ. Nominal unification. Theor. Comput. Sci., 2004. 323(1-3):473-497. doi:10.1016/j.tcs.2004.06.016. · Zbl 1078.68140 · doi:10.1016/j.tcs.2004.06.016 |
| [8] | Calvès C, Fernández M. A polynomial nominal unification algorithm. Theor. Comput. Sci., 2008. 403(2-3):285-306. doi:10.1016/j.tcs.2008.05.012. · Zbl 1154.68108 · doi:10.1016/j.tcs.2008.05.012 |
| [9] | Levy J, Villaret M. Nominal Unification from a Higher-Order Perspective. ACM Trans. Comput. Log., 2012. 13(2):10. doi:10.1145/2159531.2159532. · Zbl 1352.03017 · doi:10.1145/2159531.2159532 |
| [10] | Miller D. A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. J. Log. Comput., 1991. 1(4):497-536. doi:10.1093/logcom/1.4.497. · Zbl 0738.68016 · doi:10.1093/logcom/1.4.497 |
| [11] | Levy J, Villaret M. An Efficient Nominal Unification Algorithm. In: Lynch C (ed.), Proc. 21st RTA, volume 6 of LIPIcs. Schloss Dagstuhl, 2010 pp. 209-226. doi:10.4230/LIPIcs.RTA.2010.209. · Zbl 1236.68138 · doi:10.4230/LIPIcs.RTA.2010.209 |
| [12] | Ayala-Rincón M, Fernández M, Rocha-Oliveira AC. Completeness in PVS of a Nominal Unification Algorithm. ENTCS, 2016. 323(3):57-74. doi:10.1016/j.entcs.2016.06.005. · Zbl 1394.68348 · doi:10.1016/j.entcs.2016.06.005 |
| [13] | 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. Electr. Notes Theor. Comput. Sci., 2017. 332:21-38. doi:10.1016/j.entcs.2017.04.003. · Zbl 1401.68273 · doi:10.1016/j.entcs.2017.04.003 |
| [14] | Ayala-Rincón M, Fernández M, Nantes-Sobrinho D. Nominal Narrowing. In: Pientka B, Kesner D (eds.), Proc. first FSCD, LIPIcs. 2016 pp. 11:1-11:17. doi:10.4230/LIPIcs.FSCD.2016.11. · Zbl 1387.68142 · doi:10.4230/LIPIcs.FSCD.2016.11 |
| [15] | Cheney J. Equivariant Unification. J. Autom. Reasoning, 2010. 45(3):267-300. doi:10.1007/ s10817-009-9164-3. · Zbl 1207.68368 |
| [16] | Cheney J. Nominal Logic Programming. Ph.D. thesis, Cornell University, Ithaca, New York, U.S.A., 2004. |
| [17] | Aoto T, Kikuchi K. A Rule-Based Procedure for Equivariant Nominal Unification. In: Informal proceedings HOR. 2016 p. 5. |
| [18] | Moran AKD, Sands D, Carlsson M. Erratic Fudgets: A semantic theory for an embedded coordination language. In: Coordination ’99, volume 1594 of LNCS. Springer-Verlag, 1999 pp. 85-102. doi:10.1007/ 3-540-48919-3 8. |
| [19] | Schmidt-Schauß M, Schütz M, Sabel D. Safety of Nöcker’s Strictness Analysis. J. Funct. Programming, 2008. 18(04):503-551. doi:10.1017/S0956796807006624. · Zbl 1153.68012 · doi:10.1017/S0956796807006624 |
| [20] | Ariola ZM, Klop JW. Cyclic Lambda Graph Rewriting. In: Proc. IEEE LICS. IEEE Press, 1994 pp. 416-425. doi:10.1109/LICS.1994.316066. · doi:10.1109/LICS.1994.316066 |
| [21] | Marlow S (ed.). Haskell 2010 -Language Report. 2010. URL https://www.haskell.org. |
| [22] | Cheney J. Toward a General Theory of Names: Binding and Scope. In: MERLIN 2005. ACM, 2005 pp. 33-40. doi:10.1145/1088454.1088459. · doi:10.1145/1088454.1088459 |
| [23] | Urban C, Kaliszyk C. General Bindings and Alpha-Equivalence in Nominal Isabelle. Log. Methods Comput. Sci., 2012. 8(2). doi:10.2168/LMCS-8(2:14)2012. · Zbl 1242.68283 · doi:10.2168/LMCS-8(2:14)2012 |
| [24] | Simon L, Mallya A, Bansal A, Gupta G. Coinductive Logic Programming. In: Etalle S, Truszczynski M (eds.), 22nd ICLP, LNCS. 2006 pp. 330-345. doi:10.1007/11799573 25. · Zbl 1131.68400 · doi:10.1007/1179957325 |
| [25] | Jeannin J, Kozen D, Silva A. CoCaml: Functional Programming with Regular Coinductive Types. Fundam. Inform., 2017. 150(3-4):347-377. doi:10.3233/FI-2017-1473. · Zbl 1374.68098 · doi:10.3233/FI-2017-1473 |
| [26] | Martelli A, Montanari U. An efficient unification algorithm. ACM Trans. Program. Lang. Syst., 1982. 4(2):258-282. doi:10.1145/357162.357169. · Zbl 0478.68093 · doi:10.1145/357162.357169 |
| [27] | Schmidt-Schauß M, Sabel D, Kutz YDK. Nominal unification with atom-variables. J. Symb. Comput., 2019. 90:42-64. doi:10.1016/j.jsc.2018.04.003. · Zbl 1395.68096 · doi:10.1016/j.jsc.2018.04.003 |
| [28] | Schmidt-Schauß M, Sabel D. Nominal Unification with Atom and Context Variables. In: Kirchner [49], 2018 pp. 28:1-28:20. doi:10.4230/LIPIcs.FSCD.2018.28. · Zbl 1462.68026 · doi:10.4230/LIPIcs.FSCD.2018.28 |
| [29] | Ayala-Rincón M, de Carvalho Segundo W, Fernández M, Nantes-Sobrinho D. Nominal C-Unification. In: Fioravanti F, Gallagher JP (eds.), 27th LOPSTR, Revised Selected Papers, volume 10855 of LNCS. Springer, 2017 pp. 235-251. doi:10.1007/978-3-319-94460-9 14. · Zbl 1502.68144 · doi:10.1007/978-3-319-94460-914 |
| [30] | Ayala-Rincón M, Fernández M, Nantes-Sobrinho D. Fixed-Point Constraints for Nominal Equational Unification. In: Kirchner [49], 2018 pp. 7:1-7:16. doi:10.4230/LIPIcs.FSCD.2018.7. · Zbl 1462.68089 · doi:10.4230/LIPIcs.FSCD.2018.7 |
| [31] | Schmidt-Schauss M, Kutsia T, Levy J, Villaret M. Nominal Unification of Higher Order Expressions with Recursive Let. RISC Report Series 16-03, RISC, Johannes Kepler University Linz, Austria, 2016. · Zbl 1485.68074 |
| [32] | Fernández M, Gabbay M. Nominal rewriting. Inf. Comput., 2007. 205(6):917-965. doi:10.1016/j.ic.2006. 12.002. · Zbl 1118.68075 · doi:10.1016/j.ic.2006.12.002 |
| [33] | Baldan P, Bertolissi C, Cirstea H, Kirchner C. A rewriting calculus for cyclic higher-order term graphs. Mathematical Structures in Computer Science, 2007. 17(3):363-406. doi:10.1017/S0960129507006093. · Zbl 1125.68062 · doi:10.1017/S0960129507006093 |
| [34] | Rau C, Schmidt-Schauß M. A Unification Algorithm to Compute Overlaps in a Call-by-Need Lambda-Calculus with Variable-Binding Chains. In: Proc. 25th UNIF. 2011 pp. 35-41. |
| [35] | Rau C, Schmidt-Schauß M. Towards Correctness of Program Transformations Through Unification and Critical Pair Computation. In: Proc. 24th UNIF, volume 42 of EPTCS. 2010 pp. 39-54. doi: 10.4204/EPTCS.42.4. · doi:10.4204/EPTCS.42.4 |
| [36] | Schmidt-Schauß M, Sabel D. Unification of program expressions with recursive bindings. In: Cheney J, Vidal G (eds.), 18th PPDP. ACM, 2016 pp. 160-173. doi:10.1145/2967973.2968603. · doi:10.1145/2967973.2968603 |
| [37] | Dowek G, Gabbay MJ, Mulligan DP. Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques. Log. J. IGPL, 2010. 18(6):769-822. doi:10.1093/jigpal/jzq006. · Zbl 1215.03048 · doi:10.1093/jigpal/jzq006 |
| [38] | Schmidt-Schauß M, Rau C, Sabel D. Algorithms for Extended Alpha-Equivalence and Complexity. In: van Raamsdonk F (ed.), 24th RTA 2013, volume 21 of LIPIcs. Schloss Dagstuhl, 2013 pp. 255-270. doi:10.4230/LIPIcs.RTA.2013255. · Zbl 1356.68046 · doi:10.4230/LIPIcs.RTA.2013255 |
| [39] | Luks EM. Permutation Groups and Polynomial-Time Computation. In: Finkelstein L, Kantor WM (eds.), Groups And Computation, volume 11 of DIMACS. DIMACS/AMS, 1991 pp. 139-176. · Zbl 0813.20004 |
| [40] | Furst ML, Hopcroft JE, Luks EM. Polynomial-Time Algorithms for Permutation Groups. In: 21st FoCS. IEEE Computer Society, 1980 pp. 36-41. doi:10.1109/SFCS.1980.34. · doi:10.1109/SFCS.1980.34 |
| [41] | Picouleau C. Complexity of the Hamiltonian Cycle in Regular Graph Problem. Theor. Comput. Sci., 1994. 131(2):463-473. doi:10.1016/0304-3975(94)90185-6. · Zbl 0809.68091 · doi:10.1016/0304-3975(94)90185-6 |
| [42] | Garey MR, Johnson DS, Tarjan RE. The Planar Hamiltonian Circuit Problem is NP-Complete. SIAM J. Comput., 1976. 5(4):704-714. doi:10.1137/0205049. · Zbl 0346.05110 · doi:10.1137/0205049 |
| [43] | Ariola ZM, Felleisen M, Maraist J, Odersky M, Wadler P. A call-by-need lambda calculus. In: POPL’95. ACM Press, San Francisco, CA, 1995 pp. 233-246. doi:10.1145/199448.199507. · doi:10.1145/199448.199507 |
| [44] | Schöning U. Graph Isomorphism is in the Low Hierarchy. J. Comput. Syst. Sci., 1988. 37(3):312-323. doi:10.1016/0022-0000(88)90010-4. · Zbl 0666.68048 · doi:10.1016/0022-0000(88)90010-4 |
| [45] | Babai L. Graph Isomorphism in Quasipolynomial Time. http://arxiv.org/abs/1512.03547v2, 2016. · Zbl 1376.68058 |
| [46] | Booth KS. Isomorphism Testing for Graphs, Semigroups, and Finite Automata Are Polynomially Equivalent Problems. SIAM J. Comput., 1978. 7(3):273-279. doi:10.1137/0207023. · Zbl 0381.68042 · doi:10.1137/0207023 |
| [47] | Lohrey M, Maneth S, Schmidt-Schauß M. Parameter reduction and automata evaluation for grammar-compressed trees. J. Comput. Syst. Sci., 2012. 78(5):1651-1669. doi:10.1016/j.jcss.2012.03.003. · Zbl 1246.68114 · doi:10.1016/j.jcss.2012.03.003 |
| [48] | Gascón A, Godoy G, Schmidt-Schauß M. Unification and matching on compressed terms. ACM Trans. Comput. Log., 2011. 12(4):26:1-26:37. doi:10.1145/1970398.1970402. · Zbl 1351.68128 · doi:10.1145/1970398.1970402 |
| [49] | Kirchner H (ed.). 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, volume 108 of LIPIcs. Schloss Dagstuhl, 2018. |
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.
