Nominal Unification and Matching of Higher Order Expressions with Recursive Let

• Autorzy: Schmidt-Schauß Manfred , Kutsia Temur , Levy Jordi , Villaret Mateu , Kutz Yunus

Identyfikatory

DOI

10.3233/FI-222110

• Języki publikacji: EN

Abstrakty

EN

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

Słowa kluczowe

EN

atom variables; higher-order expressions; lambda calculus; Nominal unification; recursive let

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: Vol. 185, nr 3
• Strony: 247--283
• Opis fizyczny: Bibliogr. 49 poz.

Twórcy

autor

Schmidt-Schauß Manfred

• GU Frankfurt, Germany

autor

Kutsia Temur

• RISC, JKU Linz, Austria

autor

Levy Jordi

• 3IIIA - CSIC, Spain.

autor

Villaret Mateu

• IMA, Universitat de Girona, Spain.

autor

Kutz Yunus

Bibliografia

• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [15] Cheney J. Equivariant Unification. J. Autom. Reasoning, 2010. 45(3):267-300. doi:10.1007/s10817-009-9164-3.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [26] Martelli A, Montanari U. An efficient unification algorithm. ACM Trans. Program. Lang. Syst., 1982.4(2):258-282. 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.
• [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.
• [29] Ayala-Rinc´on M, de Carvalho Segundo W, Fern´andez 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
• [30] Ayala-Rincón M, Fern´andez 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.
• [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. [32] Fernández M, Gabbay M. Nominal rewriting. Inf. Comput., 2007. 205(6):917-965. 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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [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.
• [45] Babai L. Graph Isomorphism in Quasipolynomial Time. http://arxiv.org/abs/1512.03547v2, 2016.
• [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.
• [47] Lohrey M, Maneth S, Schmidt-Schauß M. Parameter reduction and automata evaluation for grammarcompressed trees. J. Comput. Syst. Sci., 2012. 78(5):1651-1669. doi:10.1016/j.jcss.2012.03.003.
• [48] Gasc´on 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.
• [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.

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023). (PL)