Left-linear Semi-unification (LLSU)

Input

A set of pairs of terms $S = \{(M_1, N_1), \ldots, (M_k, N_k)\}$ that is left linear.

Problem

Is $S$ semi-unifiable?

Definitions

We follow the discussion given in [1] for definitions. A ranked alphabet $A = (F, a)$ is a finite set $F$ of function symbols together with an arity function $a$ that maps every element in $F$ to a natural number. A function symbol of arity 0 is called a constant. The set of variables $V$ is a denumerable infinite set that is disjoint from $F$. The terms over $A$ and $V$ is the set $T(A, V)$ consisting of all strings generated by the grammar $$M \to x \mid c \mid f(M, \ldots, M),$$ where $f$ is a function symbol from $A$ with arity $k$ greater than 0, $c$ is a constant, $x$ is any variable from $V$, and $M$ appears $k$ times as an argument to $f$.

Two terms $M$ and $N$ are equal, written $M = N$, if and only if they are identical as strings. A substitution $\sigma$ is a mapping from $V$ to $T(A, V)$ that is the identity on all but a finite set of $V$. The set of variables on which $\sigma$ is not the identity is the domain of $\sigma$. Every substitution $\sigma : V \to T(A, V)$ can be extended to $\sigma : T(A, V) \to T(A, V)$ by defining $$\sigma(f(M_1, \ldots, M_k)) = f(\sigma(M_1), \ldots, \sigma(M_k)).$$

A term $M$ subsumes $N$, written $M \leq N$, if there is a substitution $\rho$ such that $\rho(M) = N$. Given $S$ a substitution $\sigma$ is a semi-unifier of $S$ if $$\sigma(M_1) \leq \sigma(N_1), \ldots, \sigma(M_k) \leq \sigma(N_k).$$

Set $S$ is semi-unifiable if it has a semi-unifier.

Status

$\P$-complete (Henglein [2]).

Remarks

The proof is adapted from the one for UNIF [3], so it is from MCVP.

Define $k$LLSU to be the problem of left-linear semiunifiability with exactly $k$ term inequalities (same $k$ as above) and Monadic Semi-unification (MSU) to be the problem of semiunifiability for the alphabet $A = (F, a)$, where $a(f)$ is greater than or equal to 1 for all $f \in F$ and $a(f)$ equals 1 for at least one $f$.

2LLSU and MSU are $\P$-complete [1]. See Problem UNIF for related problems. Also see 1LLSU for an open problem.