On Asymmetric Unification for the Theory of XOR with a Homomorphism

TL;DR

This paper develops a new automata-based decision procedure for asymmetric unification in the XOR theory with a homomorphism, addressing a gap in algorithms for cryptographic protocol analysis.

Contribution

It introduces a novel automata-based decision procedure for asymmetric unification in ACUNh and adapts existing methods to improve analysis capabilities.

Findings

Developed a new automata-based decision procedure for asymmetric-ACUNh.

Adapted asymmetric combination procedures for improved unification.

Compared new approach with variant unification methods.

Abstract

Asymmetric unification, or unification with irreducibility constraints, is a newly developed paradigm that arose out of the automated analysis of cryptographic protocols. However, there are still relatively few asymmetric unification algorithms. In this paper we address this lack by exploring the application of automata-based unification methods. We examine the theory of xor with a homomorphism, ACUNh, from the point of view of asymmetric unification, and develop a new automata-based decision procedure. Then, we adapt a recently developed asymmetric combination procedure to produce a general asymmetric- ACUNh decision procedure. Finally, we present a new approach for obtaining a solution-generating asymmetric-ACUNh unification automaton. We also compare our approach to the most commonly used form of asymmetric unification available today, variant unification.

Full text

1 Introduction

We examine the newly developed paradigm of asymmetric unification in the theory of xor with a homomorphism. Asymmetric unification is motivated by requirements arising from symbolic cryptographic protocol analysis [6]. These symbolic analysis methods require unification-based exploration of a space in which the states obey rich equational theories that can be expressed as a decomposition $R\uplus\Delta$ , where $R$ is a set of rewrite rules that is confluent, terminating, and coherent modulo $\Delta$. However, in order to apply state space reduction techniques, it is usually necessary for at least part of this state to be in normal form, and to remain in normal form even after unification is performed. This requirement can be expressed as an asymmetric unification problem $\{s_{1}=_{\downarrow}t_{1},~{}\ldots,~{}s_{n}=_{\downarrow}t_{n}\}$ where the $=_{\downarrow}$ denotes a unification problem with the restriction that any unifier leaves the right-hand side of each equation irreducible.

At this point there are relatively few such algorithms. Thus in most cases when asymmetric unification is needed, an algorithm based on variant unification [8] is used. Variant unification turns an $R\uplus\Delta$-problem into a set of $\Delta$-problems. Application of variant unification requires that a number of conditions on the decomposition be satisfied. In particular, the set of $\Delta$-problems produced must always be finite (this is equivalent to the finite variant property [4]) and $\Delta$-unification must be decidable and finitary. Unfortunately, there is a class of theories commonly occurring in cryptographic protocols that do not have decompositions satisfying these necessary conditions: theories including an operator $h$ that is homomorphic over an Abelian group operator $+$, that is $AGh$. There are a number of cryptosystems that include an operation that is homomorphic over an Abelian group operator, and a number of constructions that rely on this homomorphic property. These include for example RSA [12], whose homomorphic property is used in Chaum’s blind signatures [3], and Pallier cryptosystems [11], used in electronic voting and digital cash protocols. Thus an alternative approach is called for.

In this paper we concentrate on asymmetric unification for a special case of $AGh$: the theory of xor with homomorphism, or $ACUNh$. We first develop an automata-based $ACUNh$-asymmetric decision procedure. We then apply a recently developed combination procedure for asymmetric unification algorithms to obtain a general asymmetric decision procedure allowing for free function symbols. This requires a non-trivial adaptation of the combination procedure, which originally required that the algorithms combined were not only decision procedures but produced complete sets of unifiers. In addition, the decomposition of $ACUNh$ we use is $\Delta=ACh$. It is known that unification modulo $ACh$ is undecidable [10], so our result also yields the first asymmetric decision procedure for which $\Delta$ does not have a decidable finitary unification algorithm.

We then consider the problem of producing complete sets of asymmetric unifiers for $ACUNh$. We show how the decision procedure developed in this paper can be adapted to produce an automaton that generates a (possibly infinite) complete set of solutions. We then show, via an example, that asymmetric unification modulo $ACUNh$ is not finitary.

1.1 Outline

Section 2 provides a brief description of preliminaries. Section 3 develops an automaton based decision procedure for the $ACUNh$-theory. In Section 4 an automaton approach that produces substitutions is outlined. Section 5 develops the modified combination method needed to obtain general asymmetric algorithms. In Section 6 we conclude the paper and discuss further work.

2 Preliminaries

We use the standard notation of equational unification [1] and term rewriting systems [1].$\Sigma$-terms, denoted by $T(\Sigma,$ $\mathcal{X})$, are built over the signature $\Sigma$ and the (countably infinite) set of variables $\mathcal{X}$. The terms $t|_{p}$ and $t[u]_{p}$ denote respectively the subterm of $t$ at the position $p$, and the term $t$ having $u$ as subterm at position $p$. The symbol of $t$ occurring at the position $p$ (resp. the top symbol of $t$) is written $t(p)$ (resp. $t(\epsilon)$). The set of positions of a term $t$ is denoted by $Pos(t)$, the set of non variable positions for a term $t$ over a signature $\Sigma$ is denoted by $Pos(t)_{\Sigma}$. A $\Sigma$-rooted term is a term whose top symbol is in $\Sigma$. The set of variables of a term $t$ is denoted by $Var(t)$. A term is ground if it contains no variables.

Definition 1

Let $\Gamma$ be an $E$-unification problem, let $\mathcal{X}$ denote the set of variables occurring in $\Gamma$ and $\mathcal{C}$ the set of free constants occurring in $\Gamma$. For a given linear ordering $<$ on $\mathcal{X}\cup\mathcal{C}$, and for each $c\in\mathcal{C}$ define the set $V_{c}$ as $\{x~{}|~{}x\text{ is a variable with }x<c\}$. An $E$-unification problem with linear constant restriction (LCR) is an $E$-unification problem with constants, $\Gamma$, where each constant $c$ in $\Gamma$ is equipped with a set $V_{c}$ of variables. A solution of the problem is an $E$-unifier $\sigma$ of $\Gamma$ such that for all $c,x$ with $x\in V_{c}$, the constant $c$ does not occur in $x\sigma$. We call $\sigma$ an $E$-unifier with LCR.

A rewrite rule is an ordered pair $l\rightarrow r$ such that $l,r\in T(\Sigma,\mathcal{X})$ and $l\not\in\mathcal{X}$. We use $R$ to denote a term rewrite system which is defined as a set of rewrite rules. The rewrite relation on $T(\Sigma,\mathcal{X})$, written $t\rightarrow_{R}s$, hold between $t$ and $s$ iff there exists a non-variable $p\in Pos_{\Sigma}(t)$, $l\rightarrow r\in R$ and a substitution $\sigma$, such that $t|_{p}=l\sigma$ and $s=t[r\sigma]_{p}$. The relation $\rightarrow_{R/E}$ on $T(\Sigma,\mathcal{X})$ is $=_{E}\circ\rightarrow_{R}\circ=_{E}$. The relation $\rightarrow_{R,E}$ on $T(\Sigma,\mathcal{X})$ is defined as: $t\rightarrow_{R,E}t^{\prime}$ if there exists a position $p\in Pos_{\Sigma}(t)$, a rule $l\rightarrow r\in R$ and a substitution $\sigma$ such that $t|_{p}=_{E}l\sigma$ and $t^{\prime}=t[r\sigma]_{p}$. The transitive (resp. transitive and reflexive) closure of $\rightarrow_{R,E}$ is denoted by $\rightarrow^{+}_{R,E}$ (resp. $\rightarrow^{*}_{R,E}$). A term $t$ is $\rightarrow_{R,E}$ irreducible (or in $R,E$-normal form) if there is no term $t^{\prime}$ such that $t\rightarrow_{R,E}t^{\prime}$. If $\rightarrow_{R,E}$ is confluent and terminating we denote the irreducible version of a term, $t$, by $t\downarrow_{R,E}$.

Definition 2

We call $(\Sigma,~{}E,~{}R)$ a weak decomposition of an equational theory $\Delta$ over a signature $\Sigma$ if $\Delta=R\uplus E$ and $R$ and $E$ satisfy the following conditions:

Matching modulo $E$ is decidable. 2. 2.

$R$ is terminating modulo $E$, i.e., the relation $\rightarrow_{R/E}$ is terminating. 3. 3.

The relation $\rightarrow_{R,E}$ is confluent and $E$-coherent, i.e., $\forall t_{1},t_{2},t_{3}$ if $t_{1}\rightarrow_{R,E}t_{2}$ and $t_{1}=_{E}t_{3}$ then $\exists~{}t_{4},t_{5}$ such that $t_{2}\rightarrow^{*}_{R,E}t_{4}$, $t_{3}\rightarrow^{+}_{R,E}t_{5}$, and $t_{4}=_{E}t_{5}$.

This definition is a modification of the definition in [6]. where asymmetric unification and the corresponding theory decomposition are first defined. The last restrictions ensure that $s\rightarrow^{!}_{R/E}t$ iff $s\rightarrow^{!}_{R,E}t$ (see [8, 6]).

Definition 3 (Asymmetric Unification)

Given a weak decomposition $(\Sigma,E,R)$ of an equational theory, a substitution $\sigma$ is an asymmetric $R,E$-unifier of a set $\mathcal{S}$ of asymmetric equations $\{s_{1}=_{\downarrow}t_{1},~{}\ldots,~{}s_{n}=_{\downarrow}t_{n}\}$ iff for each asymmetric equations $s_{i}=_{\downarrow}t_{i}$, $\sigma$ is an $(E\cup R)$-unifier of the equation $s_{i}=^{?}t_{i}$ and $(t_{i}\downarrow_{R,E})\sigma$ is in $R,E$-normal form. A set of substitutions $\Omega$ is a complete set of asymmetric $R,E$-unifiers of $\mathcal{S}$ (denoted $CSAU_{R\cup E}(\mathcal{S})$ or just $CSAU(\mathcal{S})$ if the background theory is clear) iff: (i) every member of $\Omega$ is an asymmetric $R,E$-unifier of $\mathcal{S}$, and (ii) for every asymmetric $R,E$-unifier $\theta$ of $\mathcal{S}$ there exists a $\sigma\in\Omega$ such that $\sigma\leq_{E}^{Var(\mathcal{S})}\theta$.

Example 1

Let $R=\{x\oplus 0\rightarrow x,~{}x\oplus x\rightarrow 0,~{}x\oplus x\oplus y\rightarrow y\}$ and $E$ be the $AC$ theory for $\oplus$. Consider the equation $y\oplus x=_{\downarrow}x\oplus a$, the substitution $\sigma_{1}=\{y\mapsto a\}$ is an asymmetric solution but, $\sigma_{2}=\{x\mapsto 0,~{}y\mapsto a\}$ is not.

Definition 4 (Asymmetric Unification with Linear Constant Restriction)

Let $\mathcal{S}$ be a set of asymmetric equations with some LCR. A substitution $\sigma$ is an asymmetric $R,E$-unifier of $\mathcal{S}$ with LCR iff $\sigma$ is an asymmetric solution to $\mathcal{S}$ and $\sigma$ satisfies the LCR.

Definition 5

Let $R$ be a term rewriting system and ${E}$ be a set of identities. We say $(R,E)$ is $R,E$-convergent if and only if

• (a)

$\rightarrow_{R,E}\,$ is terminating, and

• (b)

for all terms $s$, $t$, if $s\,\approx_{R\cup E}\,t$, there exist terms $s^{\prime}$, $t^{\prime}$ such that $s\,\rightarrow_{R,E}^{!}\,s^{\prime},\;t\,\rightarrow_{R,E}^{!}\,t^{\prime},\;\;\mathrm{and}\;\;s^{\prime}\,\approx_{E}\,t^{\prime}$

Definition 6

A term $t$ is an $R,\Delta$-normal form of a term $s$ if and only if $s\rightarrow_{R,\Delta}^{!}t$. This is often represented as t\,=\,s\!\big{\downarrow}_{R,\Delta}.

3 An Asymmetric $ACUNh$-unification Decision Procedure via an Automata

Approach

In this section we develop a new asymmetric unification algorithm for the theory $ACUNh$. The theory $ACUNh$ consists of the following identities: $x+x\approx 0,\;x+0\approx x,\;h(x+y)\approx h(x)+h(y),\;h(0)\approx 0,\;(x+y)+z\approx x+(y+z),\;x+y\approx y+x$

Following the definition of asymmetric unification, we first decompose the theory into a set of rewrite rules, $R$, modulo a set of equations, $\Delta$. Actually, there are two such decompositions possible. The first decomposition keeps $associativity$ and  $commutativity$ as identities ${\Delta}$ and the rest as rewrite rules. This decomposition has the following $AC$-convergent term rewriting system $R_{1}$: $x+x\rightarrow 0,\;$ $x+0\rightarrow x,\;$ $x+(y+x)\rightarrow y,\;$ $h(x+y)\rightarrow h(x)+h(y),\;$ $h(0)\rightarrow 0$, as well as $R_{1}^{\prime}$: $x+x\rightarrow 0,\;x+0\rightarrow x,\;x+(y+x)\rightarrow y,\;h(x)+h(y)\rightarrow h(x+y),\;h(0)\rightarrow 0$ (when $+$ is given a higher precedence over $h$).

The second decomposition has $associativity$, $commutativity$ and the distributive homomorphism identity as $\Delta$ 111This is the background theory., i.e., $\Delta=ACh$. Our goal here is to prove that the following term rewriting system $R_{2}$: $x+x\rightarrow 0,\;$ $x+0\rightarrow x,\;$ $x+(y+x)\rightarrow y,\;$ $h(0)\rightarrow 0$ is $ACh$-convergent. The proof for convergence of $\rightarrow_{R_{2},\,ACh}$ is provided in Appendix $A$.

Decidability of asymmetric unification for the theory $R_{2}$, $ACh$ can be shown by automata -theoretic methods analogous to the method used for deciding the Weak Second Order Theory of One successor (WS1S) [5, 2]. In WS1S we consider quantification over finite sets of natural numbers, along with one successor function. All equations or formulas are transformed into finite-state automata which accepts the strings that correspond to a model of the formula [9, 13]. This automata-based approach is key to showing decidability of WS1S, since the satisfiability of WS1S formulas reduces to the automata intersection-emptiness problem. We follow the same approach here.

To be precise, what we show here is that ground solvability of asymmetric unification, for a given set of constants, is decidable. We explain at the end of this section why this is equivalent to solvability in general, in Lemma 3.1 and Lemma 3.2.

Problems with one constant

: For ease of exposition, let us consider the case where there is only one constant $a$. Thus every ground term can be represented as a set of natural numbers. The homomorphism $\mathsf{h}$ is treated as a successor function. Just as in WS1S, the input to the automata are column vectors of bits. The length of each column vector is the number of variables in the problem. $\Sigma=\left\{\vphantom{b^{b}}\begin{pmatrix}0\\ 0\\ \vdots\\ 0\end{pmatrix},\ldots,\begin{pmatrix}1\\ 1\\ \vdots\\ 1\end{pmatrix}\right\}$. The deterministic finite automata (DFA) are illustrated here. The $\mathsf{+}$ operator behaves like the symmetric set difference operator.

We illustrate how an automaton is constructed for each equation in standard form. In order to avoid cluttering up the diagrams the dead state has been included only for the first automaton. The missing transitions lead to the dead state by default for the others. Recall that we are considering the case of one constant $a$.

$\bf{Fig.~{}\ref{fig:M1}}$: Let $\mathsf{P_{i},Q_{i}}\text{ and }\mathsf{R_{i}}$ denote the ${i^{th}}$ bits of $\mathsf{P,Q}\text{ and }\mathsf{R}\;respectively$. $\mathsf{P_{i}}$ has a value 1, when either $\mathsf{Q_{i}}$ or $\mathsf{R_{i}}$ has a value 1. We need 3-bit alphabet symbols for this equation. The input for this automaton are column vectors of 3-bits each, i.e., $\Sigma=\{\begin{pmatrix}0\\ 0\\ 0\end{pmatrix},\cdots,\begin{pmatrix}1\\ 1\\ 1\end{pmatrix}\}$. For example, if $\mathsf{R_{2}}$ = 0, $\mathsf{Q_{2}}$ = 1, then $\mathsf{P_{2}}$ = 1. The corresponding alphabet symbol is $\begin{pmatrix}P_{2}\\ Q_{2}\\ R_{2}\end{pmatrix}$ = $\begin{pmatrix}1\\ 0\\ 1\end{pmatrix}$. Hence, only strings with the alphabet symbols $\{$ $\begin{pmatrix}0\\ 0\\ 0\end{pmatrix},\begin{pmatrix}0\\ 1\\ 1\end{pmatrix},\begin{pmatrix}1\\ 0\\ 1\end{pmatrix},\begin{pmatrix}1\\ 1\\ 0\end{pmatrix}$ $\}$ are accepted by this automaton. The rest of the input symbols $\{$ $\begin{pmatrix}0\\ 0\\ 1\end{pmatrix},\begin{pmatrix}1\\ 1\\ 1\end{pmatrix},\begin{pmatrix}0\\ 1\\ 0\end{pmatrix},\begin{pmatrix}1\\ 0\\ 0\end{pmatrix}$ $\}$ go to the dead state $D$, as they violate the XOR property. Note that the string $\begin{pmatrix}1\\ 0\\ 1\end{pmatrix}\begin{pmatrix}1\\ 1\\ 0\end{pmatrix}$ is accepted by this automaton. This corresponds to $\mathsf{P=a+h(a)}$, $\mathsf{Q=h(a)}$ and $\mathsf{R=a}$.

$\bf{Fig.~{}\ref{fig:M2}}$: To preserve asymmetry on the right-hand side of this equation, $\mathsf{Q+R}$ should be irreducible. If either $\mathsf{Q}$ or $\mathsf{R}$ is empty, or if they have any term in common, then a reduction will occur. For example, if $\mathsf{Q}$ = $\mathsf{h(a)}$ and $\mathsf{R}$ = $\mathsf{h(a)+a}$, there is a reduction, whereas if $\mathsf{R}$ = $\mathsf{h(a)}$ and $\mathsf{Q}$ = $\mathsf{a}$, irreducibility is preserved, since there is no common term and neither one is empty. Since neither $\mathsf{Q}$ nor $\mathsf{R}$ can be empty, any accepted string should have one occurrence of $\begin{pmatrix}1\\ 0\\ 1\end{pmatrix}$ and one occurrence of $\begin{pmatrix}1\\ 1\\ 0\end{pmatrix}$.

$\bf{Fig.~{}\ref{fig:M3}}$: We need 2-bit vectors as alphabet symbols since we have two unknowns $\mathsf{X}$ and $\mathsf{Y}$. Remember that $\mathsf{h}$ acts like the successor function. $q_{0}$ is the only accepting state. A state transition occurs with bit vectors $\begin{pmatrix}1\\ 0\end{pmatrix},\begin{pmatrix}0\\ 1\end{pmatrix}$. If $\mathsf{Y}$=1 in current state, then $\mathsf{X}$=1 in the next state, hence a transition occurs from $\mathsf{q_{0}}$ to $\mathsf{q_{1}}$, and vice versa. The ordering of variables is $\begin{pmatrix}Y\\ X\end{pmatrix}$.

$\bf{Fig.~{}\ref{fig:M4}}$: In this equation, $\mathsf{h(Y)}$ should be in normal form. So $\mathsf{Y}$ cannot be 0, but can contain terms of the form $\mathsf{u+v}$. $\begin{pmatrix}Y\\ X\end{pmatrix}$ is the ordering of variables. Therefore the bit vector $\begin{pmatrix}1\\ 0\end{pmatrix}$ should be succeeded by $\begin{pmatrix}0\\ 1\end{pmatrix}$, with possible occurrences of the bit vector $\begin{pmatrix}1\\ 1\end{pmatrix}$ in between. Thus the string either ends with $\begin{pmatrix}0\\ 1\end{pmatrix}$ or $\begin{pmatrix}0\\ 0\end{pmatrix}$. For example, if $\mathsf{Y}$ = $\mathsf{h(a)+a}$, then $\mathsf{X}$ = $\mathsf{h^{2}(a)+h(a)}$, which results in the string \begin{pmatrix}1\\ 0\end{pmatrix}$$\begin{pmatrix}1\\ 1\end{pmatrix}$$\begin{pmatrix}0\\ 1\end{pmatrix} is accepted by this automaton.

$\bf{Fig.~{}\ref{fig:M4a}}$: This automaton represents the disequality $\mathsf{X^{a}\not=Y^{a}}$. In general, if there are two or more constants, we have to guess which components are not equal. This enables us to handle the disequality constraints mentioned in the next section.

$\bf{Fig.~{}\ref{fig:M4b}}$: This automaton represents the disequality $\mathsf{X\not=a}$, where $a$ is a constant.

Example 2

Let \Big{\{}U=_{\downarrow}V+Y,\;W=h(V),\;Y=_{\downarrow}h(W)\Big{\}} be an asymmetric unification problem. We need 4-bit vectors and 3 automata since we have 4 unknowns in 3 equations, with bit-vectors represented in this ordering of set variables: $\begin{pmatrix}V\\ W\\ Y\\ U\end{pmatrix}$. We include the $\times$ (“don’t-care”) symbol in state transitions to indicate that the values can be either [math] or $1$. This is done to avoid cluttering the diagrams. Note that here this $\times$ symbol is a placeholder for the variables which do not have any significance in a given automaton. The automata constructed for this example are indicated in $\bf{Fig.~{}\ref{fig:M5}}$, $\bf{Fig.~{}\ref{fig:M6}}$ and $\bf{Fig.~{}\ref{fig:M7}}$. The string \begin{pmatrix}1\\ 0\\ 0\\ 1\end{pmatrix}$$\begin{pmatrix}0\\ 1\\ 0\\ 0\end{pmatrix}$$\begin{pmatrix}0\\ 0\\ 1\\ 1\end{pmatrix}$$\begin{pmatrix}0\\ 0\\ 0\\ 0\end{pmatrix} is accepted by all the three automata. The corresponding asymmetric unifier is $\{V\mapsto a,\,W\mapsto h(a),\,Y\mapsto h^{2}(a),\,U\mapsto(h^{2}(a)+a)\}.$

Once we have automata constructed for all the formulas, we take the intersection and check if there exists a string accepted by all the automata. If the intersection is not empty, then we have a solution or an asymmetric unifier for the given problem.

Problems with more than one constant

: This technique can be extended to the case where we have more than one constant. Suppose we have $k$ constants, say $c_{1},\ldots,c_{k}$. We express each variable $X$ in terms of the constants as follows: $X~{}=~{}X^{c_{1}}+\ldots+X^{c_{k}}$. For example, if $\mathsf{Y}$ is a variable and $\mathsf{a,b,c}$ are the constants in the problem, then we create the equation $\mathsf{Y}$ = $\mathsf{Y^{a}+Y^{b}+Y^{c}}$.

If we have an equation $\mathsf{X=h(Y)}$ with constants $\mathsf{a,b,c}$, then we have equations $\mathsf{X^{a}=h(Y^{a})}$, $\mathsf{X^{b}=h(Y^{b})}$ and $\mathsf{X^{c}=h(Y^{c})}$. However, if it is an asymmetric equation $\mathsf{X=_{\downarrow}h(Y)}$ all $\mathsf{Y^{a}}$, $\mathsf{Y^{b}}$ and $\mathsf{Y^{c}}$ cannot be zeros simultaneously.

Similarly, if the equation to be solved is $\mathsf{X=W+Z}$, with $\mathsf{a,b,c}$ as constants, we form the equations $\mathsf{X^{a}=W^{a}+Z^{a}}$, $\mathsf{X^{b}=W^{b}+Z^{b}}$ and $\mathsf{X^{c}=W^{c}+Z^{c}}$ and solve the eq-uations. But if it is an asymmetric equation $\mathsf{X=_{\downarrow}W+Z}$ then we cannot have $\mathsf{W^{a}}$, $\mathsf{W^{b}}$, $\mathsf{W^{c}}$ to be all zero simultaneously, and similarly with $\mathsf{Z^{a}}$, $\mathsf{Z^{b}}$, $\mathsf{Z^{c}}$.

Our approach is to design a nondeterministic algorithm by guessing which constant component in each variable has to be [math], i.e., for each variable $Y$ and each constant $b$, we “flip a coin” as to whether $Y^{b}$ will be set equal to [math] by the target solution222The linear constant restrictions in Section 5 can also be handled this way: a constant restriction of the form $a\;\not\in\;X$ can be taken care of by setting $\mathsf{X^{a}}=0$. Now for the case $\mathsf{X=_{\downarrow}W+Z}$, we do the following:

[TABLE]

Similarly, for the case $\mathsf{X=_{\downarrow}h(Y)}$ we follow these steps:

[TABLE]

This is summarized in Algorithm 2. Thus, it follows that

Theorem 3.1

Algorithm 2 is a decision procedure for ground asymmetric unification modulo $(R_{2},\,ACh)$.

Proof

This holds by construction, as outlined in “Problems with only one constant” and “Problems with more than one constant”.

We now show that general asymmetric unification modulo $ACUNh$, where the solutions need not be ground solutions over the current set of constants, is decidable by showing that a general solution exists if and only if there is a ground solution in the extended signature where we add an extra constant.

We represent each term as a sum of terms of the form $h^{i}(\alpha)$ where $\alpha$ is either a constant or variable. The superscript (power) $i$ is referred to as the degree of the simple term $h^{i}(\alpha)$. The degree of a term is the maximum degree of its summands.

Lemma 3.1

Let $t$ be an irreducible term and $d$ be its degree. Let $\,\mathcal{V}ar(t)\;=\;\{X_{1},X_{2},$ …, $X_{n}\}$. Suppose $c$ is a constant that does not appear in $t$. Then for any $D>d$, $t\theta$ is irreducible, where \theta\;=\;\big{\{}X_{1}\mapsto c,\;X_{2}\mapsto h^{D}(c),\;X_{3}\mapsto h^{2D}(c),\;\ldots,\;X_{n}\mapsto h^{(n-1)(D)}(c)\big{\}}.

Lemma 3.2

Let \,\Gamma~{}=~{}\big{\{}s_{1}\,{\approx}_{\downarrow}^{?}\,t_{1},\ldots,s_{n}\,{\approx}_{\downarrow}^{?}\,t_{n}\big{\}} be an asymmetric unification problem. Let $\beta$ be an asymmetric unifier of $\Gamma$ and $V=\mathcal{V}\!\mathcal{R}an(\beta)=\{X_{1},\ldots X_{m}\}$. Let $D=1+\mathop{max}\limits_{1\leq i\leq n}degree(s_{i}\beta,t_{i}\beta)$, and $c$ be a constant that does not appear in $\Gamma$. Then \theta=\big{\{}X_{1}\mapsto c,\;X_{2}\mapsto h^{D}(c),\;\ldots,\;X_{m}\mapsto h^{(n-1)D}(c)\big{\}} is an asymmetric unifier of $\;\Gamma$.

General solutions over variables, without this extra constant $c$, can be enumerated by back-substituting (abstracting) terms of the form $h^{j}(c)$ and checking whether the obtained substitutions are indeed solutions to the problem.

The exact complexity of this problem is open.

4 Automaton to find a complete set of unifiers

In this section we create automata to find all solutions of an ACUNh asymmetric unification problem with constants. We also have linear constant restrictions and disequalities for combination. Our terms will be built from elements in the set described below.

Definition 7

Let $C$ be a set of constants and $X$ be a set of variables. Define $H(X,C)$ as the set $\{h^{i}(t)\,\,|\,\,t\in X\cup C\}$. We also define $H_{n}(X,C)$ as $\{h^{i}(t)\,\,|\,\,t\in X\cup C,i\leq n\}$. For any object $t$ we define $Const(t)$ to be the set of constants in $t$, except for 0. For an object $t$, define $H(t)=H(Var(t),Const(t))$ and $H_{n}(t)=H_{n}(Var(t),Const(t))$.

Terms are sums. We often need to talk about the multiset of terms in a sum.

Definition 8

Let $t$ be a term whose $R_{h}$ normal form is $t_{1}+\cdots+t_{n}$. Then we define $mset(t)=\{t_{1},\cdots,t_{n}\}$. Inversely, if $T=\{t_{1},\cdots,t_{n}\}$ then $\Sigma T=t_{1}+\cdots+t_{n}$.

A term in normal form modulo $R_{1}$ can be described as a sum in the following way.

Theorem 4.1

Let $t$ be a term in $R_{1}$ normal form. Then there exists an $H\subseteq H(t)$ such that $t=\Sigma H$.

Proof

Since $t$ is reduced by $h(x+y)\rightarrow h(x)+h(y)$, it cannot have an $h$ symbol above a $+$ symbol. So it must be a sum of terms of the form $h^{i}(s)$ where $i\geq 0$ and $s$ is a constant. Since $t$ is also reduced by $R_{2}$, there can be no duplicates in the sum.

We show that every substitution $\theta$ that is irreducible with respect to $R_{1}$, can be represented as a sequence of smaller substitutions, which we will later use to construct an automaton.

Definition 9

Let $\zeta$ be a substitution and $X$ be a set of variables. Then $\zeta$ is a zero substitution on $X$ if $Dom(\zeta)\subseteq X$ and $x\zeta=0$ for all $x\in Dom(\zeta)$.

Theorem 4.2

*Let $t$ be an object and $\theta$ be a ground substitution in $R_{1}$ normal form, such that $Dom(\theta)=Var(t)$. Let $m$ be the maximum degree in $mset(Ran(\theta))$ Then there are substitutions $\zeta$, $\theta_{0},\cdots,\theta_{m}$ such that *

$\zeta$* is a zero substitution on $Dom(\theta)$,* 2. 2.

$\zeta\theta_{0}\cdots\theta_{m}=\theta$*, * 3. 3.

$Dom(\theta_{i})=Var(t\zeta\theta_{0}\cdots\theta_{i-i})$** 4. 4.

for all $i$ and all variables $x$ in $Dom(\theta_{i})$, $x\theta_{i}=\Sigma T$ for some nonempty $T\subseteq Const($ Ran($\theta))\cup\{h(x)\}$*. *

Proof

By the previous theorem, we know that each $x\theta$ is a sum of $h$-terms or is 0. Then $\zeta$ and $\theta_{i}$ can be defined as follows, where $S^{x}=mset(x\theta)$ and ${S_{i}}^{x}$ is the set of terms in $S$ with degree $i$:

• •

If $x\theta=0$ then $x\zeta=0$ else $x\zeta=x$.

• •

For all $x\in Dom(\theta_{i})$

• –

If the maximum degree of $S^{x}$ is $i$ then $x\theta_{i}=\Sigma{S_{i}}^{x}$.

• –

If no terms in $S^{x}$ have degree $i$ then $x\theta_{i}=h(x)$.

• –

If $S^{x}$ has terms of degree $i$ and also terms of degree greater than $i$ then $x\theta_{i}=h(x)+\Sigma{S_{i}}^{x}$.

In the rest of this section we will be considering the ACUNh asymmetric equation $u=_{\tiny{\downarrow}}^{?}v$, where $u$ and $v$ are in $R_{1}$ normal form, and we will build an automaton to represent all the solutions of $u=_{\tiny{\downarrow}}^{?}v$. We will need the following definitions.

Definition 10

Let $t$ be an object. Define $loseh(t)=\Sigma\{h^{i}(t)\,\,|\,\,h^{i+1}(t)\in mset(t\downarrow_{R_{h}})\}$.

In the next four automata definitions we will use the following notation: Let $P$ be a set of ACUNh asymmetric equations. Let $m$ be the maximum degree of terms in $P$. Let $\Theta$ be the set of all substitutions $\theta$ such that $Dom(\theta)\subseteq Var(P)$ and for all $x\in Dom(\theta)$, $x\theta=\Sigma T$ where $T$ is a nonempty subset of $Const(P)\cup\{h(x)\}$. Let $u=_{\tiny{\downarrow}}^{?}v$ be an ACUNh asymmetric equation.

First we define an automaton to solve the $ACUNh$ asymmetric unification problem with constants.

Definition 11

The automaton $M(u=_{\tiny{\downarrow}}^{?}v,P)$ consists of the quintuple $(Q,q_{u=_{\tiny{\downarrow}}^{?}v},F,$ $\Theta,$ $\delta)$, where $Q$ is the set of states, $q_{u=_{\tiny{\downarrow}}^{?}v}$ is the start state, $F$ is the set of accepting states, $\Theta$ is the alphabet, and $\delta$ is the transition function, defined as follows:

• •

$Q$ is a set of states of the form $q_{s=_{\tiny{\downarrow}}^{?}t}$, where $s=\Sigma S$ and $t=\Sigma T$, for some $S$ and $T$ subsets of $H_{m}(P)$.

• •

$F=\{q_{s=_{\tiny{\downarrow}}^{?}t}\in Q\,\,|\,\,mset(s)=mset(t)\}$

• •

$\delta:Q\times\Theta\longrightarrow Q$ such that $\delta(q_{s=_{\tiny{\downarrow}}^{?}t},\theta)=q_{loseh(s\theta)\downarrow_{R_{1}}=_{\tiny{\downarrow}}^{?}loseh(t\theta)}$ if $Dom(\theta_{i})=Var$ ($s=_{\tiny{\downarrow}}^{?}t)$, $mset((s\theta)\downarrow_{R_{1}})\cap H_{0}(P)=mset(t\theta)\cap H_{0}(P)$, and $mset(t\theta)$ contains no duplicates.

Next we define an automaton to solve linear constant restrictions.

Definition 12

Let $R$ be a set of linear constant restrictions of the form $(x,c)$. $M_{LCR}(R,$ $P)=(\{q_{0}\},$ $q_{0},\{q_{0}\},\Theta,\delta_{LCR})$ where $\delta_{LCR}(q_{0},\theta)=q_{0}$ if for all variables $x$ and all $(x,c)\in R$, $c\not\in Const(x\theta)$.

Next we define an automaton to solve disequalities between a variable and a constant.

Definition 13

Let $D$ be a set of disequalities of the form $x\not=c$ where $x$ is a variable and $c$ is a constant. $M_{VC}(D,P)=(\{q_{0},q_{1}\},q_{0},$ $\{q_{0},q_{1}\},\Theta,\delta_{VC})$ where $\delta_{VC}(q_{0},\theta)=q_{1}$ if for all variables $x$ and all $x\not=c\in D$, $x\theta\not=c$. Also $\delta_{VC}(q_{1},\theta)=q_{1}$.

Finally we define automata for solving disequalities between variables

Definition 14

Let $x$ and $y$ be variables. Then $M_{VV}(x\not=y,P)=(\{q_{0},q_{1}\},q_{o},\{q_{1}\},\Theta,$ $\delta_{x\not=y})$ where $\delta_{x\not=y}(q_{0},\theta)=q_{0}$ if $mset(x\theta)=T\cup\{h(x)\}$ and $mset(y\theta)=T\cup\{h(y)\}$ for some $T$. Also $\delta_{x\not=y}(q_{0},\theta)=q_{1}$ if $mset(x\theta)\not=mset(y\theta)$ and $mset(x\theta)[x\mapsto y]\not=mset(y\theta)$.

These are all valid automata. In particular, the first automaton described has a finite number of states, and each transition yields a state in the automaton. Now we show that these automata can be used to find all asymmetric ACUNh unifiers.

We need a few properties before we show our main theorem, that the constructed automaton finds all solutions.

Lemma 4.1

Let $t$ be an object and $\theta$ be a substitution, such that, for all $x\in Var(t)$, $mset(x\theta)$ does not contain a variable. Then $mset(t\theta)$ does not contain a variable.

Proof

Consider $s\in mset(t)$. If $s$ is not a variable then $s\theta$ is not a variable. If $s$ is a variable, then, by our hypothesis, $s\theta$ is not a variable.

Lemma 4.2

Let $s=_{\tiny{\downarrow}}^{?}t$ be an ACUNh asymmetric unification equation in $P$, where $mset(s)$ and $mset(t)$ contain no variables and $mset(s\downarrow_{R_{1}})\cap H_{0}(P)\not=mset(t)\cap H_{0}(P)$. Then for all substitutions $\sigma$, $s\sigma$ and $t\sigma$ are not unifiable.

Proof

$s$ and $t$ are not unifiable, because, wlog, the multiplicity of some constant in $mset(s\downarrow_{R_{1}})$ is not in $mset(t\downarrow_{R_{1}})$. When we apply a substitution, that same constant will appear in $mset((s\sigma)\downarrow_{R_{1}})$ but not $mset((t\sigma)\downarrow_{R_{1}})$, since $mset(s)$ and $mset(t)$ contain no variables. So $s\sigma$ and $t\sigma$ are not unifiable.

Lemma 4.3

Let $t$ be such that $mset(t)$ contains a duplicate. Then $\forall~{}\sigma$, $t\sigma$ is reducible by $R_{2}$.

Proof

We know $t$ is reducible by $R_{2}$ because $mset(t)$ contains a duplicate. But then $t\sigma$ also contains a duplicate.

Lemma 4.4

Let $s=_{\tiny{\downarrow}}^{?}t$ be an ACUNh asymmetric unification equation in $P$, such that $mset(s)$ and $mset(t)$ contain no variables. Suppose also that $mset(s\downarrow_{R_{1}})\cap H_{0}(P)=mset(t)\cap H_{0}(P))$ and $mset(t)$ contains no duplicates. Then $\sigma$ is an ACUNh asymmetric unifier of $s=_{\tiny{\downarrow}}^{?}t$ if and only if $\sigma$ is an ACUNh asymmetric unifier of $loseh(s\downarrow_{R_{1}})=_{\tiny{\downarrow}}^{?}loseh(t)$.

Proof

Let $s^{\prime}=loseh(s\downarrow_{R_{1}})$ and $t^{\prime}=loseh(t)$. If $mset(s^{\prime})$ and $mset(t^{\prime})$ contain no constants, then $s=_{\tiny{\downarrow}}^{?}t$ and $s^{\prime}=_{\tiny{\downarrow}}^{?}t^{\prime}$ have the same solutions. Since $mset(s)$ and $mset(t)$ contain no variables, the multiset of constants in $s$ is the same as the multiset of constants in $s\sigma$. Similarly for $t$ and $t\sigma$. Therefore $s=_{\tiny{\downarrow}}^{?}t$ has the same solutions as $s^{\prime}=_{\tiny{\downarrow}}^{?}t^{\prime}$.

Theorem 4.3

Let $P$ be a set of asymmetric ACUNh equations, such that all terms in $P$ are reduced by $R_{1}$. Let $\theta$ be a substitution which is reduced by $R_{1}$. Let $R$ be a set of linear constant restrictions. Let $D$ be a set of variable/constant disequalities. Let $D^{\prime}$ be a set of variable/variable disequalities.

Then $\theta$ is a solution to $P$ if and only if there exists a zero substitution $\zeta$ on $P$ where all right hand sides in $P$ are irreducible, and a sequence of substitutions $\theta_{0},\cdots,\theta_{m}$ such that $\theta\leq\zeta\theta_{0}\cdots\theta_{m}$ and

The string $\theta_{0}\cdots\theta_{m}$ is accepted by $M((u=_{\tiny{\downarrow}}^{?}v)\zeta)\downarrow_{R_{1}},P^{\prime}\zeta)$ for all $u=_{\tiny{\downarrow}}^{?}v\in P$. 2. 2.

The string $\theta_{0}\cdots\theta_{m}$ is accepted by $M_{LCR}(R,P^{\prime}\zeta)$. 3. 3.

The string $\theta_{0}\cdots\theta_{m}$ is accepted by $M_{VC}(D,P^{\prime}\zeta)$. 4. 4.

The string $\theta_{0}\cdots\theta_{m}$ is accepted by $M_{VV}(x\not=y,P^{\prime}\zeta)$ for all $x\not=y\in D^{\prime}$.

where $P^{\prime}=P\cup\{c=_{\tiny{\downarrow}}^{?}c\}$ for a fresh constant $c$.

Proof

First we show that Item 1 holds for a ground substitution $\theta$ reduced by $R_{1}$. By the previous theorem, $\theta$ can be represented as $\zeta\theta_{0}\cdots\theta_{m}$.

We show by induction that, for all $i$, if $\theta=\zeta\theta_{0}\cdots\theta_{i}$ and $\delta(q_{(u=_{\tiny{\downarrow}}^{?}v)\zeta},\theta_{0}\cdots\theta_{i})=q_{s=_{\tiny{\downarrow}}^{?}t}$ then $\theta\sigma$ is an asymmetric ACUNh unifier of $u=_{\tiny{\downarrow}}^{?}v$ if and only if $\sigma$ is an asymmetric ACUNh unifier of $s=_{\tiny{\downarrow}}^{?}t$. In the base case, $\theta=\zeta$ and $(s=_{\tiny{\downarrow}}^{?}t)=(u=_{\tiny{\downarrow}}^{?}v)\zeta$, so it is true.

For the inductive step, we assume the statement is true for $i$ and prove it for $i+1$. Then let $\sigma^{\prime}$ be an arbitrary substitution, and instantiate $\sigma$ $\theta\sigma^{\prime}$ in the inductive assumption, where $\theta=\zeta\theta_{0}\cdots\theta_{i}$. Our assumption implies that $\theta\theta_{i+1}\sigma$ is an asymmetric ACUNh unifier of $u=_{\tiny{\downarrow}}^{?}v$ if and only if $\theta_{i}\sigma$ is an asymmetric ACUNh unifier of $s=_{\tiny{\downarrow}}^{?}t$ (i.e., $\sigma$ is an asymmetric ACUNh unifier of $(s=_{\tiny{\downarrow}}^{?}t)\theta_{i+1}$). If we can now show that $\sigma$ is an asymmetric ACUNh unifier of $(s=_{\tiny{\downarrow}}^{?}t)\theta_{i+1}$ if and only if $\sigma$ is an ACUNh unifier of $loseh(s\theta_{i+1})=_{\tiny{\downarrow}}^{?}loseh(t\theta_{i+1})$. and $mset(s\theta_{i+1}\cap H_{0}(P^{\prime})=mset(t\theta_{i+1})\cap H_{0}(P^{\prime})$ and $mset(t\theta_{i+1})$ contains no duplicates, then we are done. By Lemma 4.1, we know that $mset(s=_{\tiny{\downarrow}}^{?}t)\theta_{i+1}$ contains no variables. Then we apply Lemma 4.4 to prove the induction step.

This proves our inductive statement. If $\theta$ is not an asymmetric ACUNh unifier of $u=_{\tiny{\downarrow}}^{?}v$, then Lemmas 4.2 and 4.3 imply that the transition function will not be applicable at some point. Our inductive statement shows that $\theta$ is an asymmetric ACUNh unifier of $u=_{\tiny{\downarrow}}^{?}v$ if and only if there is a final state with $id$ as an asymmetric ACUNh unifier, which will be an accepting state.

This concludes the case for a ground substitution $\theta$. It $\theta$ is not ground, then the fact that $P^{\prime}$ contains a fresh constant $c$ means that we create substitutions with an additional constant. We have already shown in this paper that nonground solutions are generalizations of solutions involving one additional constant.

It is straightforward to see that the other automata only accept valid solutions of linear constant restrictions and disequations.

If desired, we could intersect all the automata, yielding an automaton representing all the solutions of the problem (think of the results after applying $\zeta$ as a set of initial states). This shows that the set of solutions can be represented by a regular language, with or without $LCRs$ and disequalities. If we only want to decide asymmetric unification, we just check if there is an accepting state reachable from an initial state. We could enumerate all the solutions by finding all accepting states reachable in 1 step, 2 steps, etc. If there is a cycle on a path to an accepting state, then there are an infinite number of solutions, otherwise there are only a finite number of solutions. This will find all the ground substitutions. To find all solutions, we generalize the solutions we find and check them. Indeed, the only terms that need to be generalized are those containing $c$. This is decidable because there are only a finite number of generalizations.

In Figure (5(b)), we show the automaton created for the problem $h(x)+b=_{\tiny{\downarrow}}^{?}x+y$, without linear constant restrictions and disequality constraints. In this example, the only zero substitution that works is the identity. Notice that $c$ never appears in the domain of a substitution, because no such substitution satisfies the conditions for the transition function. This leads to the following theorem.

Theorem 4.4

Asymmetric ACUNh unification with constants is not finitary.

Proof

The automaton constructed for $h(x)+b=_{\tiny{\downarrow}}^{?}x+y$ has a cycle on a path to an accepting state. Therefore there are an infinite number of solutions. Since there is no $c$ in the range of the solution, all the solutions are ground. So no solution can be more general than another one, which means this infinite set of solutions is also a minimal complete set of solutions.

5 Combining Automata based Asymmetric Algorithms with the Free Theory

In order to obtain a general asymmetric ACUNh-unification decision procedure we need to add free function symbols. We can do this by using disjoint combination. The problem of asymmetric unification in the combination of disjoint theories was studied in [7] where an algorithm is developed for the problem. However, the algorithm of [7] does not immediately apply to the two methods developed in this paper. This is due to the nature of the two automata based approaches. More formally, let $\Delta_{1}$ and $\Delta_{2}$ denote two equational theories with disjoint signatures $\Sigma_{1}$ and $\Sigma_{2}$. Let $\Delta$ be the combination, $\Delta=\Delta_{1}\cup\Delta_{2}$, of the two theories having signature $\Sigma_{1}\cup\Sigma_{2}$. The algorithm of [7] solves the asymmetric $\Delta$-unification problem. It assumes that there exists a finitary complete asymmetric $\Delta_{i}$-unification algorithm with linear constant restrictions, $A_{i}$. Based on this assumption the algorithm is able to check solutions produced by the $A_{1}$ and $A_{2}$ algorithms for theory-preserving and injective properties, discarding those that are not. A substitution $\sigma_{i}$ is injective modulo $\Delta_{i}$ if $x\sigma_{i}=_{\Delta_{i}}y\sigma_{i}$ iff $x=y$, and $\sigma_{i}$ is theory preserving if for any variable $x$ of index $i$, $x\sigma_{i}$ is not a variable of index $j\neq i$. For the automaton it is not always possible to check solutions, however, it is possible to build constraints into the automaton that enforce these conditions. Algorithm 3 is a modification of the algorithm from [7] with the following properties:

• •

$\Delta_{1}=ACUNh$ and $\Delta_{2}=F_{\Omega}$, for some free theory $F_{\Omega}$ with symbols $\Omega$.

• •

For each $\Delta_{1}$-pure problem, partition, and theory index, an automaton is constructed enforcing the injective and theory preserving restrictions. Since these restrictions are built into the automata, the only $\Delta_{1}$ solutions produced will be both theory preserving and injective.

• •

The solution produced by the $F_{\Omega}$ algorithm is checked as in the original algorithm. If the solution is found not to be injective or theory preserving it is discarded.

The new modified version is presented in Algorithm 3 (included in the appendix due to space). Given the decision procedure of Section 3 we obtain the following.

Theorem 5.1

Assume there exists an asymmetric $ACUNh$ decision procedure that enforces linear constant restrictions, theory indexes, and injectivity. Then Algorithm 3 is a general asymmetric $ACUNh$ decision procedure.

Proof

The result follows directly from the proof contained in [7]. There it is shown that Algorithm 3 is both sound and complete. The only modification is that in [7] the combination algorithm checks the $\Delta_{1}$ solutions for the properties of being injective and theory preserving, while in Algorithm 3 it is assumed that the algorithm $A_{1}$ itself will enforce these restrictions.

If instead of a decision procedure we want to obtain a general asymmetric $ACUNh$ unification algorithm we can use the automata based algorithm from Section 4 and again a modification of the asymmetric combination algorithm of [7]. Here, the modification to the combination algorithm is even smaller. We just remove the check on injective and theory preserving substitutions. Again these restrictions are enforced by the automata. The solutions to the $ACUNh$ and the free theory are combined as is done in [7] since they obey the same linear constant restrictions. Since asymmetric $ACUNh$ unification with constants is not finitary (Theorem 4.4), the general asymmetric $ACUNh$ unification algorithm will not in general produce a finite set of solutions. However, based on the algorithm of Section 4 we easily obtain the following result.

Theorem 5.2

Assume there exists an asymmetric $ACUNh$ algorithm that enforces linear constant restrictions, theory indexes and injectivity, and produces a complete set of unifiers. Then there exists a general asymmetric $ACUNh$ algorithm producing a complete set of unifiers.

6 Conclusion

We have provided a decision procedure and an algorithm for asymmetric unification modulo $ACUNh$ using a decomposition $R\uplus ACh$. This is the first example of an asymmetric unification algorithm for a theory in which unification modulo the set $\Delta$ of axioms is undecidable. It also has some practical advantages: it is possible to tell by inspection of the automaton used to construct unifiers whether or not a problem has a finitary solution. Moreover, the construction of the automaton gives us a natural way of enumerating solutions; simply traverse one of the loops one more time to get the next unifier.

There are a number of ways in which we could extend this work. For example, the logical next step is to consider the decidability of asymmetric unification of $AGh$ with a $\Delta=ACh$. If the methods we used for $ACUNh$ extend to $AGh$, then we have an asymmetric unification algorithm for $AGh$, although with $\Delta=ACh$ instead of $AC$. On the other hand, if we can prove undecidability of asymmetric unification for $AGh$ with $\Delta=ACh$ as well as with $\Delta=AC$, this could give us new understanding of the problem that might allow us to obtain more general results. Either way, we expect the results to give increased understanding of asymmetric unification when homomorphic encryption is involved.

Appendix 0.A Proof of $R_{2},ACh$ convergence

0.A.1 $R_{2}$ is $ACh$-convergent

To begin with let us show that the theory, $\rightarrow_{R_{2}/ACh}$, is terminating.

Lemma 0.A.1

$\rightarrow_{R_{2}/ACh}$* is terminating.*

Proof

We use a polynomial interpretation. The signature of $R_{2}$ is $\Sigma\;=\;\{+,h,0\}$. We take the polynomial interpretation $P_{h}\;=\;2*X,\;P_{0}\;=\;1,\;P_{+}\;=\;X+Y$. It is not hard to see that the rewrite rules are decreasing and the identities are preserved under this interpretation. Hence $\rightarrow_{R_{2},ACh}$ is terminating.

The identities in $ACh$ can be further decomposed, retaining associativity and commutativity as identities ${\Delta}$ and viewing the other identity as a rewrite rule $R_{h}$.

Thus $R_{h}$ is the term rewriting system: $h(x+y)\rightarrow h(x)+h(y)$ with the identities $AC$: $(x+y)+z\approx x+(y+z),\;\;\;x+y\approx y+x$ Note that $R_{1}~{}=~{}R_{2}\cup R_{h}$. Thus $\longrightarrow_{R_{1},AC}\;=\;\longrightarrow_{R_{2},AC}\;\cup\;\longrightarrow_{R_{h},AC}$. All these term rewriting systems, $R_{1}$, $R_{2}$ and $R_{h}$, are $AC$-convergent.

We define some terms which will be used later:

Definition 15

A term is a $\bf{+}$-term if and only if it has only variables and constants, and no occurrences of $h$.

Definition 16

A term is a pure $\bf{+}$-term if and only if it is a $\bf{+}$-term with no constants (i.e., it belongs to $T(\{+\},V)$).

In order to prove that $R_{2}$ is $ACh$-convergent we first prove the following lemmas:

Lemma 0.A.2

If $s$ and $t$ are irreducible by $\rightarrow_{R_{h},AC}$, then so is $s+t$.

Proof

The only rule in $R_{h}$ has $h$ as the root of its left-hand side. Hence for the term $s+t$ there is no reduction possible.

Corollary 0.A.2.1

(s+t)\!\big{\downarrow}_{R_{h},AC}~{}=~{}s\!\big{\downarrow}_{R_{h},AC}\;+\;t\!\big{\downarrow}_{R_{h},AC}**

Lemma 0.A.3

If s is a $\bf{+}$-term, then $s\;\lesssim_{ACh}\;t$ if and only if s\;\lesssim_{AC}\;t\!\big{\downarrow}_{R_{h},AC}.

Proof

Since $s$ is a $\bf{+}$-term, $s$ is of the form $Y_{1}+\ldots+Y_{n}+c_{1}+\ldots+c_{m}$, where the $Y_{i}$’s need not be distinct. Let $t^{\prime}$ be the normal form of $t$ modulo $R_{h}$, i.e., t^{\prime}=t\!\big{\downarrow}_{R_{h},AC}.

“if” part: If $s$ $AC$ matches with $t^{\prime}$, then $s$ is $ACh$ matchable with $t$.

Let $\theta$ be a matching substitution such that $s\theta\;{\approx}_{AC}\;t^{\prime}$. The substitution $\theta$ also $ACh$ matches $s$ with $t$, i.e., $s\theta\;\approx_{ACh}\;t$, because $AC$ is a subset of $ACh$.

“only if” part: If $s$ $ACh$ matches with $t$, then $s\;AC$ matches with $t^{\prime}$.

Suppose $s\sigma\;{\approx}_{ACh}\;t$, where $\sigma$ is substitution. Let $\sigma^{\prime}$ be a substitution defined as z\sigma^{\prime}~{}=~{}z\sigma\!\big{\downarrow}_{R_{h},AC} for all $z\in Dom(\sigma)$. We now show that $s\sigma^{\prime}\;\approx_{AC}\;t^{\prime}$.

We have $s\sigma\;{\approx}_{ACh}\;t$ and by Corollary 0.A.2.1, s\sigma^{\prime}\;=\;s\sigma\!\big{\downarrow}_{R_{h},AC}, i.e., $s\sigma\rightarrow_{R_{h},AC}^{!}s\sigma^{\prime}$. Thus $s\sigma^{\prime}\;\approx_{AC}\;t^{\prime}$.

Corollary 0.A.3.1

A term $s$ is reducible at the root (i.e., at position $\epsilon$) by $\;\longrightarrow_{R_{2},ACh}\;$ if and only if s\!\big{\downarrow}_{R_{h},AC} is reducible at the root by $\;\longrightarrow_{R_{2},AC}$.

Lemma 0.A.4

If $s$ is a pure $\bf{+}$-term, then $s\;\lesssim_{ACh}\;h(t)$ if and only if $s\;\lesssim_{ACh}\;t$.

Proof

For the “if” part, let $\theta$ be the matching substitution. Then the substitution $\theta^{\prime}$, defined as $y\theta^{\prime}=h(y\theta)$ $\text{ for all }y$ matches $s$ with $h(t)$.

For the “only if” part, suppose $\beta$ is a substitution that $ACh$-matches $s$ with $h(t)$. We can assume without loss of generality that $t$ is a ground term. Since $R_{h}$ is $AC$-convergent, we can also assume that the normal form of $h(t)$, modulo $\rightarrow_{R_{h},\,AC}$, is of the form $h^{i_{1}}(a_{1})+\ldots~{}+h^{i_{n}}(a_{n})$ where the $a_{i}$’s are constants and each exponent $i_{j}$ is a positive integer greater than zero. Therefore for each variable $X_{k}$, $X_{k}\beta~{}\approx_{ACh}~{}h(t_{k})$ for some ground term $t_{k}$. Thus $\beta^{\prime}$, defined as $y\beta^{\prime}=s^{\prime}~{}~{}\text{ if }~{}~{}y\beta~{}\approx_{ACh}~{}h(s^{\prime})$ will match $s$ with $t$.

Lemma 0.A.5

If $s$ is a $\bf{+}$-term and $s\;\lesssim_{ACh}\;h(t)$ then $s\;\lesssim_{ACh}\;t$.

Proof

Since $s$ is a $\bf{+}$-term, $s$ must be of the form $X_{1}+\ldots+X_{m}+b_{1}+\ldots+b_{n}$ where some of the $X_{i}$’s can be equal (i.e., variables can be repeated). However, clearly $s$ cannot have constants and thus must be a pure $\bf{+}$-term. The rest of the proof follows from the “only if” part of the previous lemma.

Lemma 0.A.6

For all $t,\,s,\,t^{\prime\prime}$: if $t$ is reducible at the root (i.e., at position $\epsilon$) by $\;\longrightarrow_{R_{2},ACh}\;$ and $t^{\prime\prime}\;\approx_{AC}\;t\;+\;s$ then $t^{\prime\prime}$ is also reducible by $\;\longrightarrow_{R_{2},ACh}$.

Proof

Suppose $t\;\approx_{ACh}\;l\sigma$ where $\sigma$ is a substitution and $l\rightarrow r\in R_{2}$. The case where $l=h(0)$ is trivial.

Suppose $l$ is the left-hand side of one of the other rules. Then $l$ is a $+$-term. Let t_{1}=t\!\big{\downarrow}_{R_{h},AC}. By the proof of Lemma 0.A.3, $t_{1}\;\approx_{AC}\;l\sigma^{\prime}$, where $\sigma^{\prime}$ is defined as y\sigma^{\prime}=y\sigma\!\big{\downarrow}_{R_{h},AC} for all $y\in Dom(\sigma)$. From this we have l\sigma^{\prime}\;=\;l\sigma\!\big{\downarrow}_{R_{h},AC}, i.e., $l\sigma\rightarrow_{R_{h},AC}^{!}l\sigma^{\prime}$.

Let $t^{\prime\prime}\;\approx_{AC}\;t\;+\;s$. By Corollary 0.A.2.1, $t\;+\;s\;\longrightarrow^{!}_{R_{h},AC}\;t_{1}+\widehat{s}\,$ where \widehat{s}\,=\,s\!\big{\downarrow}_{R_{h},AC}. Since $t_{1}$ is reducible at the root by $\longrightarrow_{R_{2},AC}$, so is $t_{1}+\widehat{s}$, as can be seen from an examination of the rules. Thus $t^{\prime\prime}\;\longrightarrow^{!}_{R_{h},AC}\;t_{1}+\widehat{s}\;~{}\;\approx_{AC}\;~{}l^{\prime}\beta$ for some rule $(l^{\prime}\rightarrow r^{\prime})$ in $R_{2}$. This implies that $\,t^{\prime\prime}\;~{}\;\approx_{ACh}\;~{}l^{\prime}\beta$.

Lemma 0.A.7

For all $t$, if $h(t)$ is reducible by $\;\longrightarrow_{R_{2},ACh}\;$ then $t=0$ or $t$ is reducible by $\;\longrightarrow_{R_{2},ACh}$.

Proof

Suppose $t\neq 0$ and that $t$ is not reducible by $\;\longrightarrow_{R_{2},ACh}$. Then there must be some left-hand side $l$ in $R_{2}$ such that $l\;\lesssim_{ACh}\;h(t)$. Since $t\neq 0$, $l$ cannot be $h(0)$, so $l$ must be a $\bf{+}$-term. If $l\;\lesssim_{ACh}\;h(t)$, by Lemma 0.A.5 we know that $l\;\lesssim_{ACh}\;t$, which is a contradiction.

Lemma 0.A.8

For all $s,s^{\prime}$, if $s$ is reducible by $\;\longrightarrow_{R_{2},ACh}\;$ and $s\,\approx_{AC}\,s^{\prime}$, then $s^{\prime}$ is reducible by $\;\longrightarrow_{R_{2},ACh}$.

Proof

Assume the contrary. Let $t$ be the smallest term such that $t$ is reducible by $\;\longrightarrow_{R_{2},ACh}\;$ and there is another term $t^{\prime}$, AC-equivalent to $t$, such that $t^{\prime}$ is irreducible by $\;\longrightarrow_{R_{2},ACh}$. Clearly $t$ cannot be reducible at the root. Let $p\neq\epsilon$ be an outermost position in $t$ such that $t|_{p}$ is a redex. Let $p=p^{\prime}\cdot i$. Obviously, $t|_{p}$ cannot be $h(0)$. The parent of node $p$ cannot have a $+$-symbol because then that subterm, i.e., $t|_{p^{\prime}}$, will be a redex too, by the proof of Lemma 0.A.6. Thus it has to be an $h$: in other words, $h(t|_{p})$ is a subterm of $t$. Since $t^{\prime}\,\approx_{AC}\,t$, $t^{\prime}$ should have a subterm $h(t_{1}^{\prime})$ where $t_{1}^{\prime}\,\approx_{AC}\,t|_{p}$. If $t_{1}^{\prime}$ is reducible then so is $t^{\prime}$; if not, then $t^{\prime}$ is a smaller counterexample.

Corollary 0.A.8.1

For all $t,\,t^{\prime},\,t^{\prime\prime}$: if $t$ is reducible by $\;\longrightarrow_{R_{2},ACh}\;$ and $t^{\prime\prime}\;\approx_{AC}\;t\;+\;t^{\prime}$ then $t^{\prime\prime}$ is also reducible by $\;\longrightarrow_{R_{2},ACh}$.

Lemma 0.A.9

For all $s_{1},\,s_{2},\,s_{3}$: if $s_{1}$ $\;\longrightarrow_{R_{h},AC}\;$ $s_{2}$, and $s_{2}$ $\;\longrightarrow_{R_{2},ACh}\;$ $s_{3}$, then $s_{1}$ is also reducible by $\longrightarrow_{R_{2},ACh}$.

Proof

Suppose $s_{1}$ reduces to $s_{2}$ at some position $p$ and $s_{2}$ reduces to $s_{3}$ at some position $q$, i.e., $s_{1}\;\longrightarrow_{R_{h},AC}^{p}\;s_{2}$ and $s_{2}\;\longrightarrow_{R_{2},ACh}^{q}\;s_{3}$. Thus there is a substitution $\theta$ such that ${s_{1}}|_{p}\;\approx_{AC}\;(h(x+y))\theta$ and $s_{2}\;=\;s_{1}[h(x\theta)+h(y\theta)]_{p}$.

Two cases have to be considered:

$p<q:$ Either $h(x\theta)$ or $h(y\theta)$ is reducible by $\longrightarrow_{R_{2},ACh}$. Assume, without loss of generality, that $h(x\theta)$ is reducible by $\longrightarrow_{R_{2},ACh}$. By Lemma 0.A.7, $x\theta$ is either 0 or reducible by $\longrightarrow_{R_{2},ACh}$. If $x\theta$ is reducible by $\longrightarrow_{R_{2},ACh}$, then $x\theta+y\theta$ is also reducible by $\longrightarrow_{R_{2},ACh}$, by Corollary 0.A.8.1. If $x\theta=0$, then clearly $x\theta+y\theta\;=\;0+y\theta$ is reducible by $\longrightarrow_{R_{2},ACh}$.

$q\lesssim p:$ Let $p=q\cdot\pi$. Let $s_{4}~{}=~{}s_{1}|_{q}$ and $s_{5}~{}=~{}s_{4}\left[\vphantom{b_{a}^{c}}h(x\theta)+h(y\theta)\right]_{\pi}$. Thus $s_{4}\;\longrightarrow_{R_{h},AC}^{\pi}\;s_{5}$ and $s_{5}$ is reducible at the root by $\longrightarrow_{R_{2},ACh}$. By Corollary 0.A.3.1, s_{5}\!\big{\downarrow}_{R_{h},AC} is reducible at the root by $\longrightarrow_{R_{2},AC}$, i.e., s_{5}\!\big{\downarrow}_{R_{h},AC}\;\approx_{AC}\;l\beta for some left-hand side $l$. Thus (putting it all together), s_{1}|_{q}\;\longrightarrow_{R_{h},AC}^{!}\;s_{5}\!\big{\downarrow}_{R_{h},AC}\;\approx_{AC}\;l\beta. Thus, again by Corollary 0.A.3.1, $s_{1}|_{q}$ is reducible by $\longrightarrow_{R_{2},ACh}$.

Finally, we can prove the convergence.

Lemma 0.A.10

$\longrightarrow_{R_{2},ACh}\,$* is $ACh$-convergent.*

Proof

We prove by contradiction. Suppose $\longrightarrow_{R_{2},ACh}\,$ is not $ACh$-convergent. Since $\longrightarrow_{R_{2},ACh}\,$ is terminating, there must be terms $s$ and $t$ such that $s$ and $t$ are in normal form modulo $\longrightarrow_{R_{2},ACh}\,$ and $s\;\not\approx_{ACh}\;t$. Since $\longrightarrow_{R_{h},AC}\,$ is AC-convergent, the normal forms of $s$ and $t$ modulo $\longrightarrow_{R_{h},AC}\,$ cannot be $AC$-equal. Let $\widehat{s}$ and $\widehat{t}$ be respectively the normal forms of $s$ and $t$ modulo $\longrightarrow_{R_{h},AC}$. If either $\widehat{s}$ or $\widehat{t}$ is reducible by $\longrightarrow_{R_{2},ACh}\,$, then, by Lemma 0.A.9, either $s$ or $t$ will be reducible by $\longrightarrow_{R_{2},ACh}$. But since $\longrightarrow_{R_{1},AC}\,$ is AC-convergent, either $\widehat{s}$ or $\widehat{t}$ must be reducible by $\longrightarrow_{R_{1},AC}$. This also leads to a contradiction, since $\longrightarrow_{R_{1},AC}\;=\;\longrightarrow_{R_{2},AC}\;\cup\;\longrightarrow_{R_{h},AC}$.

Appendix 0.B Asymmetric Combination Algorithm