1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
\documentclass[11pt]{article}
\usepackage{a4}
\usepackage{hevea}
\begin{document}
\setlength{\parskip}{6pt}
\setlength{\parindent}{0pt}
\section*{Context Unification}
\begin{abstract}
Are {\em context unification} and
{\em linear second order unification} decidable?
\end{abstract}
{\em Context unification} and {\em linear second order unification}
are closely related, they both generalize string unification
(which is known to be decidable, \cite{Makanin:77})
and are special cases of second order unification
(which is know to be undecidable, \cite{Goldfarb:tcs81}).
Context unification (\cite{Comon:rr699}, \cite{Schauss:rr94-12}) 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 $\lambda$-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
\begin{itemize}
\item solving membership constraints in completion of contraint rewriting
(\cite{Comon:rr699}, \cite{Comon:icalp92})
\item solving constraints occurring in Distributive Unification
(\cite{schmidt-schauss:jsc97})
\item Extended Critical Pairs in Bi-Rewriting Systems
(\cite{LevyAgust:jsc96})
\item Semantics of ellipses in natural language
(\cite{Niehren:cade97})
\item One-Step Rewriting constraints
(\cite{Niehren:cade97})
\end{itemize}
Some special cases have been solved:
\begin{itemize}
\item Hubert Comon \cite{Comon:rr699} solved a special case where
any occurrence of the same context variable is always applied
to the same term,
\item Manfred Schmidt-Schau{\ss} \cite{Schauss:rr94-12} (see also
\cite{schmidt-schauss:jsc97}) solved the case of so-called
{\em 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,
\item Jordi Levy \cite{Levy:rta96} (see also \cite{Niehren:cade97})
showed that linear-second order
unification is decidable when any variable has at most two
occurrences.
\item Manfred Schmidt-Schau{\ss} and Klaus Schulz \cite{Schauss:cade99}
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.
\end{itemize}
Progress towards a decidability proof along the lines
of Makanin's proof for string-unification has been reported
in~\cite{schmidt-schauss:rta98}. Levy and Villaret \cite{Levy:rta00}
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.
\nocite{Schauss:cisrep99}
\bibliographystyle{alpha}
\bibliography{rewriting}
\end{document}
|
