Problem #90
Originator: Hubert Comon, Manfred Schmidt-Schauß, Jordi Levy [Com91], [SS94], [Lev96]
Date: September 1991, 1994, July 1996
Summary:
Are context unification and
linear second order unification decidable?
Context unification and linear second order unification
are closely related, they both generalize string unification
(which is known to be decidable, [Mak77])
and are special cases of second order unification
(which is know to be undecidable, [Gol81]).
Context unification ([Com91], [SS94]) is
unification of first-order terms with context variables that range
over terms with one hole.
Linear Second Order Unification is second-order unification where
the domain of functions is restricted to λ-terms with exactly
one occurrence of any bound variable (there can be several bound variables
in contrast to context unification allowing for just one hole)
Applications are
-
solving membership constraints in completion of contraint rewriting
([Com98a])
- solving constraints occurring in Distributive Unification
(Problem #38, [SS97])
- Extended Critical Pairs in Bi-Rewriting Systems
([LA96])
- Semantics of ellipses in natural language
([NPR97])
- One-Step Rewriting constraints
([NPR97])
Some special cases have been solved:
-
Hubert Comon [Com98b] solved a special case where
any occurrence of the same context variable is always applied
to the same term,
- Manfred Schmidt-Schauß [SS94] (see also
[SS97]) solved the case of so-called
stratified context unification, where for any occurrence
of the same second-order variable the string of
second-order variables from this occurrence to the root of the
containing term is the same,
- Jordi Levy [Lev96] (see also [NPR97])
showed that linear-second order
unification is decidable when any variable has at most two
occurrences.
- Manfred Schmidt-Schauß and Klaus Schulz [SSS99a]
showed that solvability is decidable for systems of
context equations containing only two context variables (having
an arbitrary number of occurrences in the system) and an
arbitray number of first-order variables.
Progress towards a decidability proof along the lines of Makanin’s proof for
string-unification has been reported in [SSS98]. Levy and
Villaret [LV00] show how to reduce linear second-order unification
to context unification plus membership predicates in regular tree languages,
and discuss a possible way of showing decidability of the latter.
[LV02] shows that it is sufficient, both for linear 2nd-order and
for context unification, to consider signatures consisting of an arbitrary
number of constants and one binary function symbol.
References
-
[Com91]
-
Hubert Comon.
Completion of rewrite systems with membership constraints.
Rapport de Recherche 699, L.R.I., Université de Paris-Sud,
September 1991.
- [Com98a]
-
Hubert Comon.
Completion of rewrite systems with membership constraints. Part
I: Deduction rules.
Journal of Symbolic
Computation, 25:397–419, 1998.
- [Com98b]
-
Hubert Comon.
Completion of rewrite systems with membership constraints. Part
II: Constraint solving.
Journal of Symbolic
Computation, 25:421–453, 1998.
- [Gol81]
-
Warren D. Goldfarb.
The undecidability of the second-order unification problem.
Theoretical Computer
Science, 13:225–230, 1981.
- [LA96]
-
Jordi Levy and Jaume Agustí.
Bi-rewriting systems.
Journal of Symbolic
Computation, 22(3):279–314, September 1996.
- [Lev96]
-
Jordi Levy.
Linear second-order unification.
In Harald Ganzinger, editor, 7th International Conference on
Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer
Science, pages 332–346, New Brunswick, NJ, USA, July 1996.
Springer-Verlag.
- [LV00]
-
Jordi Levy and Mateu Villaret.
Linear second-order unification and context unification with
tree-regular constraints.
In Leo Bachmair, editor, Rewriting Techniques and
Applications, volume 1833 of Lecture Notes in Computer
Science, pages 156–171, Norwich, UK, July 2000.
Springer-Verlag.
- [LV02]
-
Jordi Levy and Mateu Villaret.
Currying second-order unification problems.
In Sophie Tison, editor, Rewriting Techniques and Applications,
volume 2378 of Lecture Notes in Computer
Science, pages 326–339, Copenhagen, Denmark, July 2002.
Springer-Verlag.
- [Mak77]
-
G. S. Makanin.
The problem of solvability of equations in a free semi-group.
Math. USSR Sbornik, 32(2):129–198, 1977.
- [NPR97]
-
Joachim Niehren, Manfred Pinkal, and Peter Ruhrberg.
On equality up-to constraints over finite trees, context unification
and one-step rewriting.
In William McClune, editor, 14th International Conference on
Automated Deduction, volume 1249 of Lecture Notes in
Artificial Intelligence, pages 34–48, Townsville, Australia, July 1997.
Springer-Verlag.
- [SS94]
-
Manfred Schmidt-Schauß.
Unification of stratified second-order terms.
Internal Report 12/94, Johann-Wolfgang-Goethe-Universität,
Frankfurt, Germany, 1994.
- [SS97]
-
Manfred Schmidt-Schauß.
A unification algorithm for distributivity and a multiplicative unit.
Journal of Symbolic
Computation, 22(3):315–344, 1997.
- [SSS98]
-
Manfred Schmidt-Schauß and Klaus Schulz.
On the exponent of peridicity of minimal solutions of context
equations.
In Tobias Nipkow, editor, 9th International Conference on
Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer
Science, pages 61–75, Tsukuba, Japan, April 1998.
Springer-Verlag.
- [SSS99a]
-
Manfred Schmidt-Schauß and Klaus Schulz.
Solvability of context unification with two context variables is
decidable.
In Harald Ganzinger, editor, 16th International Conference on
Automated Deduction, volume 1632 of Lecture Notes in
Artificial Intelligence, pages 67–81, Trento, Italy, July 1999.
Springer-Verlag.
Complete version as [SSS99b].
- [SSS99b]
-
Manfred Schmidt-Schauß and Klaus Schulz.
Solvability of context unification with two context variables is decidable.
CIS-Report 98-114, CIS, Universität München, München, Germany,
1999.