Problem #90
Originator: Hubert Comon, Manfred SchmidtSchauß, 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 firstorder terms with context variables that range
over terms with one hole.
Linear Second Order Unification is secondorder 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 BiRewriting Systems
([LA96])
 Semantics of ellipses in natural language
([NPR97])
 OneStep 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 SchmidtSchauß [SS94] (see also
[SS97]) solved the case of socalled
stratified context unification, where for any occurrence
of the same secondorder variable the string of
secondorder variables from this occurrence to the root of the
containing term is the same,
 Jordi Levy [Lev96] (see also [NPR97])
showed that linearsecond order
unification is decidable when any variable has at most two
occurrences.
 Manfred SchmidtSchauß 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 firstorder variables.
Progress towards a decidability proof along the lines of Makanin’s proof for
stringunification has been reported in [SSS98]. Levy and
Villaret [LV00] show how to reduce linear secondorder 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 2ndorder 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 ParisSud,
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 secondorder unification problem.
Theoretical Computer
Science, 13:225–230, 1981.
 [LA96]

Jordi Levy and Jaume Agustí.
Birewriting systems.
Journal of Symbolic
Computation, 22(3):279–314, September 1996.
 [Lev96]

Jordi Levy.
Linear secondorder 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.
SpringerVerlag.
 [LV00]

Jordi Levy and Mateu Villaret.
Linear secondorder unification and context unification with
treeregular constraints.
In Leo Bachmair, editor, Rewriting Techniques and
Applications, volume 1833 of Lecture Notes in Computer
Science, pages 156–171, Norwich, UK, July 2000.
SpringerVerlag.
 [LV02]

Jordi Levy and Mateu Villaret.
Currying secondorder 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.
SpringerVerlag.
 [Mak77]

G. S. Makanin.
The problem of solvability of equations in a free semigroup.
Math. USSR Sbornik, 32(2):129–198, 1977.
 [NPR97]

Joachim Niehren, Manfred Pinkal, and Peter Ruhrberg.
On equality upto constraints over finite trees, context unification
and onestep 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.
SpringerVerlag.
 [SS94]

Manfred SchmidtSchauß.
Unification of stratified secondorder terms.
Internal Report 12/94, JohannWolfgangGoetheUniversität,
Frankfurt, Germany, 1994.
 [SS97]

Manfred SchmidtSchauß.
A unification algorithm for distributivity and a multiplicative unit.
Journal of Symbolic
Computation, 22(3):315–344, 1997.
 [SSS98]

Manfred SchmidtSchauß 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.
SpringerVerlag.
 [SSS99a]

Manfred SchmidtSchauß 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.
SpringerVerlag.
Complete version as [SSS99b].
 [SSS99b]

Manfred SchmidtSchauß and Klaus Schulz.
Solvability of context unification with two context variables is decidable.
CISReport 98114, CIS, Universität München, München, Germany,
1999.