Document Open Access Logo

Two-Restricted One Context Unification is in Polynomial Time

Authors Adrià Gascón, Manfred Schmidt-Schauß, Ashish Tiwari

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.405.pdf
  • Filesize: 0.61 MB
  • 18 pages

Document Identifiers

Author Details

Adrià Gascón
Manfred Schmidt-Schauß
Ashish Tiwari

Cite As Get BibTex

Adrià Gascón, Manfred Schmidt-Schauß, and Ashish Tiwari. Two-Restricted One Context Unification is in Polynomial Time. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 405-422, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.405

Abstract

One Context Unification (1CU) extends first-order unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several more-general classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of first-order unification and can be used to solve related problems in polynomial time, such as first-order unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs.

Subject Classification

Keywords
  • context unification
  • first-order unification
  • deduction
  • type checking

Metrics

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

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, New York, NY, USA, 1998. Google Scholar
  2. F. Baader and W. Snyder. Unification theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 445-532. Elsevier and MIT Press, 2001. Google Scholar
  3. H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree Automata Techniques and Applications. Available on: http://www.grappa.univ-lille3.fr/tata, 2007. release October, 12th 2007.
  4. C. Creus, A. Gascón, and G. Godoy. One-context Unification with STG-Compressed Terms is in NP. In RTA, pages 149-164, 2012. Google Scholar
  5. S. Schulze Frielinghaus and H. Seidl M. Petter. Inter-procedural Two-variable herbrand Equalities. In Proc. Symp. Programming, ESOP, LNCS 9032, pages 457-482, 2015. Google Scholar
  6. A. Gascón, G. Godoy, and M. Schmidt-Schauß. Context Matching for Compressed Terms. In LICS, pages 93-102, 2008. Google Scholar
  7. A. Gascón, G. Godoy, and M. Schmidt-Schauß. Unification and Matching on Compressed Terms. ACM Trans. Comput. Log., 12(4):26, 2011. Google Scholar
  8. A. Gascón, G. Godoy, M. Schmidt-Schauß, and A. Tiwari. Context Unification with One Context Variable. J. Symb. Comput., 45(2):173-193, 2010. Google Scholar
  9. A. Gascón, M. Schmidt-Schauß, and A. Tiwari. One Context Unification Problems Solvable in Polynomial Time. In LICS, 2015. To appear. Google Scholar
  10. W. D. Goldfarb. The Undecidability of the Second-Order Unification Problem. Theor. Comput. Sci., 13:225-230, 1981. Google Scholar
  11. S. Gulwani and A. Tiwari. Computing procedure summaries for interprocedural analysis. In ESOP, pages 253-267, 2007. Google Scholar
  12. A. Jeż. Context unification is in PSPACE. In ICALP, pages 244-255, 2014. Google Scholar
  13. J. Levy, M. Schmidt-Schauß, and M. Villaret. Monadic Second-Order Unification is NP-Complete. In RTA, pages 55-69, 2004. Google Scholar
  14. J. Levy, M. Schmidt-Schauß, and M. Villaret. Bounded Second-Order Unification is NP-complete. In RTA, pages 400-414, 2006. Google Scholar
  15. J. Levy, M. Schmidt-Schauß, and M. Villaret. Stratified Context Unification is NP-complete. In IJCAR, pages 82-96, 2006. Google Scholar
  16. J. Levy, M. Schmidt-Schauß, and M. Villaret. The Complexity of Monadic Second-Order Unification. SIAM J. Comput., 38(3):1113-1140, 2008. Google Scholar
  17. J. Levy, M. Schmidt-Schauß, and M. Villaret. On the complexity of Bounded Second-Order Unification and Stratified Context Unification. Logic Journal (IGPL), 19(6):763-789, 2011. Google Scholar
  18. M. Lohrey. Algorithmics on SLP-compressed strings: A survey. Groups Complexity Cryptology, 4(2):241-299, 2012. Google Scholar
  19. M. S. Paterson and M. N. Wegman. Linear unification. J. of Computer and System Sciences, 16:158-167, 1978. Google Scholar
  20. M. Schmidt-Schauß and K. U. Schulz. Solvability of Context Equations with Two Context Variables is Decidable. J. Symb. Comput., 33(1):77-122, 2002. Google Scholar
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 About DROPS Imprint Privacy Contact