Document Open Access Logo

Nominal Unification with Atom and Context Variables

Authors Manfred Schmidt-Schauß , David Sabel

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.28.pdf
  • Filesize: 0.55 MB
  • 20 pages

Document Identifiers

Author Details

Manfred Schmidt-Schauß
  • Goethe-University Frankfurt, Germany
David Sabel
  • Goethe-University Frankfurt, Germany

Funding

  • Schmidt-Schauß, Manfred: Supported by the Deutsche Forschungsgemeinschaft (DFG) under grant SCHM 986/11-1.
  • Sabel, David: Supported by the Deutsche Forschungsgemeinschaft (DFG) under grant SA2908/3-1.

Cite AsGet BibTex

Manfred Schmidt-Schauß and David Sabel. Nominal Unification with Atom and Context Variables. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.28

Abstract

Automated deduction in higher-order program calculi, where properties of transformation rules are demanded, or confluence or other equational properties are requested, can often be done by syntactically computing overlaps (critical pairs) of reduction rules and transformation rules. Since higher-order calculi have alpha-equivalence as fundamental equivalence, the reasoning procedure must deal with it. We define ASD1-unification problems, which are higher-order equational unification problems employing variables for atoms, expressions and contexts, with additional distinct-variable constraints, and which have to be solved w.r.t. alpha-equivalence. Our proposal is to extend nominal unification to solve these unification problems. We succeeded in constructing the nominal unification algorithm NomUnifyASD. We show that NomUnifyASD is sound and complete for this problem class, and outputs a set of unifiers with constraints in nondeterministic polynomial time if the final constraints are satisfiable. We also show that solvability of the output constraints can be decided in NEXPTIME, and for a fixed number of context-variables in NP time. For terms without context-variables and atom-variables, NomUnifyASD runs in polynomial time, is unitary, and extends the classical problem by permitting distinct-variable constraints.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • automated deduction
  • nominal unification
  • lambda calculus
  • functional programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Andreas Abel and Brigitte Pientka. Higher-order dynamic pattern unification for dependent types and records. In C.-H. Luke Ong, editor, Proc. 10th TLCA 2011, volume 6690 of Lect. Notes Comput. Sci., pages 10-26. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-21691-6_5.
  2. Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. A call-by-need lambda calculus. In Proc. POPL 1995, pages 233-246, San Francisco, CA, 1995. ACM Press. URL: http://dx.doi.org/10.1145/199448.199507.
  3. Mauricio Ayala-Rincón, Maribel Fernández, Murdoch Gabbay, and Ana Cristina Rocha Oliveira. Checking overlaps of nominal rewriting rules. Electr. Notes Theor. Comput. Sci., 323:39-56, 2016. URL: http://dx.doi.org/10.1016/j.entcs.2016.06.004.
  4. Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Nominal narrowing. In Delia Kesner and Brigitte Pientka, editors, Proc. FSCD 2016, volume 52, pages 11:1-11:17, Dagstuhl, Germany, 2016. Schloss Dagstuhl. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.11.
  5. Henk P. Barendregt. The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam, New York, 1984. Google Scholar
  6. Christophe Calvès and Maribel Fernández. A polynomial nominal unification algorithm. Theor. Comput. Sci., 403(2-3):285-306, 2008. URL: http://dx.doi.org/10.1016/j.tcs.2008.05.012.
  7. James Cheney. The complexity of equivariant unification. In Proc. ICALP 2004, volume 3142 of Lect. Notes Comput. Sci., pages 332-344. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-27836-8_30.
  8. James Cheney. Nominal Logic Programming. PhD thesis, Cornell University, Ithaca, NY, 2004. Google Scholar
  9. James Cheney. Relating higher-order pattern unification and nominal unification. In Proc. UNIF 2005, pages 104-119, 2005. Google Scholar
  10. James Cheney. Equivariant unification. J. Autom. Reasoning, 45(3):267-300, 2010. URL: http://dx.doi.org/10.1007/s10817-009-9164-3.
  11. Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies: A tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae, 34:381-392, 1972. Google Scholar
  12. Maribel Fernández and Albert Rubio. Nominal completion for rewrite systems with binders. In Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts, and Roger Wattenhofer, editors, Proc. ICALP 2012 Part II, volume 7392 of Lect. Notes Comput. Sci., pages 201-213. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31585-5_21.
  13. Gérard P. Huet. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci., 1(1):27-57, 1975. URL: http://dx.doi.org/10.1016/0304-3975(75)90011-0.
  14. Artur Jez. Context unification is in PSPACE. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Proc. ICALP 2014 Part II, volume 8573 of Lect. Notes Comput. Sci., pages 244-255. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-43951-7_21.
  15. Yunus Kutz and Manfred Schmidt-Schauß. Most general unifiers in generalized nominal unification. In Informal Proceedings of UNIF 2017, 2017. Google Scholar
  16. Matthew R. Lakin. Constraint solving in non-permutative nominal abstract syntax. Logical Methods in Computer Science, 7(3), 2011. URL: http://dx.doi.org/10.2168/LMCS-7(3:6)2011.
  17. Jordi Levy and Mateu Villaret. An efficient nominal unification algorithm. In Christopher Lynch, editor, Proc. RTA 2010, volume 6 of LIPIcs, pages 209-226. Schloss Dagstuhl, 2010. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2010.209.
  18. Jordi Levy and Mateu Villaret. Nominal unification from a higher-order perspective. ACM Trans. Comput. Log., 13(2):10, 2012. URL: http://dx.doi.org/10.1145/2159531.2159532.
  19. Tomer Libal and Dale Miller. Functions-as-constructors higher-order unification. In Delia Kesner and Brigitte Pientka, editors, Proc. FSCD 2016, volume 52 of LIPIcs, pages 26:1-26:17. Schloss Dagstuhl, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.26.
  20. Markus Lohrey. Algorithmics on SLP-compressed strings: A survey. Groups Complexity Cryptology, 4(2):241-299, 2012. URL: http://dx.doi.org/10.1515/gcc-2012-0016.
  21. Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Trans. Program. Lang., 4(2):258-282, 1982. URL: http://dx.doi.org/10.1145/357162.357169.
  22. Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput., 1(4):497-536, 1991. URL: http://dx.doi.org/10.1093/logcom/1.4.497.
  23. Andrew K. D. Moran, David Sands, and Magnus Carlsson. Erratic fudgets: A semantic theory for an embedded coordination language. In Proc. Coordination 1999, volume 1594 of Lect. Notes Comput. Sci., pages 85-102. Springer, 1999. URL: http://dx.doi.org/10.1007/3-540-48919-3_8.
  24. Tobias Nipkow. Functional unification of higher-order patterns. In Proc. LICS 1993, pages 64-74. IEEE Computer Society, 1993. URL: http://dx.doi.org/10.1109/LICS.1993.287599.
  25. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Richard L. Wexelblat, editor, Proc. PLDI 1988, pages 199-208. ACM, 1988. URL: http://dx.doi.org/10.1145/53990.54010.
  26. Andrew Pitts. Nominal techniques. ACM SIGLOG News, 3(1):57-72, 2016. URL: http://dx.doi.org/10.1145/2893582.2893594.
  27. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. Google Scholar
  28. Zhenyu Qian. Linear unification of higher-order patterns. In Proc. TAPSOFT 1993, pages 391-405. Springer, 1993. URL: http://dx.doi.org/10.1007/3-540-56610-4_78.
  29. David Sabel. Alpha-renaming of higher-order meta-expressions. In Wim Vanhoof and Brigitte Pientka, editors, Proc. PPDP 2017, pages 151-162. ACM, 2017. URL: http://dx.doi.org/10.1145/3131851.3131866.
  30. Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal unification of higher order expressions with recursive let. In Manuel V. Hermenegildo and Pedro López-García, editors, Proc. LOPSTR 2016, volume 10184 of Lect. Notes Comput. Sci., pages 328-344. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-63139-4_19.
  31. Manfred Schmidt-Schauß and David Sabel. Unification of program expressions with recursive bindings. In James Cheney and German Vidal, editors, Proc. PPDP 2016, pages 160-173. ACM, 2016. URL: http://dx.doi.org/10.1145/2967973.2968603.
  32. Manfred Schmidt-Schauß and David Sabel. Nominal unification with atom and context variables - report version. Frank report 59, Institut für Informatik, Goethe-Universität Frankfurt am Main, 2018. URL: http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:hebis:30:3-452767.
  33. Manfred Schmidt-Schauß, David Sabel, and Yunus Kutz. Nominal unification with atom-variables. J. Symbolic Comput., 2018. to appear. URL: http://dx.doi.org/10.1016/j.jsc.2018.04.003.
  34. Manfred Schmidt-Schauß, Marko Schütz, and David Sabel. Safety of Nöcker’s strictness analysis. J. Funct. Programming, 18(04):503-551, 2008. URL: http://dx.doi.org/10.1017/S0956796807006624.
  35. Christian Urban. Nominal techniques in Isabelle/HOL. J. Autom. Reasoning, 40(4):327-356, 2008. URL: http://dx.doi.org/10.1007/s10817-008-9097-2.
  36. Christian Urban and Cezary Kaliszyk. General bindings and alpha-equivalence in nominal Isabelle. Log. Methods Comput. Sci., 8(2), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(2:14)2012.
  37. Christian Urban, Andrew M. Pitts, and Murdoch Gabbay. Nominal unification. In Proc. CSL 2003, EACSL 2003, and KGC 2003, volume 2803 of Lect. Notes Comput. Sci., pages 513-527. Springer, 2003. URL: http://dx.doi.org/10.1007/978-3-540-45220-1_41.
  38. Joe B. Wells, Detlef Plump, and Fairouz Kamareddine. Diagrams for meaning preservation. In Robert Nieuwenhuis, editor, Proc. RTA 2003, volume 2706 of Lect. Notes Comput. Sci., pages 88-106. Springer, 2003. URL: http://dx.doi.org/10.1007/3-540-44881-0_8.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact