colorlinks, citecolor=black, filecolor=black, linkcolor=black, urlcolor=black

22 2110

# Nominal Unification and Matching of
Higher Order Expressions with Recursive Let

Manfred Schmidt-Schauß
GU Frankfurt Address for correspondence: Goethe-Universität Frankfurt am Main
Fachbereich 12: Informatik und Mathematik, Robert-Mayer-Straße 11-15, 60325
Frankfurt am Main, Grrmany.

Received February 2021; accepted April 2022.
https://orcid.org/0000-0001-8809-7385 Germany
<EMAIL_ADDRESS>Temur Kutsia
RISC  https://orcid.org/0000-0003-4084-7380 JKU Linz  Austria
<EMAIL_ADDRESS>Jordi Levy
IIIA - CSIC  https://orcid.org/0000-0001-5883-5746 Spain
<EMAIL_ADDRESS>Mateu Villaret
IMA  https://orcid.org/0000-0002-8066-3458 Universitat de Girona  Spain
<EMAIL_ADDRESS>Yunus Kutz
GU Frankfurt  https://orcid.org/0000-0002-5060-502X Germany
<EMAIL_ADDRESS>
###### Abstract

A sound and complete algorithm for nominal unification of higher-order
expressions with a recursive let is described, and shown to run in
nondeterministic polynomial time. We also explore specializations like nominal
letrec-matching for expressions, for DAGs, and for garbage-free expressions
and determine their complexity. We also provide a nominal unification
algorithm for higher-order expressions with recursive let and atom-variables,
where we show that it also runs in nondeterministic polynomial time. In
addition we prove that there is a guessing strategy for nominal unification
with letrec and atom-variable that is a trade-off between exponential growth
and non-determinism. Nominal matching with variables representing partial
letrec-environments is also shown to be in NP.

###### keywords:

Nominal unification, lambda calculus, higher-order expressions, recursive let,
atom variables

††volume: 185††issue: 3

Nominal Unification with Recursive Let

_This paper is an extended version of the conference publication[1]._

##  1 Introduction

Unification [2] is an operation to make two logical expressions equal by
finding substitutions into variables. There are numerous applications in
computer science, in particular of (efficient) first-order unification, for
example in automated reasoning, type checking and verification. Unification
algorithms are also extended to higher-order calculi with various equivalence
relations. If equality includes $\alpha$-conversion and $\beta$-reduction and
perhaps also $\eta$-conversion of a (typed or untyped) lambda-calculus, then
unification procedures are known (see, e.g., [3]), however, the problem is
undecidable [4, 5].

Our motivation comes from syntactical reasoning on higher-order expressions,
with equality being $\alpha$-equivalence of expressions, and where a
unification algorithm is demanded as a basic service. Nominal unification is
the extension of first-order unification with abstractions. It unifies
expressions w.r.t. $\alpha$-equivalence, and employs permutations as a
mathematically clean treatment of renamings. It is known that nominal
unification is decidable [6, 7], where the complexity of the decision problem
is polynomial time [8]. It can be seen also from a higher-order perspective
[9], as equivalent to Miller’s higher-order pattern unification [10]. There
are efficient algorithms [8, 11], formalizations of nominal unification [12],
formalizations with extensions to commutation properties within expressions
[13], and generalizations of nominal unification to narrowing [14].
Equivariant (nominal) unification [15, 16, 17] extends nominal unification by
permutation-variables, but it can also be seen as a generalization of nominal
unification by permitting abstract names for variables.

We are interested in unification w.r.t. an additional extension with cyclic
let. To the best of our knowledge, there is no nominal unification algorithm
for higher-order expressions permitting general binding structures like a
cyclic let. Higher-order unification could be applied, however, the algorithms
are rather general and thus the obtained complexities of specializations are
too high. Thus we propose to extend and adapt usual nominal unification [6, 7]
to languages with recursive let.

The motivation and intended application scenario is as follows: constructing
syntactic reasoning algorithms for showing properties of program
transformations on higher-order expressions in call-by-need functional
languages (see for example [18, 19]) that have a letrec-construct (also called
cyclic let) [20] as in Haskell [21], (see e.g. [22] for a discussion on
reasoning with more general name binders, and [23] for a formalization of
general binders in Isabelle). Extended nominal matching algorithms are
necessary for applying program transformations that could be represented as
rewrite rules. Basic properties of program transformations like commuting
properties of conflicting applications or overlaps can be analyzed in an
automated way if there is a nominal unification algorithm of appropriate
complexity. There may be applications also to co-inductive extensions of logic
programming [24] and strict functional languages [25]. Basically, overlaps of
expressions have to be computed (a variant of critical pairs) and reduction
steps (under some strategy) have to be performed. To this end, first an
expressive higher-order language is required to represent the meta-notation of
expressions. For example, the meta-notation $((\lambda x.e_{1})~{}e_{2})$ for
a beta-redex is made operational by using unification variables $X_{1},X_{2}$
for $e_{1},e_{2}$. The scoping of $X_{1}$ and $X_{2}$ is different, which can
be dealt with by nominal techniques. In fact, a more powerful unification
algorithm is required for meta-terms employing recursive letrec-environments.

Our main algorithm LetrecUnify is derived from first-order unification and
nominal unification: From first-order unification we borrow the decomposition
rules, and the sharing method from Martelli-Montanari-style unification
algorithms [26]. The adaptations of decomposition for abstractions and the
advantageous use of permutations of atoms is derived from nominal unification
algorithms. Decomposing letrec-expression requires an extension by a
permutation of the bindings in the environment, where, however, one has to
take care of scoping. Since in contrast to basic nominal unification, there
are nontrivial fixpoints of permutations (see Example 3.2), novel techniques
are required and lead to a surprisingly moderate complexity: a fixed-point
shifting rule (FPS) and a redundancy removing rule (ElimFP) are required.
These rules bound the number of fixpoint equations $X\doteq\pi{\cdot}X$ (where
$\pi$ is a permutation) using techniques and results from computations in
permutation groups. The application of these techniques is indispensable (see
Example 4.6) for obtaining efficiency.

Inspired by the applications in programming languages, we investigate the
notion of garbage-free expressions. The restriction to garbage-free
expressions permits several optimizations of the unification algorithms. The
first is that testing $\alpha$-equivalence is polynomial. Another advantage is
that due to the unique correspondence of positions for two $\alpha$-equal
garbage-free expressions, we show that in this case, fixpoint equations can be
replaced by freshness constraints (Corollary 8.5).

As a further extension, we study the possibility to formulate input problems
using atom variables as in [27, 28] in order to take advantage of the
potential of less nondeterminism. The corresponding algorithm LetrecUnifyAV
requires permutation expressions and generalizes freshness constraints as
further expressibility, and also other techniques such as explicit compression
of permutations. The algorithm runs in NP time. We added a strategy to really
exploit the extended expressivity and the omission of certain nondeterministic
choices.

_Related Work:_ Besides the already mentioned related work, we highlight
further work. In nominal commutative unification [29], one can observe that
there are nontrivial fixpoints of permutations. This is similar to what we
have in nominal unification with recursive let (when garbage-freeness is not
required), which is not surprising, because, essentially, this phenomenon is
related to the lack of the ordering: in one case among the arguments of a
commutative function symbol, in the other case among the bindings of recursive
let. Consequently, nominal C-unification reduces to fixpoint constraints.
Those constraints may have infinitely many incomparable solutions expressed in
terms of substitutions and freshness constraints (which is the standard way to
represent nominal unifiers). In [30], the authors proposed to use fixpoint
constraints as a primitive notion (instead of freshness constraints) to
axiomatize $\alpha$-equivalence and, hence, use them in the representation of
unifiers, which helped to finitely represent solutions of nominal
C-unification problems. The technical report [31] contains explanations how to
obtain a nominal C-unification algorithm from a letrec unification algorithm
and transfers the NP-completeness result for letrec unification to nominal
commutative unification.

An investigation into nominal rewriting and nominal matching is in [32], where
a nominal matching algorithm is implicitly derived from nominal unification.

The $\rho_{g}$-calculus [33] integrates term rewriting and lambda calculus,
where cyclic, shared terms are permitted. Such term-graphs are represented as
recursion constraints, which resemble to recursive let environments. The
evaluation mechanism of the $\rho_{g}$-calculus is based on matching for such
shared structures. Matching and recursion equations are incorporated in the
object level and rules for their evaluation are presented.

Unification of higher-order expressions with recursive let (but without
nominal features) has been studied in the context of proving correctness of
program transformations in call-by-need $\lambda$-calculi [34, 35]. Later, in
[36], the authors proposed a more elaborated approach to address semantic
properties of program calculi, which involves unification of meta-expressions
of higher-order lambda calculi with letrec environments. This unification
problem extends those from [34, 35]: environments are treated as multisets,
different kinds of variables are considered (for letrec environments,
contexts, and binding chains), more than one environment variable is
permitted, and non-linear unification problems are allowed. Equivalence there
is syntactic, in contrast to our nominal approach where equality modulo
$\alpha$ is considered. Unlike [36], our unification problems do not involve
context and chain variables, but we do have environment variables in matching
problems. We investigate an extension of nominal letrec unification with atom
variables.

There are investigations into variants of nominal techniques with a modified
view of variables and their renamings and algorithms for the respective
variants of nominal unification [37], however, it is unclear whether this can
be extended to letrec.

Results: The nominal letrec unification algorithm is complete and runs in
nondeterministic polynomial time (Theorem 5.3, 5.7). The nominal letrec
matching is NP-complete (Theorems 6.4, 5.1), as well as the nominal letrec
unification problem (Theorems 5.7, 5.1). Nominal letrec matching for DAGs is
in NP and outputs substitutions only (subsection 6.1), and a very restricted
nominal letrec matching problem is already graph-isomorphism hard (Theorem
7.2). Nominal unification for garbage-free expressions can be done with simple
fixpoint rules (Corollary 8.5). In the extension with atom variables, nominal
unification can be done using further useful strategies with less
nondeterminism and is NP-complete (Theorem 9.19). We construct an algorithm
for nominal matching including letrec-environment variables, which runs in NP
time (Theorem 10.4).

Structure of the paper. It starts with a motivating intuition on nominal
unification (Sec. 2). After explaining the ground letrec-language LLR in Sec.
3, the unification algorithm LetrecUnify for LLR-expression is described in
Sec. 4. Sec. 5 contains the arguments for soundness and completeness of
LetrecUnify. Sec. 6 describes an improved algorithm for nominal matching on
LLR: LetrecMatch. Further sections are on extensions. Sec. 7 shows Graph-
Isomorphism-hardness of nominal letrec matching and unification on garbage-
free expressions (Theorem 7.2). Sec. 8 shows that fixpoint-equations for
garbage-free expressions can be translated into freshness constraints (Cor.
8.5). Sec. 9 considers nominal unification in an extension with atom
variables, an nominal unification algorithm LetrecUnifyAV is defined and the
differences to LetrecUnify are highlighted. It is shown that there is a simple
strategy such that nominal unification runs in NP time (Theorem 9.19). The
last section (Sec. 10) presents a nominal matching algorithm LetrecEnvMatch
that is derived from the corresponding nominal unification algorithm
LetrecUnifyAV. Sec. 11 concludes the paper.

##  2 Some intuitions

In first order unification we have a language of applications of function
symbols over a (possible empty) list of arguments $(fe_{1}\dots e_{n})$, where
$n$ is the arity of $f$, and variables $X$. Solutions of equations between
terms are substitutions for variables that make both sides of equations
syntactically equal. First order unification problems may be solved using the
following two problem transformation rules:

(Decomposition) ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{(f\,e_{1}\dots e_{n})\doteq(f\,e^{\prime}_{1}\dots
e^{\prime}_{n})\\}}{\Gamma\cup\\{e_{1}\doteq e^{\prime}_{1}\dots e_{n}\doteq
e^{\prime}_{n}\\}}}$

(Instantiation) ${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{X\doteq
e\\}}{[X\mapsto e]\Gamma}}$ If $X$ does not occur in $e$.

The substitution solving the original set of equation may be easily recovered
from the sequence of transformations. However, the algorithm resulting from
these rules is exponential in the worst case.

Martelli and Montanari [26] described a set of improved rules that result into
an $O(n\,\log n)$ time algorithm111The original Martelli and Montanari’s
algorithm is a bit different. In fact, they do not flatten equations. However,
the essence of the algorithm is basically the same as the one described here.
where $n$ is the size of the input equations. In a first phase the problem is
flattened,222In the flattening process we replace every proper subterm
$(fe_{1}\dots e_{n})$ by a fresh variable $X$, and add the equation
$X\doteq(fe_{1}\dots e_{n})$. We repeat this operation (at most a linear
number of times) until all proper subterms are variable occurrences. resulting
into equations where every term is a variable or of the form $(f~{}X_{1}\ldots
X_{n})$. The second phase is a transformation using the following rules:
$\begin{array}[]{@{}ll@{}}\begin{minipage}{113.81102pt}(Decomposition)
\end{minipage}&{{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{(f\,X_{1}\dots X_{n})\doteq(f\,Y_{1}\dots
Y_{n})\\}}{\Gamma\cup\\{X_{1}\doteq Y_{1},\dots,X_{n}\doteq
Y_{n}\\}}\vspace{3mm}}}\\\ \begin{minipage}{113.81102pt} (Variable~{}
Instantiation) \end{minipage}&{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{X\doteq Y\\}}{[X\mapsto Y]\Gamma}}\end{array}$
(Elimination) ${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{X\doteq
e\\}}{\Gamma}}$ If $X$ neither occurs in $e$ nor in $\Gamma$

(Merge) ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{X\doteq(f\,X_{1}\dots X_{n}),X\doteq(f\,Y_{1}\dots
Y_{n})\\}}{\Gamma\cup\\{X\doteq(f\,X_{1}\dots X_{n}),X_{1}\doteq
Y_{1},\dots,X_{n}\doteq Y_{n}\\}}}$

Notice that in these rules the terms involved in the equations are not
modified (they are not instantiated), except by the replacement of a variable
by another in the Variable Instantiation rule. We can define a measure on
problems as the number of distinct variables, plus the number of equations,
plus the sum of the arities of the function symbol occurrences. All rules
decrease this measure (for instance, the merge rule increases the number of
equations by $n-1$, but removes a function symbol occurrence of arity $n$).
Since this measure is linear in the size of the problem, this proves that the
maximal number of rule applications is linear. The Merge rule is usually
described as

${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{X\doteq e_{1},X\doteq
e_{2}\\}}{\Gamma\cup\\{X\doteq e_{1},e_{1}\doteq e_{2}\\}}}$ If $e_{1}$ and
$e_{2}$ are not variables

However, this rule does not decrease the proposed measure. We can force the
algorithm to, if possible, immediately apply a decomposition of the equation
$e_{1}\doteq e_{2}$. Then, the application of both rules (resulting into the
first proposed Merge rule) does decrease the measure.

###  2.1 Nominal unification

Nominal unification is an extension of first-order unification in the presence
of lambda-binders. Variables of the target language are called atoms, and the
unification-variables are simply called variables. Bound atoms can be renamed.
For instance, $\lambda a.(f\,a)$ is equivalent to $\lambda b.(f\,b)$. We also
have permutations of atom names (represented as swappings) applied to
expressions of the language. When these permutations are applied to a
variable, this is called a _suspension_. The action of a permutation on a term
is simplified until we get a term where permutations are innermost and only
apply to variables. For instance, $(a\,b){\cdot}\lambda
a.(f\,X\,a\,(f\,b\,c))$, where $(a\,b)$ is a swapping between the atoms $a$
and $b$, results into $\lambda b.(f\,(a\,b){\cdot}X\,b\,(f\,a\,c))$. As we
will see below, we also need a predicate to denote that an atom $a$ cannot
occur free in a term $e$, noted $a\\#e$.

We can extend the previous first-order unification algorithm to the nominal
language modulo $\alpha$-equivalence. The decomposition of
$\lambda$-expressions distinguishes two cases, when the binder name is the
same and when they are distinct and we have to rename one of them:

<EMAIL_ADDRESS>\centering(Decomposition \\\ lambda 1)
\@add@centering\end{minipage}&{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\lambda a.s\doteq\lambda a.t\\}}{\Gamma\cup\\{s\doteq
t\\}}}&\begin{minipage}{71.13188pt} \centering(Decomposition \\\ lambda 2)
\@add@centering\end{minipage}&{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\lambda a.s\doteq\lambda
b.t\\}}{\Gamma\cup\\{s\doteq(a~{}b){\cdot}t,a{{\\#}}t\\}}}\end{array}$

As we see in the second rule, we introduce a _freshness constraint_ that has
to be checked or solved, so we need a set of transformations for this kind of
equations. This set of freshness constraints is solved in a second phase of
the algorithm.

As we have said, permutations applied to variables cannot be longer simplified
and result into suspensions. Therefore, now, we deal with suspensions instead
of variables, and we do not make any distinction between $X$ and
$\mathit{Id}{\cdot}X$. Variable instantiation distinguishes two cases:
$\begin{array}[]{<EMAIL_ADDRESS>(Variable \\\
Instantiation) \end{minipage}&{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi\cdot X\doteq\pi^{\prime}\cdot
Y\\}~{}~{}~{}X\not=Y}{[X\mapsto(\pi^{-1}\circ\pi^{\prime})\cdot
Y]\Gamma}}&\begin{minipage}{42.67912pt} (Fixpoint)
\end{minipage}&{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{\pi\cdot
X\doteq\pi^{\prime}\cdot X\\}}{\Gamma\cup\\{a\\#X\mid
a\in\mathit{dom}(\pi^{-1}\circ\pi^{\prime})\\}}}\end{array}$
Notice that equations between the same variable $X\doteq X$ that are trivially
solvable in first-order unification, adopt now the form $\pi\cdot
X\doteq\pi^{\prime}\cdot X$. This kind of equations are called _fixpoint
equations_ and impose a restriction on the possible instantiations of $X$,
when $\pi$ and $\pi^{\prime}$ are not the identity. Namely, $\pi\cdot
X\doteq\pi^{\prime}\cdot X$ is equivalent to $\\{a\\#X\mid
a\in\mathit{dom}(\pi^{-1}\circ\pi^{\prime})\\}$, where the domain
$\mathit{dom}(\pi)$ is the set of atoms $a$ such that $\pi(a)\neq a$.

From this set of rules we can derive an $O(n^{2}\,\log n)$ algorithm, similar
to the algorithms described in [8, 11]. This algorithm has three phases.
First, it flattens all equations. Second, it applies this set of problem
transformation rules. Using the same measure as in the first-order case
(considering lambda abstraction as a unary function symbol and not counting
the number of freshness equations), we can prove that the length of problem
transformation sequences is always linear. In a third phase, we deal with
freshness equations. Notice that the number of distinct non-simplifiable
freshness equations $a\\#X$ is quadratically bounded.

###  2.2 Letrec expressions

Letrec expressions have the form $({\tt
letrec}~{}a_{1}.e_{1};\ldots;a_{n}.e_{n}~{}{\tt in}~{}e)$. Variables $a_{i}$
are binders where the scope is in all expressions $e_{j}$ and in $e$. (Here we
will use $\alpha$-equivalence in an informal fashion; it is defined in Def.
3.1.) We view the environment part $a_{1}.e_{1};\ldots;a_{n}.e_{n}$ as a
multiset. We can rename these binders, obtaining an equivalent expression. For
instance, $({\tt letrec}~{}a.(f\,a)~{}{\tt in}~{}(g\,a))\sim({\tt
letrec}~{}b.(f\,b)~{}{\tt in}~{}(g\,b))$ 333Here we will use $\sim$ informally
as $\alpha$-equivalence, which will be formally defined in Def. 3.1. Moreover,
we can also swap the order of definitions. For instance, $({\tt
letrec}~{}a.f;b.g~{}{\tt in}~{}(h\,a\,b))\sim({\tt letrec}~{}b.g;a.f~{}{\tt
in}~{}(h\,a\,b))$. Schmidt-Schauß et al. [38] prove that equivalence of letrec
expressions is graph-isomorphism (GI) complete and Schmidt-Schauß and Sabel
[36] prove that unification is NP-complete. The GI-hardness can be elegantly
proved by encoding any graph, like
$G=(V,E)=(\\{v_{1},v_{2},v_{3}\\},\\{(v_{1},v_{2}),(v_{2},v_{3})\\})$, into a
letrec expression, like $({\tt letrec}~{}v_{1}.a;v_{2}.a;v_{3}.a$ ${\tt
in}~{}{\tt letrec}~{}e_{1}.(c\,v_{1}\,v_{2});e_{2}.(c\,v_{2}\,v_{3})~{}{\tt
in}~{}a)$. Here, $v_{i}$ represent the nodes and $(c\,v_{i}\,v_{j})$ the edges
of the graph.

There are nontrivial fixpoints of permutations in the letrec-language. For
example, $({\tt letrec}~{}a_{1}.b_{1},$ $a_{2}.b_{2},a_{3}.a_{3}~{}{\tt
in}~{}a_{3})$ is a fixpoint of the equation $X\doteq(b_{1}~{}b_{2})\cdot X$,
although $b_{1}$ and $b_{2}$ are not fresh in the expression, which means
$(b_{1}~{}b_{2}){\cdot}({\tt letrec}~{}a_{1}.b_{1},$
$a_{2}.b_{2},a_{3}.a_{3}~{}{\tt in}~{}a_{3})$ $\sim$ $({\tt
letrec}~{}a_{1}.b_{1},$ $a_{2}.b_{2},a_{3}.a_{3}~{}{\tt in}~{}a_{3})$.
Therefore, the fixpoint rule of the nominal algorithm in [6] would not be
complete in our setting: to ensure $X\doteq(b_{1}~{}b_{2})\cdot X$ we cannot
require $b_{1}\\#X$ and $b_{2}\\#X$. See also Example 3.2. Hence, fixpoint
equations can in general not be replaced by freshness constraints. For the
general case we need a complex elimination rule, called fixed point shift:

(FixPointShift) ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}X\doteq\pi^{\prime}_{1}{\cdot}X,\ldots,\pi_{n}{\cdot}X\doteq\pi^{\prime}_{n}{\cdot}X,\pi{\cdot}X\doteq
e\\}}{\Gamma\cup\\{\pi_{1}\pi^{-1}{\cdot}e\doteq\pi^{\prime}_{1}\pi^{-1}{\cdot}e,\ldots,\pi_{n}\pi^{-1}{\cdot}e\doteq\pi^{\prime}_{n}\pi^{-1}{\cdot}e\\}}}$,
if $X$ neither occurs in $e$ nor in $\Gamma$.

The substitution is $X\to\pi^{-1}{\cdot}e$. This rule can generate an
exponential number of equations (see Example 4.6). In order to avoid this
effect, we will use a property on the number of generators of permutation
groups (see end of Section 3).

For the decomposition of letrec expressions we also need to introduce a (don’t
know) nondeterministic choice.
${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{{\tt
letrec}~{}a_{1}.s_{1};\ldots;a_{n}.s_{n}~{}{\tt in}~{}r\doteq{\tt
letrec}~{}b_{1}.t_{1};\ldots;b_{n}.t_{n}~{}{\tt
in}~{}r^{\prime}\\}}{\mid_{\\{\rho\\}}(\Gamma\,\cup\\{s_{1}\doteq\pi{\cdot}t_{\rho(1)},\ldots,s_{n}\doteq\pi{\cdot}t_{\rho(n)},r\doteq\pi{\cdot}r^{\prime}\\}}}$

Where the necessary freshness constraints are $\\{a_{i}\\#({\tt
letrec}~{}b_{1}.t_{1};\ldots;b_{n}.t_{n}~{}{\tt in}~{}r^{\prime})\mid
i=1,\ldots,n\\}$. The permutation $\rho$ on $\\{1,\ldots,n\\}$ is chosen using
don’t-know non-determinism, indicated by the vertical bar and $\\{\rho\\}$,
and $\pi$ is an (atom-)permutation that extends $\\{b_{\rho(i)}\mapsto
a_{i}\mid i=1,\ldots,n)\\}$ with
$\mathit{dom}(\pi)\subseteq\\{a_{1},\ldots,a_{n},b_{1},\ldots,b_{n}\\}$.

In Section 4, we will describe in full detail all the transformation rules of
our algorithm.

##  3 The ground language of expressions

The very first idea of nominal techniques [6] is to use concrete variable
names in lambda-calculi (also in extensions), in order to avoid implicit
$\alpha$-renamings, and instead use operations for explicitly applying
bijective renamings. Suppose $s=\lambda{\tt x}.{\tt x}$ and $t=\lambda{\tt
y}.{\tt y}$ are concrete (syntactically different) lambda-expressions. The
nominal technique provides explicit name-changes using permutations. These
permutations are applied irrespective of binders. For example $({\tt x}~{}{\tt
y}){\cdot}(\lambda{\tt x}.\lambda{\tt x}.{\tt a})$ results in $\lambda{\tt
y}.\lambda{\tt y}.{\tt a}$. Syntactic reasoning on higher-order expressions,
for example unification of higher-order expressions modulo
$\alpha$-equivalence will be emulated by nominal techniques on a language with
concrete names, where the algorithms require certain extra constraints and
operations. The gain is that all conditions and substitutions etc. can be
computed and thus more reasoning tasks can be automated, whereas the implicit
name conditions under non-bijective renamings have a tendency to complicate
(unification-) algorithms and to hide the required conditions on
equality/disequality/occurrence/non-occurrence of names. We will stick to a
notation closer to lambda calculi than most other papers on nominal
unification, however, note that in general the differences are only in
notation and the constructs like application and abstraction can easily be
translated into something equivalent in the other language without any loss.

###  3.1 Preliminaries

We define the language $\mathit{LRL}$ (LetRec Language) of
(ground-)expressions, which is a lambda calculus extended with a recursive let
construct. The notation is consistent with [6]. The (infinite) set of atoms
$\mathbb{A}$ is a set of (concrete) symbols $a,b$ which we usually denote in a
meta-fashion; so we can use symbols $a,b$ also with indices (the variables in
lambda-calculus). There is a set ${\cal F}$ of function symbols with arity
$\mathit{ar}(\cdot)$. The syntax of the expressions $e$ of $\mathit{LRL}$ is:

$e::=a\mid\lambda a.e\mid(f~{}e_{1}~{}\ldots~{}e_{\mathit{ar}(f)})\mid({\tt
letrec}~{}a_{1}.e_{1};\ldots;a_{n}.e_{n}~{}{\tt in}~{}e)$

We assume that binding atoms $a_{1},\ldots,a_{n}$ in a letrec-expression
$({\tt letrec}~{}a_{1}.e_{1};\ldots;$ $a_{n}.e_{n}~{}{\tt in}~{}e)$ are
pairwise distinct. Sequences of bindings $a_{1}.e_{1};\ldots;a_{n}.e_{n}~{}$
may be abbreviated as $\mathit{env}$. The expressions $({\tt
letrec}~{}a_{1}.e_{1};\ldots;a_{n}.e_{n}~{}{\tt in}~{}e)$ and $({\tt
letrec}~{}a_{\rho(1)}.e_{\rho(1)};\ldots;a_{\rho(n)}.e_{\rho(n)}~{}{\tt
in}~{}e)$ are defined as equivalent for every permutation $\rho$ of
$\\{1,\ldots,n\\}$, i.e. in the following we view the environment
$a_{1}.e_{1};\ldots;a_{n}.e_{n}$ of a letrec-expression as a multi-set.

The scope of atom $a$ in $\lambda a.e$ is standard: $a$ has scope $e$. The
${\tt letrec}$-construct has a special scoping rule: in $({\tt
letrec}~{}a_{1}.s_{1};\ldots;a_{n}.s_{n}~{}{\tt in}~{}r)$, every atom $a_{i}$
that is free in some $s_{j}$ or $r$ is bound by the environment
$a_{1}.s_{1};\ldots;a_{n}.s_{n}$. This defines in $\mathit{LRL}$ the notion of
free atoms $\mathit{FA}(e)$, bound atoms $\mathit{BA}(e)$ in expression $e$,
and all atoms $\mathit{AT}(e)$ in $e$. For an environment
$\mathit{env}=\\{a_{1}.e_{1},\ldots,a_{n}.e_{n}\\}$, we define the set of
letrec-atoms as $\mathit{LA}(\mathit{env})=\\{a_{1},\ldots,a_{n}\\}$. Note
that this is well-defined, since environments are multisets, but names are
meant syntactically. We say $a$ is fresh for $e$ iff $a\not\in\mathit{FA}(e)$
(also denoted as $a\\#e$). As an example, the expression $({\tt
letrec}~{}a.\mathit{cons}~{}s_{1}~{}b;b.cons~{}s_{2}~{}a~{}{\tt in}~{}a)$
represents an infinite list
$(cons~{}s_{1}~{}(cons~{}s_{2}~{}(cons~{}s_{1}~{}(cons~{}s_{2}~{}\ldots))))$,
where $s_{1},s_{2}$ are expressions. The functional application operator in
functional languages (which is usally implicit) can be encoded by a binary
function app, which also allows to deal with partial applications. Our
language $\mathit{LRL}$ is a fragment of core calculi [18, 19], since for
example the case-construct is missing, but this could also be represented.

We will use mappings on atoms from $\mathbb{A}$. A swapping $(a~{}b)$ is a
bijective function (on $\mathit{LRL}$-expressions) that maps an atom $a$ to
atom $b$, atom $b$ to $a$, and is the identity on other atoms. We will also
use finite permutations $\pi$ on atoms from $\mathbb{A}$, which could be
represented as a composition of swappings in the algorithms below. Let
$\mathit{dom}(\pi)=\\{a\in\mathbb{A}\mid\pi(a)\not=a\\}$. Then every finite
permutation can be represented by a composition of at most
$(|\mathit{dom}(\pi)|-1)$ swappings. Composition $\pi_{1}\circ\pi_{2}$ and
inverse $\pi^{-1}$ can be immediately computed, where the complexity is
polynomial in the size of $\mathit{dom}(\pi)$. Permutations $\pi$ operate on
expressions simply by recursing on the structure. For a letrec-expression this
is $\pi\cdot({\tt letrec}~{}a_{1}.s_{1};\ldots;a_{n}.s_{n}~{}{\tt in}~{}e)$
$=$ $({\tt letrec}~{}\pi\cdot a_{1}.\pi\cdot s_{1};\ldots;\pi\cdot
a_{n}.\pi\cdot s_{n}~{}{\tt in}~{}\pi\cdot e)$. Note that permutations also
change names of bound atoms.

We will use the following definition (characterization) of
$\alpha$-equivalence:

###### Definition 3.1

The $\alpha$-equivalence $\sim$ on expressions $e\in\mathit{LRL}$ is defined
as follows:

  * •

$a\sim a$.

  * •

if $e_{i}\sim e_{i}^{\prime}$ for all $i$, then $(fe_{1}\ldots
e_{n})\sim(fe_{1}^{\prime}\ldots e_{n}^{\prime})$ for an $n$-ary $f\in{\cal
F}$.

  * •

If $e\sim e^{\prime}$, then $\lambda a.e\sim\lambda a.e^{\prime}$.

  * •

If $a\\#e^{\prime}$ and $e\sim(a~{}b)\cdot e^{\prime}$, then $\lambda
a.e\sim\lambda b.e^{\prime}$.

  * •

If there is a permutation $\pi$ on atoms such that

    * –

$\mathit{dom}(\pi)\subseteq\\{a_{1},\ldots,a_{n}\\}\cup\\{b_{1},\ldots,b_{n}\\}$,
where $a_{i}\not=a_{j}$ and $b_{i}\not=b_{j}$ for all $i\not=j$,

    * –

$\pi(b_{i})=a_{i}$ for all $i$,

    * –

$\\{a_{1},\ldots,a_{n}\\}\\#({\tt
letrec}~{}b_{1}.t_{1},\ldots,b_{n}.t_{n}~{}{\tt in}~{}r^{\prime})$, and

    * –

$r\sim\pi(r^{\prime})$ and $s_{i}\sim\pi(t_{i})$ for $i=1,\ldots,n$ hold.

Then $({\tt letrec}~{}a_{1}.s_{1},\ldots,a_{n}.s_{n}~{}{\tt in}~{}r)\sim({\tt
letrec}~{}b_{1}.t_{1},\ldots,b_{n}.t_{n}~{}{\tt in}~{}r^{\prime})$.

The last phrase includes $({\tt
letrec}~{}a_{1}.s_{1},\ldots,a_{n}.s_{n}~{}{\tt in}~{}r)\sim({\tt
letrec}~{}b_{\rho(1)}.t_{\rho(1)},\ldots,b_{\rho(n)}.t_{\rho(n)}$ ${\tt in}$
$~{}r^{\prime})$ for every permutation $\rho$ on $\\{1,\ldots,n\\}$, by the
definition of syntactic equality that treats the let-environment as a multi-
set.

Note that $\\{a_{1},\ldots,a_{n}\\}\\#({\tt
letrec}~{}b_{1}.t_{1},\ldots,b_{n}.t_{n}~{}{\tt in}~{}r^{\prime})$ is
equivalent to
$(\\{a_{1},\ldots,a_{n}\\}\setminus\\{b_{1},\ldots,b_{n}\\})$ $\\#$ $({\tt
letrec}~{}b_{1}.t_{1},\ldots,b_{n}.t_{n}~{}{\tt in}~{}r^{\prime})$. Note also
that $\sim$ is identical to $\alpha$-equivalence, i.e., the relation generated
by renamings of binding constructs and permutation of bindings in a letrec. We
omit a proof, since it detracts the attention from the main contents. Such a
proof is not hard to construct by using that $\alpha$-equivalence holds, if
and only if the graph constructed by replacing bindings by pointing edges,
where the outgoing edges from an environment are unordered and the one from a
function application are ordered. Note that our view is that algorithms work
on the syntactic terms as given, and not with equivalence classes modulo
$\sim$.

A nice and important property that is often implicitly used is: $e_{1}\sim
e_{2}$ is equivalent to $\pi{\cdot}e_{1}\sim\pi{\cdot}e_{2}$ for any
(atom-)permutation $\pi$.

In usual nominal unification, the solutions of fixpoint equations
$X\doteq\pi{\cdot}X$, i.e. the sets $\\{e\mid\pi\cdot e\sim e\\}$ can be
characterized by using finitely many freshness constraints [6]. Clearly, all
these sets and also all finite intersections are nonempty, since at least
fresh atoms are elements and since $\mathbb{A}$ is infinite. However, in our
setting, these sets are nontrivial:

###### Example 3.2

The $\alpha$-equivalence $(a~{}b)\cdot({\tt letrec}~{}c.a;d.b~{}{\tt
in}~{}\mathit{True})$ $\sim$ $({\tt letrec}~{}\allowbreak c.a;d.b~{}{\tt
in}~{}\mathit{True})$ holds, which means that there are expressions $t$ in
$\mathit{LRL}$ with $t\sim(a~{}b)\cdot t$ and $\mathit{FA}(t)=\\{a,b\\}$. This
is in contrast to usual nominal unification.

###  3.2 Permutation groups

Below we will use the results on complexity of operations in finite
permutation groups, see [39, 40]. We summarize some facts on the so-called
symmetric group and its properties. We consider a set
$\\{o_{1},\ldots,o_{n}\\}$ of distinct objects $o_{i}$ (in our case atoms),
and the symmetric group $\Sigma(\\{o_{1},\ldots,o_{n}\\})$ (of size $n!$) of
permutations of these objects. We will also look at its elements, subsets and
subgroups. Subgroups of $\Sigma(\\{o_{1},\ldots,o_{n}\\})$ can always be
represented by a set of generators (represented as permutations on
$\\{o_{1},\ldots,o_{n}\\}$). If $H$ is a set of elements (or generators), then
$\langle H\rangle$ denotes the generated subgroup of
$\Sigma(\\{o_{1},\ldots,o_{n}\\})$. Some facts are:

  * •

A permutation can be represented in space linear in $n$.

  * •

Every subgroup of $\Sigma(\\{o_{1},\ldots,o_{n}\\})$ can be represented by
$\leq n^{2}$ generators.

However, elements in a subgroup may not be representable as a product of
polynomially many of these generators.

The following questions can be answered in polynomial time:

  * •

The element-question: $\pi\in G$.

  * •

The subgroup question: $G_{1}\subseteq G_{2}$.

However, intersection of groups and set-stabilizer (i.e. $\\{\pi\in
G\mid\pi(M)=M\\}$) are not known to be computable in polynomial time, since
those problems are as hard as graph-isomorphism (see [39]).

##  4 A nominal letrec unification algorithm

###  4.1 Preparations

As an extension of $\mathit{LRL}$, there is a countably infinite set of
(unification) variables $\mathit{Var}$ ranged over by $X,Y$ where we also use
indices. The syntax of the language $\mathit{LRLX}$ (LetRec Language eXtended)
is

$\begin{array}[]{lcl}e&::=&a\mid X\mid\pi\cdot{}X\mid\lambda
a.e\mid(f~{}e_{1}~{}\ldots e_{\mathit{ar}(f)})~{}|~{}({\tt
letrec}~{}a_{1}.e_{1};\ldots;a_{n}.e_{n}~{}{\tt in}~{}e)\\\
\pi&:=&\emptyset\mid(a~{}b){\cdot}\pi\end{array}$

$\mathit{Var}(e)$ is the set of variables $X$ occurring in $e$.

$\displaystyle\displaystyle{\hbox{\hskip
22.47661pt\vbox{\hbox{\hskip-22.47661pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}b\\}\mathaccent
0{\cdot}\cup\nabla$}}}\vbox{}}}\over\hbox{\hskip
4.50002pt\vbox{\vbox{}\hbox{\hskip-4.5pt\hbox{\hbox{$\displaystyle\displaystyle\nabla$}}}}}}$
if $a\neq b$ $\displaystyle\displaystyle{\hbox{\hskip
38.59769pt\vbox{\hbox{\hskip-38.59767pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}(f~{}s_{1}\ldots
s_{n})\\}\mathaccent 0{\cdot}\cup\nabla$}}}\vbox{}}}\over\hbox{\hskip
39.45705pt\vbox{\vbox{}\hbox{\hskip-39.45703pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}s_{1},\ldots,a{{\\#}}s_{n}\\}\cup\nabla$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
33.1584pt\vbox{\hbox{\hskip-33.1584pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}(\lambda
a.s)\\}\mathaccent 0{\cdot}\cup\nabla$}}}\vbox{}}}\over\hbox{\hskip
4.50002pt\vbox{\vbox{}\hbox{\hskip-4.5pt\hbox{\hbox{$\displaystyle\displaystyle\nabla$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
32.711pt\vbox{\hbox{\hskip-32.71098pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}(\lambda
b.s)\\}\mathaccent 0{\cdot}\cup\nabla$}}}\vbox{}}}\over\hbox{\hskip
21.40474pt\vbox{\vbox{}\hbox{\hskip-21.40474pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}s\\}\cup\nabla$}}}}}}$
if $a\neq b$

$\displaystyle\displaystyle{\hbox{\hskip
70.35474pt\vbox{\hbox{\hskip-70.35472pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}({\tt
letrec}~{}a_{1}.s_{1};\ldots,a_{n}.s_{n}~{}{\tt in}~{}r)\\}\mathaccent
0{\cdot}\cup\nabla$}}}\vbox{}}}\over\hbox{\hskip
4.50002pt\vbox{\vbox{}\hbox{\hskip-4.5pt\hbox{\hbox{$\displaystyle\displaystyle\nabla$}}}}}}$
if $a\in\\{a_{1},\ldots,a_{n}\\}$ $\displaystyle\displaystyle{\hbox{\hskip
22.92403pt\vbox{\hbox{\hskip-22.92401pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}a\\}\mathaccent
0{\cdot}\cup\nabla$}}}\vbox{}}}\over\hbox{\hskip
4.50002pt\vbox{\vbox{}\hbox{\hskip-4.5pt\hbox{\hbox{$\displaystyle\displaystyle\bot$}}}}}}$

$\displaystyle\displaystyle{\hbox{\hskip
70.35474pt\vbox{\hbox{\hskip-70.35472pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}({\tt
letrec}~{}a_{1}.s_{1};\ldots,a_{n}.s_{n}~{}{\tt in}~{}r)\\}\mathaccent
0{\cdot}\cup\nabla$}}}\vbox{}}}\over\hbox{\hskip
48.1576pt\vbox{\vbox{}\hbox{\hskip-48.15758pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}s_{1},\ldots
a{{\\#}}s_{n},a{{\\#}}r\\}\cup\nabla$}}}}}}$ if
$a\not\in\\{a_{1},\ldots,a_{n}\\}$ $\displaystyle\displaystyle{\hbox{\hskip
33.94173pt\vbox{\hbox{\hskip-33.94173pt\hbox{\hbox{$\displaystyle\displaystyle\\{a{{\\#}}(\pi\cdot
X)\\}\mathaccent 0{\cdot}\cup\nabla$}}}\vbox{}}}\over\hbox{\hskip
31.54173pt\vbox{\vbox{}\hbox{\hskip-31.54172pt\hbox{\hbox{$\displaystyle\displaystyle\\{\pi^{-1}(a){{\\#}}X\\}\cup\nabla$}}}}}}$

Figure 1: Simplification of freshness constraints in $\mathit{LRLX}$

The expression $\pi{\cdot}e$ for a non-variable $e$ means an operation, which
is performed by shifting $\pi$ down, using the additional simplification
$\pi_{1}{\cdot}(\pi_{2}{\cdot}e)$ $\to$ $(\pi_{1}\circ\pi_{2}){\cdot}e$, where
after the shift, $\pi$ only occurs in the subexpressions of the form
$\pi\cdot{}X$, which are called suspensions. Usually, we do not distinguish
$X$ and $\mathit{Id}{\cdot}X$, notationally. A single freshness constraint in
our unification algorithm is of the form $a{{\\#}}e$, where $e$ is an
$\mathit{LRLX}$-expression, and an atomic freshness constraint is of the form
$a{{\\#}}X$. A conjunction (or set) of freshness constraints is sometimes
called freshness context.

###### Lemma 4.1

The rules in Fig. 1 for simplifying sets of freshness constraints in
$\mathit{LRLX}$ run in polynomial time and the result is either $\bot$, i.e.
fail, or a set of freshness constraints where all single constraints are
atomic. This constitutes a polynomial decision algorithm for satisfiability of
$\nabla$: If $\bot$ is in the result, then unsatisfiable, otherwise
satisfiable.

We can assume in the following algorithms that sets of freshness constraint
are immediately simplified. In the following we will use
$\mathit{Var}(\Gamma,\nabla)$, and $\mathit{Var}(\Gamma,e)$ and similar
notation for the set of unification-variables occurring in the syntactic
objects mentioned in the brackets.

###### Definition 4.2

An $\mathit{LRLX}$-unification problem is a pair $(\Gamma,\nabla)$, where
$\Gamma$ is a set of equations $\\{s_{1}\doteq t_{1},\ldots,s_{n}\doteq
t_{n}\\}$, and $\nabla$ is a set of freshness constraints
$\\{a_{1}{\\#}X_{1},\ldots,a_{m}{\\#}X_{m}\\}$. A (ground) solution of
$(\Gamma,\nabla)$ is a substitution $\rho$, mapping variables in
$\mathit{Var}(\Gamma,\nabla)$ to ground expressions, such that $s_{i}\rho\sim
t_{i}\rho$, for $i=1,\ldots,n$, and $a_{j}\\#(X_{j}\rho)$, for $j=1,\ldots,m$.
The decision problem is whether there is a ground solution for a given
$(\Gamma,\nabla)$ or not.

For the unification algorithms below, we employ a representation of unifiers
as iterated single substitutions which is like a DAG-compression of a
substitution. For example the representation $\\{x\mapsto f(y,z),y\mapsto
f(a,a),z\mapsto g(b,b)\\}$ represents the substitution $\\{x\mapsto
f(f(a,a),g(b,b)),y\mapsto f(a,a),z\mapsto g(b,b)\\}$.

###### Definition 4.3

Let $(\Gamma,\nabla)$ be an $\mathit{LRLX}$-unification problem. We consider
triples $(\sigma,\nabla^{\prime},\mathit{FIX})$ as representing general
unifiers, where $\sigma$ is a substitution represented by a sequence of single
assignments (which has the effect of a DAG-compression), mapping variables to
$\mathit{LRLX}$-expressions, $\nabla^{\prime}$ is a set of freshness
constraints, and $\mathit{FIX}$ is a set of fixpoint equations of the form
$\pi^{\prime}{\cdot}X\doteq\pi{\cdot}X$, where $X\not\in\mathit{dom}(\sigma)$.

A triple $(\sigma,\nabla^{\prime},\mathit{FIX})$ is a unifier of
$(\Gamma,\nabla)$, if

  * (i)

there exists a ground substitution $\rho$ that solves
$(\nabla^{\prime}\sigma,\mathit{FIX})$, i.e., for every $a{\\#}X$ in
$\nabla^{\prime}$, $a{\\#}X\sigma\rho$ is valid, and for every fixpoint
equation $\pi^{\prime}{\cdot}X\doteq\pi{\cdot}X\in\mathit{FIX}$, it holds
$\pi^{\prime}{\cdot}(X\rho)\sim\pi{\cdot}(X\rho)$; and

  * (ii)

for every ground substitution $\rho$ that instantiates all variables in
$Var(\Gamma,\nabla)$ and which solves $(\nabla^{\prime}\sigma,\mathit{FIX})$,
the ground substitution $\sigma\rho$ is a solution of $(\Gamma,\nabla)$.

A set $M$ of unifiers is complete, if every solution $\mu$ is covered by at
least one unifier, i.e., there is some unifier
$(\sigma,\nabla^{\prime},\mathit{FIX})$ in $M$, and a ground substitution
$\rho$, such that $X\mu\sim X\sigma\rho$ for all
$X\in\mathit{Var}(\Gamma,\nabla)$.

We will employ nondeterministic rule-based algorithms computing unifiers:
There are clearly indicated disjunctive (don’t know nondeterministic) rules,
and all other rules are don’t care nondeterministic. This distinction is
related to the completeness of the solution algorithms: don’t care means that
the rule has several possibilities where it is sufficient for completeness to
take only one. On the other hand, don’t know means that for achieving
completeness, every possibility of the rule has to be explored. The collecting
variant of the algorithm runs and collects all solutions from all alternatives
of the disjunctive rule(s). The decision variant guesses and verifies one
possibility and tries to detect the existence of a single unifier.

Since we want to avoid the exponential size explosion of the Robinson-style
unification, keeping the good properties of Martelli Montanari-style
algorithms [26], we stick to a set of equations as data structure. As a
preparation for the algorithm, all expressions in equations are exhaustively
flattened as follows: $(f~{}t_{1}\ldots t_{n})\to(f~{}X_{1}\ldots X_{n})$ plus
the equations $X_{1}\doteq t_{1},\ldots,X_{n}\doteq t_{n}$. Also $\lambda a.s$
is replaced by $\lambda a.X$ with equation $X\doteq s$, and $({\tt
letrec}~{}a_{1}.s_{1};\ldots,a_{n}.s_{n}~{}{\tt in}~{}r)$ is replaced by
$({\tt letrec}~{}a_{1}.X_{1};\ldots,a_{n}.X_{n}~{}{\tt in}~{}X)$ with the
additional equations $X_{1}\doteq s_{1};\ldots;X_{n}\doteq s_{n};X\doteq r$.
The introduced variables $X_{i},X$ are fresh ones. Thus, all expressions in
equations are of depth at most 1, not counting the permutation applications in
the suspensions.

In the notation of the rules, we use $[e/X]$ as substitution that replaces $X$
by $e$, whereas $\\{X\to t\\}$ is used for constructing a syntactically
represented substitution. In the written rules, we may omit $\nabla$ or
$\theta$ if they are not changed. We will use a notation “$|$” in the
consequence part of a rule, usually with a set of possibilities indicated by
for example $\\{\rho\\}$, to denote disjunctive (i.e. don’t know)
nondeterminism. The only nondeterministic rule that requires exploring all
alternatives is rule (6) in Fig. 2. The other rules can be applied in any
order, where it is not necessary to explore alternatives.

$(1)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{e\doteq
e\\},\nabla,\theta}{\Gamma,\nabla,\theta}}$
$(2)~{}{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}X\doteq\pi_{2}{\cdot}Y\\},\nabla,\theta\qquad
Y\not=X}{\Gamma[\pi_{1}^{-1}\pi_{2}{\cdot}Y/X],\nabla[\pi_{1}^{-1}\pi_{2}{\cdot}Y/X],\theta\cup\\{X\mapsto\pi_{1}^{-1}\pi_{2}{\cdot}Y\\}}}$

$(3)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{(f~{}s_{1}\ldots
s_{n})\doteq(f~{}s_{1}^{\prime}\ldots
s_{n}^{\prime})\\},\nabla,\theta}{\Gamma\cup\\{s_{1}\doteq
s_{1}^{\prime},\ldots,s_{n}\doteq s_{n}^{\prime}\\},\nabla,\theta}}$

$(4)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{\lambda
a.s\doteq\lambda a.t\\},\nabla,\theta}{\Gamma\cup\\{s\doteq
t\\},\nabla,\theta}}$ $(5)~{}{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\lambda a.s\doteq\lambda b.t\\},\nabla,\theta\qquad
a\not=b}{\Gamma\cup\\{s\doteq(a~{}b){\cdot}t\\},\nabla\cup\\{a{{\\#}}t\\},\theta}}$

$(6)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{{\tt
letrec}~{}a_{1}.s_{1};\ldots;a_{n}.s_{n}~{}{\tt in}~{}r\doteq{\tt
letrec}~{}b_{1}.t_{1};\ldots;b_{n}.t_{n}~{}{\tt
in}~{}r^{\prime}\\},\nabla,\theta}{\begin{array}[]{l}\begin{array}[]{ll}{\begin{array}[]{c}\left|\begin{array}[]{c}{}\hfil\\\
\end{array}\right.\\\
{\\{\rho\\}}\end{array}}&\begin{array}[]{l}(\Gamma\,\cup\\{s_{1}\doteq\pi{\cdot}t_{\rho(1)},\ldots,s_{n}\doteq\pi{\cdot}t_{\rho(n)},r\doteq\pi{\cdot}r^{\prime}\\},\\\
~{}~{}~{}\nabla\cup\\{a_{i}\\#({\tt
letrec}~{}b_{1}.t_{1};\ldots;b_{n}.t_{n}~{}{\tt in}~{}r^{\prime})\mid
i=1,\ldots,n\\},\theta)\end{array}\end{array}\\\\[5.69054pt] \mbox{where
$\rho$ is a permutation on $\\{1,\ldots,n\\}$. The permutation $\pi$ is chosen
don't care such that}\\\ \mbox{ it extends $\\{b_{\rho(i)}\mapsto a_{i}\mid
i=1,\ldots,n)\\}$ with
$\mathit{dom}(\pi)\subseteq\\{a_{1},\ldots,a_{n},b_{1},\ldots,b_{n}\\}$ }\\\
\end{array}}}$

Figure 2: Standard (1,2) and decomposition rules (3,4,5,6)

###  4.2 Rules of the algorithm LetrecUnify

(MMS) ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}X\doteq e_{1},\pi_{2}{\cdot}X\doteq
e_{2}\\},\nabla,\theta}{\Gamma\cup\\{\pi_{1}{\cdot}X\doteq
e_{1}\\}\cup\Gamma^{\prime},\nabla\cup\nabla^{\prime},\theta}}$,  if
$e_{1},e_{2}$ are not suspensions, where $\Gamma^{\prime}$ is the set of
equations generated by decomposing
$\pi_{1}^{-1}{\cdot}e_{1}\doteq\pi_{2}^{-1}{\cdot}e_{2}$ using (3)–(6), and
where $\nabla^{\prime}$ is the corresponding resulting set of freshness
constraints.

(FPS) ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}X\doteq\pi^{\prime}_{1}{\cdot}X,\ldots,\pi_{n}{\cdot}X\doteq\pi^{\prime}_{n}{\cdot}X,\pi{\cdot}X\doteq
e\\},\nabla,\theta}{\Gamma\cup\\{\pi_{1}\pi^{-1}{\cdot}e\doteq\pi^{\prime}_{1}\pi^{-1}{\cdot}e,\ldots,\pi_{n}\pi^{-1}{\cdot}e\doteq\pi^{\prime}_{n}\pi^{-1}{\cdot}e\\},\nabla,\theta\cup\\{X\mapsto\pi^{-1}{\cdot}e\\}}}$,

If neither $X\in\mathit{Var}(\Gamma,e)$, nor $e$ is a suspension, nor (Cycle)
(see Fig.4) is applicable.

(ElimFP) ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}X\doteq\pi^{\prime}_{1}{\cdot}X,\ldots,\pi_{n}{\cdot}X\doteq\pi^{\prime}_{n}{\cdot}X,\pi{\cdot}X\doteq\pi^{\prime}{\cdot}X\\},\nabla,\theta}{\Gamma\cup\\{\pi_{1}{\cdot}X\doteq\pi^{\prime}_{1}{\cdot}X,\ldots,\pi_{n}{\cdot}X\doteq\pi^{\prime}_{n}{\cdot}X\\},\nabla,\theta}}$,

If
$\pi^{-1}\pi^{\prime}\in\langle\pi_{1}^{-1}\pi_{1}^{\prime},\ldots,\pi_{n}^{-1}\pi_{n}^{\prime}\rangle.$

(Output) ${\displaystyle\frac{\Gamma,\nabla,\theta}{(\theta,\nabla,\Gamma)}}$
if $\Gamma$ only consists of fixpoint-equations.

Figure 3:  Main Rules of LetrecUnify

The top symbol of an expression is defined as $\mathit{tops}(f~{}s_{1}\ldots
s_{n})=f$, $\mathit{tops}(a)=a$, $\mathit{tops}(\lambda a.s)=\lambda$, and
$\mathit{tops}({\tt letrec}~{}\mathit{env}~{}{\tt in}~{}s)=({\tt letrec},n)$,
where $n$ is the number of bindings in $env$. It is undefined for variables
$X$.

###### Definition 4.4

The rule-based algorithm LetrecUnify is defined in the following. Its rules
are in Figs. 2, 3 and 4. LetrecUnify operates on a tuple
$(\Gamma,\nabla,\theta)$, where $\Gamma$ is a set of flattened equations
$e_{1}\doteq e_{2}$, and where we assume that $\doteq$ is symmetric, $\nabla$
contains freshness constraints, and $\theta$ represents the already computed
substitution as a list of mappings of the form $X\mapsto e$. Initially
$\theta$ is empty.

The final state will be reached, i.e. the output, when $\Gamma$ only contains
fixpoint equations of the form $\pi_{1}{\cdot}X\doteq\pi_{2}{\cdot}X$ that are
non-redundant, and the rule (Output) fires. Note that the rule (FPS)
represents the usual solution rule if the premise is only a single equation.

The rules (1)–(6), and (ElimFP) have highest priority; then (MMS) and (FPS).
The rule (Output) (lowest priority) terminates an execution on $\Gamma_{0}$ by
outputting a unifier $(\theta,\nabla^{\prime},\mathit{FIX})$. A general
explanation of the vertical-bar-notation is at the end of Subsection 4.1.

We assume that the algorithm LetrecUnify halts if a failure rule (see Fig.4)
is applicable.

(Clash) ${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{s\doteq
t\\},\nabla,\theta~{}~{}~{}tops(s)\not=\mathit{tops}(t)\mbox{ and $s$ and $t$
are not suspensions}}{\bot}}$

(Cycle) ${\displaystyle\frac{\Gamma\cup\\{\pi_{1}{\cdot}X_{1}\doteq
s_{1},\ldots,\pi_{n}{\cdot}X_{n}\doteq
s_{n}\\},\nabla,\theta~{}~{}~{}{\left\\{\begin{array}[]{@{}l}\text{ where
}s_{i}\text{ are not suspensions and }\\\ X_{i+1}\text{ occurs in }s_{i}\text{
for }\\\ i=1,\ldots,n-1\text{ and }X_{1}\text{ occurs in
}s_{n}.\end{array}\right.}}{\bot}}$

(FailF) ${\displaystyle\frac{\Gamma,\nabla\cup\\{a{{\\#}}a\\},\theta}{\bot}}$
(FailFS) ${\displaystyle\frac{\Gamma,\nabla\cup\\{a{{\\#}}X\\},\theta\hskip
17.07164pt\text{ and }a\text{ occurs free in }(X\theta)}{\bot}}$

Figure 4: Failure Rules of LetrecUnify

Note that the two rules (MMS) and (FPS), without further precaution, may cause
an exponential blow-up in the number of fixpoint-equations (see Example 4.6).
The rule (ElimFP) will bound the number of generated fixpoint equations by
exploiting knowledge on operations within permutation groups.

Note that the application of every rule can be done in polynomial time. In
particular rule (FailFS), since the computation of $\mathit{FA}((X)\theta)$
can be done in polynomial time by iterating over the solution components.

###### Example 4.5

We illustrate the letrec-rule (6) by a ground example without flattening. Here
we use pairs, which are functional expressions, i.e., $(s_{1},s_{2})$ means
$f(s_{1},s_{2})$ for a binary function symbol $f$ in the language.

Let the equation be: $({\tt letrec}~{}a.(a,b),b.(a,b)~{}{\tt
in}~{}b)\doteq({\tt letrec}~{}b.(b,c),c.(b,c)~{}{\tt in}~{}c).$ The algorithm
has to follow two possibilities for $\rho$: the identity, and the swapping
$(1~{}2)$.
We show the computation for the identity (position-)permutation $\rho$, which
results in: $\pi=\\{b\mapsto a;$ $c\mapsto b$; $a\mapsto c\\}$, where the
third binding that has to be added, such that the result is a bijection is
$a\mapsto c$, which is not relevant for the result, but unique in this case.
Decomposition of the equations
$(a,b)\doteq\pi{\cdot}(b,c),(a,b)\doteq\pi{\cdot}(b,c),b\doteq\pi{\cdot}c\\}$
is possible without fail and yields only trivial equations.
The freshness constraints are $a{{\\#}}({\tt letrec}~{}b.(b,c),c.(b,c)~{}{\tt
in}~{}c)$ and $b{{\\#}}({\tt letrec}~{}b.(b,c),c.(b,c)~{}{\tt in}~{}c)$, which
holds.

###### Example 4.6

This example shows that FPS (together with the standard and decomposition
rules) may give rise to an exponential number of equations in the size of the
original problem. Let there be variables $X_{i},i=1,\ldots,n$ and the
equations $\Gamma=\\{X_{n}\doteq\pi{\cdot}X_{n},$
$X_{n}\doteq(f~{}X_{n-1}~{}\rho_{n}{\cdot}X_{n-1}),\ldots,X_{2}\doteq(f~{}X_{1}~{}\rho_{2}{\cdot}X_{1})\\}$
where $\pi,\rho_{1},\ldots,\rho_{n}$ are permutations. We prove that this
unification problem may give rise to $2^{n-1}$ equations, if the redundancy
rule (ElimFP) is not there.
The first step is by (FPS):
$\left\\{\begin{array}[]{rcl}f~{}X_{n-1}~{}\rho_{n}{\cdot}X_{n-1}&\doteq&\pi{\cdot}(f~{}X_{n-1}~{}\rho_{n}{\cdot}X_{n-1}),\\\
X_{n-1}&\doteq&(f~{}X_{n-2}~{}\rho_{n-1}{\cdot}X_{n-2}),\ldots\end{array}\right\\}$
Using decomposition and inversion:
$\left\\{\begin{array}[]{rcl}X_{n-1}&\doteq&\pi{\cdot}X_{n-1},\\\
X_{n-1}&\doteq&\rho_{n}^{-1}{\cdot}\pi{\cdot}\rho_{n}{\cdot}X_{n-1},\\\
X_{n-1}&\doteq&(f~{}X_{n-2}~{}\rho_{n-1}{\cdot}X_{n-2}),\ldots\end{array}\right\\}$
After (FPS):
$\left\\{\begin{array}[]{@{}rcl@{}}(f~{}X_{n-2}~{}\rho_{n-1}{\cdot}X_{n-2})&\doteq&\pi{\cdot}(f~{}X_{n-2}~{}\rho_{n-1}{\cdot}X_{n-2}),\\\
(f~{}X_{n-2}~{}\rho_{n-1}{\cdot}X_{n-2})&\doteq&\rho_{n}^{-1}{\cdot}\pi{\cdot}\rho_{n}{\cdot}(f~{}X_{n-2}~{}\rho_{n-1}{\cdot}X_{n-2}),\\\
X_{n-2}&\doteq&(f~{}X_{n-3}~{}\rho_{n-2}{\cdot}X_{n-3}),\ldots\\\
\end{array}\right\\}$
Decomposition and inversion:
$\left\\{\begin{array}[]{rcl}X_{n-2}&\doteq&\pi{\cdot}X_{n-2},\\\
X_{n-2}&\doteq&\rho_{n-1}^{-1}{\cdot}\pi{\cdot}\rho_{n-1}{\cdot}X_{n-2},\\\
X_{n-2}&\doteq&\rho_{n}^{-1}{\cdot}\pi{\cdot}\rho_{n}{\cdot}X_{n-2},\\\
X_{n-2}&\doteq&\rho_{n-1}^{-1}{\cdot}\rho_{n}^{-1}{\cdot}\pi{\cdot}\rho_{n}{\cdot}\rho_{n-1}{\cdot}X_{n-2},\\\
X_{n-2}&\doteq&(f~{}X_{n-3}~{}\rho_{n-2}{\cdot}X_{n-3}),\ldots\\\
\end{array}\right\\}$
Now it is easy to see that all equations $X_{1}\doteq\pi^{\prime}{\cdot}X_{1}$
are generated, with $\pi^{\prime}\in\\{\rho^{-1}\pi\rho$ where $\rho$ is a
composition of a subsequence of $\rho_{n},\rho_{n-1},\ldots,\rho_{2}\\}$,
which makes $2^{n-1}$ equations. The permutations are pairwise different using
an appropriate choice of $\rho_{i}$ and $\pi$. The starting equations can be
constructed using the decomposition rule of abstractions.

Without (ElimFP) all elements of the generated group of permutations have to
be implicitly stored in $\Gamma$. The rule (ElimFP) would permit to only keep
a set of generators of the group of permutations. The explicit algorithmic
treatment of generators and group operations is standard and not explained in
this paper.

##  5 Soundness, completeness, and complexity of LetrecUnify

###  5.1 NP-Hardness of nominal letrec unification and matching

First we show that a restricted problem class of nominal letrec unification is
already NP-hard. If the equations for unification are of the form $s_{1}\doteq
t_{1},\ldots,s_{n}\doteq t_{n}$, and the expressions $t_{i}$ do not contain
variables $X_{i}$, then this is a nominal letrec-matching problem (see also
Section 6).

###### Theorem 5.1

Nominal letrec matching (hence also unification) in $\mathit{LRL}$ is
$\mathit{NP}$-hard, for two letrec expressions, where subexpressions are free
of letrec.

###### Proof 5.2

We encode the $\mathit{NP}$-hard problem of finding a Hamiltonian cycle in a
3-regular graph [41, 42], which are graphs where all nodes have the same
degree $k=3$. Let $G$ be a graph, $a_{1},\ldots,a_{n}$ be the vertexes of the
graph $G$, and $E$ be the set of edges of $G$. The first environment part is
$\mathit{env}_{1}=a_{1}.(node~{}a_{1});\ldots;a_{n}.(node~{}a_{n})$, and a
second environment part $\mathit{env}_{2}$ consists of bindings
$b.(f~{}a~{}a^{\prime})$ and $b^{\prime}.(f~{}a^{\prime}~{}a)$ for every edge
$(a,a^{\prime})\in E$ for fresh names $b,b^{\prime}$. Then let $t:=$ $({\tt
letrec}~{}\mathit{env}_{1};\mathit{env}_{2}~{}{\tt in}~{}0)$ which is intended
to represent the graph. Let the second expression encode the question whether
there is a Hamiltonian cycle in a regular graph as follows: The first part of
the environment is $\mathit{env}_{1}^{\prime}=a_{1}.(node~{}X_{1}),$ $\ldots,$
$a_{n}.(node~{}X_{n})$. The second part is $\mathit{env}_{2}^{\prime}$
consisting of $b_{1}.(f~{}X_{1}~{}X_{2})$; $b_{2}.(f~{}X_{2}~{}X_{3})$;
$\ldots;$ $b_{n}.(f~{}X_{n}~{}X_{1})$, where all $b_{i}$ are different atoms.
This part encodes the Hamiltonian cycle. We also need a third part that
matches the edges that are not part of the Hamiltonian cycle. The third part
$\mathit{env}_{3}^{\prime}$ consists of entries of the form
$b.(f~{}Z~{}Z^{\prime})$, where $b$ is always a fresh atom for every binding,
and $Z,Z^{\prime}$ are fresh variables for every entry. Thus every such entry
matches one edge. The number of these dummy entries can be computed as $3*n-n$
due to the assumption that the degree of $G$ is $3$, and the edges in the
cycle are already covered by the second part. Let $s:=$ $({\tt
letrec}~{}\mathit{env}_{1}^{\prime};\mathit{env}_{2}^{\prime};\mathit{env}_{3}^{\prime}~{}{\tt
in}~{}0)$, representing the question of the existence of the Hamiltonian
cycle. Then the matching problem $s{\ \unlhd\ }t$ is solvable iff the graph
has a Hamiltonian cycle. The degree is $3$, hence it is not possible that
there are shortcuts in the cycle.

###  5.2 Properties of the nominal unification algorithm LetrecUnify

We will use $\mathit{size}(\Gamma)$ for estimating the runtime of LetrecUnify,
which is the sum of the sizes of the equated expressions, and where the size
of an expression is its size as a term tree, where we assume that names have
size 1. We do not count the size of permutations.

For a non-deterministic algorithm outputting unifiers, we explain the
deterministic variant that follows all proper choices, but not the don’t-care
choices, and prints all solutions one after the other. This is called the
collecting (and deterministic) version of the algorithm.

###### Theorem 5.3

The decision variant of the algorithm LetrecUnify runs in nondeterministic
polynomial time, where a single unifier is represented in polynomial space.
The number of rule applications is $O(S^{3}\log(S))$ where $S$ is the size of
the input. The collecting version of LetrecUnify returns exponentially many
unifiers, where their number is bounded by $O(\exp(S^{4})\log(S)))$.

###### Proof 5.4

Let $(\Gamma_{0},\nabla_{0})$ be the input, where $\Gamma_{0}$ is assumed to
be flattened, and $S_{all}$ be $\mathit{size}(\Gamma_{0},\nabla_{0})$. We use
$S=\mathit{size}(\Gamma_{0})$ to argue on the number of steps of LetrecUnify.
The execution of a single rule can be done in polynomial time depending on the
size of the intermediate state, thus we have to show that the size of the
intermediate states remains polynomial and that the number of rule
applications is at most polynomial.

The number of fixpoint-equations for every variable $X$ is at most $S*\log(S)$
since the number of atoms is never increased, and since we assume that
(ElimFP) is applied whenever possible. The size of the permutation group on
the set of all atoms in the input is at most $S!$, and so the length of proper
subset-chains and hence the maximal number of (necessary) generators of a
subgroup is at most $\log(S!)\leq S*\log(S)$. The redundancy of generators can
be tested in polynomial time depending on the number of atoms. Note also that
applicability of (ElimFP) can be tested in polynomial time by checking the
maximal possible subsets.

The lexicographically ordered termination measure
$({\\#\mathrm{Var}},{\\#\mathrm{Lr}\lambda\mathrm{FA}},{\\#\mathrm{Eqs}})$ is
used:

  1. 1.

${\\#\mathrm{Var}}$ is the number of different variables in $\Gamma$,

  2. 2.

${\\#\mathrm{Lr}\lambda\mathrm{FA}}$ is the number of letrec-, $\lambda$,
function-symbols and atoms in $\Gamma$, but not in permutations,

  3. 3.

${\\#\mathrm{Eqs}}$ is the number of equations in $\Gamma$.

Since shifting permutations down and simplification of freshness constraints
both terminate in polynomial time, and do not increase the measures, we only
compare states which are normal forms for shifting down permutations and
simplifying freshness constraints. The following table shows the effect of the
rules:

The entries $+m$ represents an increase of at most $m$ in the relevant measure
component. This form of table permits an easy check that the complexity of a
single run is polynomial. Note that we omit the failure rules in the table,
since these stop immediately.

$\begin{array}[]{l||l|l|l|l}&{\\#\mathrm{Var}}&{\\#\mathrm{Lr}\lambda\mathrm{FA}}&{\\#\mathrm{Eqs}}\\\
\hline\cr(2)&<&\leq&<\\\ \mbox{(FPS)}&<&+2S\log(S)&<\\\
\mbox{(MMS)}&=&<&+2S\\\ (3),(4),(5),(6)&=&<&+S\\\ \mbox{(ElimFP)}&=&=&<\\\
(1)&\leq&\leq&<\\\ \end{array}$

The table shows that every rule application strictly decreases the
lexicographic measure as a combination of the three basic measures. The
entries can be verified by checking the rules, and using the argument that
there are not more than $S\log(S)$ fixpoint equations for a single variable
$X$. We use the table to argue on the (overall) number of rule applications
and hence the complexity: The rules (2) and (FPS) strictly reduce the number
of variables in $\Gamma$ and can be applied at most $S$ times. (FPS) increases
the second measure at most by $2*S\log(S)$, since the number of symbols may be
increased as often as there are fixpoint-equations and there are at most
$S\log(S)$. Since no other rule increases the measure,
${\\#\mathrm{Lr}\lambda\mathrm{FA}}$ will never be greater than
$2S^{2}\log(S)$. The rule (MMS) strictly decreases
${\\#\mathrm{Lr}\lambda\mathrm{FA}}$. Hence${\\#\mathrm{Eqs}}$, i.e. the
number of equations is bounded by $4S^{3}\log(S)$. Thus, the number of rule
applications is $O(S^{3}\log(S))$.
The complexity of applications of single rules is polynomial, in particular
(FPS), see Section 3.2. The complexity of the constraint simplification (Lemma
4.1) is also polynomial. We also have to argue on the failure rules. These
detect all fail cases, and the size of the state part $\nabla$ remains
polynomial. The checks within the failure rules can be done in polynomial time
in $S_{all}$, where the argument for polynomiality of the check in (FailFS) is
an algorithm that iteratively applies parts of $\theta$ and checks.

The arguments for the complexity of the size a single solution are already
given. Additional arguments are needed for an upper bound on the number of
solutions for the collecting version of LetrecUnify. An upper bound on the
number of different possibilities that have to be explored at a single rule
application of (6) is $O(\exp(S))$. In a single run of LetrecUnify the number
of executions of (6) is at most $O(S^{3}\log(S))$, hence we obtain an
exponential bound $\exp(S^{4})\log(S))$ for the number of solutions that are
outputted by the collecting version.

###### Theorem 5.5

The algorithm LetrecUnify is sound and complete. I.e., every computed unifier
is a unifier of the input problem (soundness), and for every ground unifier of
the input problem, there is a run of the (non-deterministic) algorithm that
produces a unifier that has the ground unifier as an instance.

###### Proof 5.6

Soundness of the algorithm holds, by easy arguments for every rule, similar as
in [6], and since the letrec-rule follows the definition of $\sim$ in Def.
3.1. A further argument is that the failure rules are sufficient to detect
states without solutions.

Completeness requires more arguments. The decomposition and standard rules,
with the exception of rule (6), retain the set of solutions. The same for
(MMS), (FPS), and (ElimFP). Note that the nondeterminism in (ElimFP) does not
affect the current set of solutions. The nondeterministic rule (6) provides
all possibilities for potential ground solutions. Moreover, the failure rules
are not applicable to states that are solvable.

A final output of LetrecUnify for a solvable input has at least one ground
solution as instance: we can instantiate all variables that remain in
$\Gamma_{\mathit{out}}$ by a fresh atom. Then all fixpoint equations are
satisfied, since the permutations cannot change this atom, and since the
(atomic) freshness constraints hold. This ground solution can be represented
in polynomial space by using $\theta$, plus an instance $X\mapsto a$ for all
remaining variables $X$ and a fresh atom $a$, and removing all fixpoint
equations and freshness constraints.

###### Theorem 5.7

The nominal letrec-unification problem is $\mathit{NP}$-complete.

###### Proof 5.8

This follows from Theorems 5.3 and 5.5, and Theorem 5.1.

##  6 Nominal matching with letrec: LetrecMatch

Reductions using reductions rules of the form $l\to r$ in higher order calculi
with letrec, for example in a core-language of Haskell, require a (nominal)
matching algorithm, matching the rules’ left hand side to an expression or
subexpression that is to be transformed. An example is the beta-reduction (see
the example below), but also a lot of other transformation rules can serve as
examples. For the application it is sufficient if the instance of the right
hand side $r\sigma$ is ground if $l\sigma$ is ground, and the variable
convention holds for $r\sigma$. In [32] nominal rewriting (without letrec) is
discussed, where more examples can be found, and where nominal matching is
derived from the nominal unification algorithm. In this work also rewriting
using freshness contexts is investigated, and matching is defined using terms-
in-context . We only concentrate on the nominal matching part, since adding
constraints is not problematic.

###### Example 6.1

Consider the (lbeta)-rule, which is the version of (beta) used in call-by-need
calculi with sharing [43, 18, 19]. Note that in this case, the binding is
used, but not the property “recursive binding“.

$\displaystyle(\mathit{lbeta})\quad$ $\displaystyle(\lambda
x.e_{1})~{}e_{2}\to~{}{\tt letrec}~{}x.e_{2}~{}{\tt in}~{}e_{1}.$

An (lbeta) step, for example, reducing $((\lambda x.x)~{}(\lambda y.y))$ to
$({\tt letrec}~{}x=(\lambda y.y)~{}{\tt in}~{}x)$ is performed by representing
the target in $LRL$ and the beta-rule in the language LRLX, where
$e_{1},e_{2}$ are represented as variables $X_{1},X_{2}$, and then matching
$(\mathit{app}~{}(\lambda c.X_{1})~{}X_{2}){\ \unlhd\
}(\mathit{app}~{}(\lambda a.a)~{}(\lambda b.b))$, where $\mathit{app}$ is the
explicit representation of the binary application operator. This results in
$\sigma:=\\{X_{1}\mapsto c;X_{2}\mapsto\lambda b.b\\}$, and the reduction
result is the instance (using $\sigma$) of $({\tt letrec}~{}c.X_{2}~{}{\tt
in}~{}X_{1})$, which is $({\tt letrec}~{}c.(\lambda b.b)~{}{\tt in}~{}c)$.
Note that this form of reduction sequences permits $\alpha$-equivalence as
intermediate steps.

We derive a nominal letrec matching algorithm as a specialization of
LetrecUnify. We use non symmetric equations written $s{\ \unlhd\ }t$, where
$s$ is an $\mathit{LRLX}$-expression (also with permutations), and $t$ is
ground, i.e., does not contain free variables. It is easy to see that we can
also assume that $t$ does not contain permutations, since these can
immediately be simplified. We assume that the input is a set $s_{1}{\ \unlhd\
}t_{1},\ldots,s_{n}{\ \unlhd\ }t_{n}$ of match equations of expressions, where
for all $i$: $s_{i}$ may contain variables, and $t_{i}$ is ground. We omit
freshness constraints in the input, since these could be checked after the run
of the algorithm. Note that suspensions are not necessary in the solution, and
hence also no fixpoint equations.

${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{e{\ \unlhd\
}e\\}}{\Gamma}}$ ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{(f~{}s_{1}\ldots s_{n}){\ \unlhd\ }(f~{}s_{1}^{\prime}\ldots
s_{n}^{\prime})\\}}{\Gamma\cup\\{s_{1}{\ \unlhd\
}s_{1}^{\prime},\ldots,s_{n}{\ \unlhd\ }s_{n}^{\prime}\\}}}$
${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{\lambda a.s{\ \unlhd\
}\lambda a.t\\}}{\Gamma\cup\\{s{\ \unlhd\ }t\\}}}$

${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{\lambda a.s{\ \unlhd\
}\lambda b.t\\}\hskip 17.07164pta\\#t}{\Gamma\cup\\{s{\ \unlhd\
}(a~{}b){\cdot}t\\}}}\quad$ ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi{\cdot}X{\ \unlhd\ }e\\}}{\Gamma\cup\\{X{\ \unlhd\
}\pi^{-1}{\cdot}e\\}}}$ ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{X{\ \unlhd\ }e_{1},X{\ \unlhd\ }e_{2}\\}\hskip
17.07164pte_{1}\sim e_{2}}{\Gamma\cup\\{X{\ \unlhd\ }e_{1}\\}}}$

${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\left\\{\begin{array}[]{@{}ll@{}}&{\tt
letrec}~{}a_{1}.s_{1};\ldots;a_{n}.s_{n}~{}{\tt in}~{}r\\\ {\ \unlhd}&{\tt
letrec}~{}b_{1}.t_{1};\ldots;b_{n}.t_{n}~{}{\tt
in}~{}r^{\prime}\end{array}\right\\}\hskip 7.11317pta_{i}{\\#}({\tt
letrec}~{}b_{1}.t_{1};\ldots;b_{n}.t_{n}~{}{\tt in}~{}r^{\prime})\text{ for
}i=1,\ldots,n}{\mathop{|}\limits_{\\{\rho\\}}~{}\Gamma\cup\\{s_{1}{\ \unlhd\
}\pi{\cdot}t_{\rho(1)},\ldots,s_{n}{\ \unlhd\ }\pi{\cdot}t_{\rho(n)},r{\
\unlhd\ }\pi{\cdot}r^{\prime}\\}}}$
where $\rho$ is a permutation on $\\{1,\ldots,n\\}$, and $\pi$ is an (atom-)
permutation that extends $\\{b_{\rho(i)}\mapsto a_{i}\mid i=1,\ldots,n)\\}$
with $\mathit{dom}(\pi)\subseteq\\{a_{1},\ldots,a_{n},b_{1},\ldots,b_{n}\\}$

Figure 5: Rules of the matching algorithm LetrecMatch

###### Definition 6.2

The rules of the nondeterministic algorithm LetrecMatch w.r.t. the language
LRLX are in Fig. 5 and the corresponding failure rules are in Fig. 6. The
result is either a fail, or a substitution in the form $X_{1}{\ \unlhd\
}s_{1},\ldots,X_{n}{\ \unlhd\ }s_{n}$.

Note that the rules are designed such that permutations are moved to the rhs,
and conditions can be immediately evaluated.

${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\left\\{\begin{array}[]{@{}ll@{}}&{\tt
letrec}~{}a_{1}.s_{1};\ldots;a_{n}.s_{n}~{}{\tt in}~{}r\\\ {\ \unlhd}&{\tt
letrec}~{}b_{1}.t_{1};\ldots;b_{n}.t_{n}~{}{\tt
in}~{}r^{\prime}\end{array}\right\\}\hskip
7.11317pt\begin{array}[]{l}a_{i}\text{ is fresh in }({\tt
letrec}~{}b_{1}.t_{1};\ldots;b_{n}.t_{n}~{}{\tt in}~{}r^{\prime})\\\ \text{
for some }i\in\\{1,\ldots,n\\}\end{array}}{\bot}}$
${\displaystyle\frac{s{\ \unlhd\ }t\in\Gamma,\text{ and }s\text{ is not a
suspension, but }\mathit{tops}(s)\not=\mathit{tops}(t)}{\bot}}$
${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{\lambda a.s{\ \unlhd\
}\lambda b.t\\}\hskip 17.07164pta\text{ is fresh in }t)}{\bot}}\quad$
${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{X{\ \unlhd\ }e_{1},X{\
\unlhd\ }e_{2}\\}\hskip 17.07164pte_{1}\not\sim e_{2}}{\bot}}$

Figure 6: Failure rules of the matching algorithm LetrecMatch

The $\alpha$-equivalence test $e_{1}\sim e_{2}$ may for example be performed
as a subroutine call to this (nondeterministic) matching procedure in the
collecting version, i.e., the test succeeds if there is a nondeterministic
execution with success as result.

###### Example 6.3

We illustrate the failure rule that signals fail, if $\lambda a.s{\ \unlhd\
}\lambda b.t$ is a match-equations and $a$ is fresh in $t$. In the case
$\lambda c.c{\ \unlhd\ }\lambda b.a$, the failure rule signals “fail”. We also
could proceed and replace it using the lambda-rule by $c{\ \unlhd\
}(c~{}b){\cdot}a$, which immediately reduces to $c{\ \unlhd\ }a$, which is
fail sind the top symbols are different.

Standard arguments show:

###### Theorem 6.4

LetrecMatch is sound and complete for nominal letrec matching. It decides
nominal letrec matching in nondeterministic polynomial time. Its collecting
version returns a finite complete set of an at most exponential number of
matching substitutions, which are of at most polynomial size.

###### Theorem 6.5

Nominal letrec matching is NP-complete.

###### Proof 6.6

The problem is in NP, which follows from Theorem 6.4. It is also NP-hard,
which follows from Theorem 5.1.

###  6.1 Remarks on letrec-matching with DAGs

A more general situation for nominal letrec matching occurs, when the matching
equations $\Gamma_{0}$ are compressed using a DAG. We construct a practically
more efficient algorithm LetrecDagMatch from LetrecUnify as follows. First we
generate $\Gamma_{1}$ from $\Gamma_{0}$, which only contains flattened
expressions by encoding the DAG-nodes as variables $X$ together with an
equation $X\doteq r$ for the subexpression, which results in a unification
equation. This representation is no longer a letrec-matching problem, since
there may be variables in the left and right-hand side of equations. However,
it has structural properties inherited from the sharing. An expression is said
$\Gamma_{0}$-ground, if it does not reference variables from $\Gamma_{0}$
(also via equations). In order to avoid suspension on the rhs (i.e. to have
nicer results), the decomposition rule for $\lambda$-expressions with
different binder names is modified as follows :

${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup(\lambda a.s\doteq\lambda
b.t\\},\nabla}{\Gamma\cup\\{s\doteq(a~{}b){\cdot}t\\},\nabla\cup\\{a{{\\#}}t\\}}}$
$\lambda b.t$ is $\Gamma_{0}$-ground

The extra conditions $a{{\\#}}t$ and $\Gamma_{0}$-ground can be tested in
polynomial time. The equations $\Gamma_{1}$ are processed applying LetrecUnify
(with the mentioned modification) with the guidance that the right-hand sides
of match-equations are also right-hand sides of equations in the decomposition
rules. The resulting matching substitutions can be interpreted as the
instantiations into the variables of $\Gamma_{0}$. Since $\Gamma_{0}$ is a
matching problem, the result will be free of fixpoint equations, and there
will be no freshness constraints in the solution.

This construction would permits better performance than simply treating the
DAG-matching problem as a unification problem.

##  7 Graph-isomorphism-hardness of nominal letrec matching and unification
without garbage

We will show in this section that Nominal Letrec Matching is at least as hard
as Graph-Isomorphism. Graph-Isomorphism is known to have complexity between
$\mathit{PTIME}$ and $\mathit{NP}$. There are arguments that it is strictly
weaker than the class of NP-complete problems [44]. There is also a claim that
it is quasi-polynomial [45], which means that it requires less than
exponential time. The general conjecture is that Graph-Isomorphism is properly
between $\mathit{PTIME}$ and $\mathit{NP}$.

First we clarify the notion of garbage, which is a notion from a programming
language point of view.

###### Definition 7.1

We say that an expression $t$ contains garbage, iff there is a subexpression
$({\tt letrec}~{}\mathit{env}$ ${\tt in}~{}r)$, and the environment
$\mathit{env}$ can be split into two environments
$\mathit{env}=\mathit{env}_{g};\mathit{env}_{ng}$, such that
$\mathit{env}_{g}$ (the garbage) is not empty, and the atoms from
$\mathit{LA}(\mathit{env}_{g})$ occur neither free in $\mathit{env}_{ng}$ nor
in $r$. Otherwise, the expression $t$ is free of garbage (or garbage-free).

An example illustrating the notions is ${\tt letrec}~{}a.b;b.c~{}{\tt
in}~{}b$, where $a,b,c$ are (different) atoms. The binding $a.b$ is not used
in the in-expression $b$, hence it can be classified as garbage, whereas the
binding $b.c$ is used. In a programming language, the garbage collector would
remove this binding and replace the expression by ${\tt letrec}~{}b.c~{}{\tt
in}~{}b$.

Since $\alpha$-equivalence of $\mathit{LRL}$-expressions is Graph-Isomorphism-
complete [38], but $\alpha$-equivalence of garbage-free
$\mathit{LRL}$-expressions is polynomial, it is useful to look for
improvements of unification and matching for garbage-free expressions.

We will show that even very restricted nominal letrec matching problems are
Graph-Isomorphism complete, which makes it very unlikely that there is a
polynomial algorithm.

###### Theorem 7.2

Nominal letrec matching with one occurrence of a single variable and a
garbage-free target expression is Graph-Isomorphism-hard.

###### Proof 7.3

Let $G_{1},G_{2}$ be two regular graphs with degree $\geq 1$. Let $t$ be
$({\tt letrec}~{}\mathit{env}_{G_{1}}~{}{\tt
in}~{}g~{}b_{1}~{}b_{1}^{\prime}\ldots b_{m}~{}b_{m}^{\prime})$ the encoding
of an arbitrary graph $G_{1}$ where $\mathit{env}_{G_{1}}$ is the encoding as
in the proof of Theorem 5.1: nodes are encoded as $a_{1},\ldots,a_{n}$,i.e.,
the bindings in the environment are
$a_{1}.(\mathit{node}~{}a_{1}),\ldots,a_{n}1.(\mathit{node}~{}a_{n})$, and the
edges are encoded as follows: The $i$-th edge $(a_{k}~{}a_{l})$ is encoded as
$b_{i}.(\mathit{edge}~{}a_{k}~{}a_{l}),b_{i}^{\prime}.(\mathit{edge}~{}a_{l}~{}a_{k})$.
Then $t$ is free of garbage, since the graph $G_{1}$ is regular. Let the
environment $\mathit{env}_{G_{2}}$ be the encoding of $G_{2}$ in $s=({\tt
letrec}~{}\mathit{env}_{G_{2}}~{}{\tt in}~{}X)$, where $\mathit{env}_{G_{2}}$
is constructed in the same way from the graph $G_{2}$. Then $s$ matches $t$
iff the graphs $G_{1},G_{2}$ are isomorphic. If there is an isomorphism of
$G_{1}$ and $G_{2}$, then it is easy to see that this bijection leads to an
equivalence of the environments, and we can instantiate $X$ with
$(g~{}b_{1}~{}b_{1}^{\prime}\ldots b_{m}~{}b_{m}^{\prime})$. Since the graph-
isomorphism problem for regular graphs of degree $\geq 1$ is GI-hard [46], we
have shown GI-hardness.

##  8 On fixpoints and garbage

We will show in this section that $\mathit{LRLX}$-expressions without garbage
only have trivial fix-pointing permutations. Looking at Example 3.2, the
$\alpha$-equivalence $(a~{}b)\cdot({\tt letrec}~{}c.a;d.b~{}{\tt
in}~{}\mathit{True})$ $\sim$ $({\tt letrec}~{}\allowbreak c.a;d.b~{}{\tt
in}~{}\mathit{True})$ holds, where $\mathit{dom}((a~{}b))\cap\mathit{FA}({\tt
letrec}~{}c.a;d.b~{}{\tt in}~{}\mathit{True})=\\{a,b\\}\not=\emptyset$.
However, we see that the expressions is equivalent (in a programming language
semantics) to $\mathit{True}$, and that the whole environment in this example
is garbage, since no binding is referenced from the in-expression (see Def.
7.1).

As a helpful information, we write the $\alpha$-equivalence-rule for letrec-
expressions in the ground language $\mathit{LRL}$ as an extension of the rule
for lambda-abstractions.

${\displaystyle\frac{r\sim\pi{\cdot}r^{\prime},\,s_{i}\sim\pi{\cdot}t_{\rho(i)},\,i=1,\ldots,n,\hskip
11.38109ptM{{\\#}}({\tt letrec}~{}b_{1}.t_{1};\ldots;b_{n}.t_{n}~{}{\tt
in}~{}r^{\prime})}{{\tt letrec}~{}a_{1}.s_{1};\ldots;a_{n}.s_{n}~{}{\tt
in}~{}r\sim{\tt letrec}~{}b_{1}.t_{1};\ldots;b_{n}.t_{n}~{}{\tt
in}~{}r^{\prime}}}$

where $\rho$ is a permutation on $\\{1,\ldots,n\\}$,
$M=\\{a_{1},\ldots,a_{n}\\}\setminus\\{b_{1},\ldots,b_{n}\\}$, and $\pi$ is an
atom-permutation-extension of the bijective function $\\{b_{i}\mapsto
a_{\rho(i)},i=1,\ldots,n\\}$ such that
$\mathit{dom}(\pi)\subseteq(\\{b_{1},\ldots,b_{n}\\}\cup\\{a_{1},\ldots,a_{n}\\})$.

Note that $\alpha$-equivalence of $s,t$ means structural equivalence of $s,t$
as trees, and a justification always comes with a bijective relation between
the positions of $s,t$ where only the names of atoms at nodes may be
different.

A further example of garbage is $({\tt letrec}~{}a.0;b.1~{}{\tt
in}~{}(f~{}b))$, where $a$ is unused, but $b$ is used in the right hand side.
In this case $a.0$ is garbage. Another example is $e:=({\tt
letrec}~{}a.d;b.1;c.d~{}{\tt in}~{}(f~{}b))$, which is an example with a free
atom $d$, and the garbage consists of two bindings, $\\{a.d;c.d\\}$. It is
$\alpha$-equivalent to $({\tt letrec}~{}a^{\prime}.d;b.1;c^{\prime}.d~{}{\tt
in}~{}(f~{}b))=:e^{\prime}$. Note that in this case, there are two different
permutations (bijective functions) mapping $e^{\prime}$ to (the
$\alpha$-equivalent) $e$: $\\{a^{\prime}\mapsto a;c^{\prime}\mapsto c\\}$ and
$\\{a^{\prime}\mapsto c;c^{\prime}\mapsto a\\}$.

The next lemma shows that this situation is only possible if the expressions
contain garbage.

###### Lemma 8.1

If $s\sim t$, and $s$ is free of garbage, then $\alpha$-equivalence provides a
unique correspondence of the positions of $s$ and $t$.

###### Proof 8.2

The proof is by induction on the structure and size of expressions. For the
structure, the only nontrivial case is letrec: Let $s=({\tt
letrec}~{}a_{1}.e_{1},\ldots,a_{n}.e_{n}~{}{\tt in}~{}e)$ $\sim$ $({\tt
letrec}~{}b_{1}.f_{1},\ldots,b_{n}.f_{n}~{}{\tt in}~{}f)=t$. Note that due to
syntactic equality all permutations of the environments are also to be
considered. Then there is bijective mapping $\varphi$, with
$\varphi(b_{i})=a_{\rho(i)},i=1,\ldots,n$, where $\rho$ is a permutation on
$\\{1,\ldots,n\\}$, and such that
$e_{i}\sim\varphi(f_{\rho(i)}),i=1,\ldots,n$, $e\sim\varphi(f)$, and
$(\\{a_{1},\ldots,a_{n}\\}\setminus\\{b_{1},\ldots,b_{n}\\})\\#t$ holds. Let
$\overline{\varphi}$ be the atom-permutation that extends $\varphi$, mapping
$(\\{a_{1},\ldots,a_{n}\\}\setminus\\{b_{1},\ldots,b_{n}\\})$ to
$(\\{b_{1},\ldots,b_{n}\\}\setminus\\{a_{1},\ldots,a_{n}\\})$.

The induction hypothesis implies a unique position correspondence of $e$ and
$f$, since $e\sim\overline{\varphi}(f)$. This implies that the bindings for
$\\{a_{1},\ldots,a_{n}\\}\cap\mathit{FA}(e)$ have a unique correspondence to
the bindings in $t$. This is continued by exhaustively following free
occurrences of atoms $a_{i}$ in the right hand sides of the top bindings in
$s$. Since there is no garbage in $s$, all bindings can be reached by this
process, hence we have uniqueness of the correspondence of positions.

###### Proposition 8.3

Let $e$ be an expression that does not have garbage, and let $\pi$ be a
permutation. Then $\pi{\cdot}e\sim e$ implies
$\mathit{dom}(\pi)\cap\mathit{FA}(e)=\emptyset$.

###### Proof 8.4

The proof is by induction on the size of the expression.

  * •

If $e$ is an atom, then this is trivial.

  * •

If $e=f~{}e_{1}\ldots.e_{n}$, then no $e_{i}$ contains garbage, and
$\pi{\cdot}e_{i}\sim e_{i}$ implies
$\mathit{dom}(\pi)\cap\mathit{FA}(e_{i})=\emptyset$, hence also
$\mathit{dom}(\pi)\cap\mathit{FA}(e)=\emptyset$.

  * •

If $e=\lambda a.e^{\prime}$, then there are two cases:

    1. 1.

$\pi(a)=a$. Then $\pi{\cdot}e^{\prime}\sim e^{\prime}$, and we can apply the
induction hypothesis.

    2. 2.

$\pi(a)=b\not=a$. Then $(a~{}b){\cdot}\pi$ fixes $e^{\prime}$, and
$b\\#e^{\prime}$. The induction hypothesis implies
$\mathit{dom}((a~{}b){\cdot}\pi)\cap\mathit{FA}(e^{\prime})=\emptyset$. We
have
$\mathit{dom}(\pi)\subseteq\mathit{dom}((a~{}b){\cdot}\pi))\cup\\{a,b\\}$,
hence $\mathit{dom}(\pi)\cap\mathit{FA}(\lambda a.e^{\prime})=\emptyset$.

  * •

First a simple case with one binding in the environment: $t=({\tt
letrec}~{}a_{1}.e_{1}~{}{\tt in}~{}e)$, $\pi{\cdot}t\sim t$. If
$\pi(a_{1})=a_{1}$, then $\pi{\cdot}(e,e_{1})\sim(e,e_{1})$, and the induction
hypothesis implies $\mathit{dom}(\pi)\cap\mathit{FA}(e,e_{1})=\emptyset$,
which in turn implies $\mathit{dom}(\pi)\cap\mathit{FA}(t)=\emptyset$.

If $\pi(a_{1})=b\not=a_{1}$, then $b\\#(e,e_{1})$ and for
$\pi^{\prime}:=(a_{1}~{}b){\cdot}\pi$, it holds
$\pi^{\prime}{\cdot}(e,e_{1})\sim(e,e_{1})$, and so
$\mathit{dom}((a_{1}~{}b){\cdot}\pi)\cap\mathit{FA}(e,e_{1})=\emptyset$. since
$\mathit{dom}(\pi)\subseteq\mathit{dom}((a_{1}~{}b){\cdot}\pi)\cup\\{a_{1},b\\}$,
we obtain $\mathit{dom}(\pi)\cap t=\emptyset$. In the case of one binding, it
is irrelevant whether the binding is garbage or not.

  * •

Let $t=({\tt letrec}~{}a_{1}.e_{1};\ldots;a_{n}.e_{n}~{}{\tt in}~{}e)$, and
$t$ is a fixpoint of $\pi$, i.e. $\pi(t)\sim t$. Note that no part of the
environment is garbage. The permutation $\pi$ can be split into
$\pi=\pi_{1}{\cdot}\pi_{2}$, where
$\mathit{dom}(\pi_{1})\subseteq\mathit{FA}(t)$ and
$\mathit{dom}(\pi_{2})\cap\mathit{FA}(t)=\emptyset$. From $t\sim\pi{\cdot}t$
and Lemma 8.1 we obtain that there is a unique permutation $\rho$ on
$\\{1,\ldots,n\\}$, such that there is an injective mapping
$\varphi:\pi(a_{1})\mapsto a_{\rho(1)},\ldots,\pi(a_{n})\mapsto a_{\rho(n)}$,
and $e\sim\varphi\pi(e)$, $e_{\rho(i)}\sim\varphi\pi(e_{i})$. Then
$\alpha$-equivalence implies that $\varphi\pi$ can be extended to a atom-
permutation $\overline{\varphi}\pi$ by mapping the atoms in
$\\{a_{1},\ldots,a_{n}\\}\setminus\\{\pi(a_{1}),\ldots,\pi(a_{n})\\}$
bijectively to
$\\{\pi(a_{1}),\ldots,\pi(a_{n})\\}\setminus\\{a_{1},\ldots,a_{n}\\}$. By the
freshness constraints for $\alpha$-equivalences of letrec-expressions,
$\overline{\varphi}\pi(e)=\varphi\pi(e)$ and
$\overline{\varphi}\pi(e_{i})=\varphi\pi(e_{i})$ which in turn implies that
$e\sim\overline{\varphi}\pi(e)$ and $e_{i}\sim\overline{\varphi}\pi(_{i}e)$,
and we can apply the induction hypothesis.

This shows that $\mathit{FA}(e)\setminus\\{a_{1},\ldots,a_{n}\\}$ are not
moved by $\overline{\varphi}\pi$, and the same for all $e_{i}$, hence this
also holds for $t$.

###### Corollary 8.5

Let $e$ be an expression that does not have garbage, and let $\pi$ be a
permutation. Then $\pi{\cdot}e\sim e$ is equivalent to
$\mathit{dom}(\pi)\cap\mathit{FA}(e)=\emptyset$.

###### Proof 8.6

This follows from Proposition 8.3. The other direction is easy.

The proof also shows a slightly more general statement:

###### Corollary 8.7

Let $e$ be an expression such that in all environments with at least two
bindings there are no garbage bindings, and let $\pi$ be a permutation. Then
$\pi{\cdot}e\sim e$ is equivalent to
$\mathit{dom}(\pi)\cap\mathit{FA}(e)=\emptyset$.

In case that the input does not represent garbage-parts, and the semantics is
defined such that only ground garbage free expressions are permitted, the set
of rules in the case without atom-variables can be optimized as follows:
(ElimFP) can be omitted and instead of (FPS) there are two rules:

(FPS2) ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{X\doteq\pi{\cdot}X\\},\nabla}{\Gamma,\nabla\cup\\{a{\\#}X\mid
a\in\mathit{dom}(\pi)\\}}}$,

(ElimX) ${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{X\doteq
e\\},\theta}{\Gamma,\theta\cup\\{X\mapsto e\\}}}$,  if
$X\not\in\mathit{Var}(\Gamma)$, and $e$ is not a suspension of $X$.

###### Example 8.8

It cannot be expected that the letrec-decomposition rule (7) can be turned
into a deterministic rule, and to obtain a unitary nominal unification, under
the restriction that input expressions are garbage-free, and also
instantiations are garbage-free. Consider the equation:

$({\tt letrec}~{}a_{1}.e_{1};a_{2}.e_{2}~{}{\tt
in}~{}((a_{1},a_{2}),X))\doteq({\tt letrec}~{}b_{1}.f_{1};b_{2}.f_{2}~{}{\tt
in}~{}(X’,(b_{1},b_{2}))).$

Then the in-expressions do not enforce a unique correspondence between the
bindings of the left and right-hand bindings. An example also follows from the
proof of Theorem 7.2, which shows that even nominal matching may have several
incomparable solutions for garbage-free expressions.

##  9 Nominal unification with letrec and atom-variables

In this section we extend the unification algorithm to the language
$\mathit{LRLXA}$, which is an extension of $\mathit{LRLX}$ with atom
variables. Atom-variables increase the expressive power of a term language
with atoms alone. If in an application example it is known that in a pair
$(x_{1},x_{2})$ the expressions $x_{1},x_{2}$ can only be atoms, but
$x_{1}=x_{2}$ as well as $x_{1}\not=x_{2}$ is possible, then two different
unification problems have to be formulated. If atom variables are possible,
then the notation $(A_{1},A_{2})$ covers both possibilities.

It is known that the nominal unification problem with atom-variables but
without letrec is NP-complete [27]. An algorithm and corresponding rules and
discussions can be found in [27]. An implication is NP-hardness of nominal
unification with atom variables and letrec.

###  9.1 Extension with atom-variables

As an extension of $\mathit{LRLX}$, we define the language$\mathit{LRLXA}$ as
follows: Let $A$ denote atom variables, $V$ denote atom variables or atoms,
$W$ denote suspensions of atoms or atom variables, $X$ denotes expression
variables, $\pi$ a permutation, and $e$ an expression. The syntax of the
language $\mathit{LRLXA}$ is

$\begin{array}[]{lcl}V&::=&a\mid A\\\ W&::=&\pi\cdot V\\\
\pi&::=&\emptyset\mid(W~{}W)\mid\pi{\circ}\pi\\\ e&::=&\pi{\cdot}X\mid
W\mid\lambda W.e\mid(f~{}e_{1}~{}\ldots e_{\mathit{ar}(f)})~{}|~{}({\tt
letrec}~{}W_{1}.e_{1};\ldots;W_{n}.e_{n}~{}{\tt in}~{}e)\end{array}$

Let $\mathit{Var}(e)$ be the set of atom or expression variables occurring in
$e$, and let $\mathit{AtVar}(e)$ be the set of atom variables occurring in
$e$. Similarly for sequences of expressions or permutations.
The expression $\pi{\cdot}e$ for a non-variable expression $e$ means an
operation, which is performed by shifting $\pi$ down in the expression, using
the simplifications $\pi_{1}{\cdot}(\pi_{2}{\cdot}X)$ $\to$
$(\pi_{1}\circ\pi_{2}){\cdot}X$, where only expressions $\pi{\cdot}X$ and
$\pi{\cdot}V$ remain, where the latter are called suspensions and where
$\pi{\cdot}V$ is abbreviated as $W$.

###### Remark 9.1

An alert for the reader: In this section the use of atom-variables induces
generalizations and changes in the $\mathit{LRLXA}$-formulation of problems:
binders may now be suspensions of atom-variables, and also “nested”
permutation representations are permitted, which is due to atom variables,
since in general, this permutation representation cannot be simplified.
Several simple facts and intuitions that are used for $\mathit{LRLX}$ no
longer hold.

A freshness constraint in our unification algorithm is of the form $V{{\\#}}e$
where $e$ is an $\mathit{LRLXA}$-expression. The justification for the
slightly more complex form as usual ($a{\\#}X$) is that atom variables prevent
a simplification to this form. The notation $\pi^{-1}$ is defined as the
reversed list of swappings of $\pi$, where the single (perhaps complex)
swappings are not modified. A semantical justification for this inverse is by
checking the ground instantiations.

We also view $\pi\cdot V{\\#}e$ as identical to the constraint
$V{\\#}\pi^{-1}\cdot e$.

Naively applying ground substitutions may lead to syntactically invalid ground
expressions, since instantiation may make binding atoms in letrecs equal,
which is illegal. This will be prevented by freshness constraints.

###### Example 9.2

The equation

$(\mathit{app}~{}({\tt letrec}~{}A.a,B.a~{}{\tt
in}~{}B)~{}A)\doteq(\mathit{app}~{}({\tt letrec}~{}A.a,B.a~{}{\tt
in}~{}B)~{}B)$

enforces that $A,B$ are instantiated with the same atom, which contradicts the
syntactic assumption on distinct atoms for the binding names in letrec-
expressions. This will be dealt with by adding the freshness constraint
$A\\#B$. However,

$(\mathit{app}~{}({\tt letrec}~{}A.a,C.a~{}{\tt
in}~{}C)~{}A)\doteq(\mathit{app}~{}({\tt letrec}~{}A.a,D.a~{}{\tt
in}~{}D)~{}B)$

is solvable. Note that the additional freshness constraints are $A\\#C,A\\#D$.

###### Remark 9.3

We circumvent the problem of illegal ground instances by adding for every
letrec-expression in the input of the unification algorithm sufficiently many
freshness constraint that prevent these illegal expressions (see below). It is
sufficient to prevent equal binding names in every single letrec-environment.

###### Definition 9.4

An $\mathit{LRLXA}$-unification problem is a pair $(\Gamma,\nabla)$, where
$\Gamma$ is a set of equations $s\doteq t$, and $\nabla$ is a set of freshness
constraints $V\\#e$. In addition, for every letrec-subexpression ${\tt
letrec}~{}W_{1}.e_{1}$, $\ldots,$ $W_{m}.e_{m}~{}{\tt in}~{}e$, which occurs
in $\Gamma$ or $\nabla$, the set $\nabla$ must also contain the freshness
constraint $W_{i}{\\#}W_{j}$ for all $i,j=1,\ldots,m$ with $i\not=j$.

A (ground) solution of $(\Gamma,\nabla)$ is a substitution $\rho$ (mapping
variables in $\mathit{Var}(\Gamma,\nabla)$ to ground expressions), such that
$s\rho\sim t\rho$ for all equations $s\doteq t$ in $\Gamma$, and for all
$V{{{\\#}}}e\in\nabla$: $V\rho\\#(e\rho)$ holds.

The decision problem is whether there is a solution for a given
$(\Gamma,\nabla)$.

###### Proposition 9.5

The $\mathit{LRLXA}$-unification problem is in NP, and hence NP-complete.

###### Proof 9.6

The argument is that every ground instantiation of an atom variable is an
atom, which can be guessed and checked in polynomial time: guess the images of
atom variables under a ground solution $\rho$ in the set of atoms in the
current state, or in an arbitrary set of fresh atom variables of cardinality
at most the number of different atom variables in the input. Then instantiate
accordingly thereby removing all atom-variables. The resulting problem can be
decided (and solved) by an NP-algorithm as shown in this paper (Theorem 5.3).

###### Remark 9.7

Note that the equation $A=\pi{\cdot}B$ for atom variables $A,B$ can be encoded
as the freshness constraint $A\\#\lambda\pi{\cdot}B.A$. In the following we
may use equations $V_{1}=_{\\#}\pi{\cdot}V_{2}$ as a more readable version of
$V_{1}\\#\lambda\pi{\cdot}V_{2}.V_{1}$.

$(1)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{e\doteq
e\\}}{\Gamma}}$ (2)$~{}{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}V_{1}\doteq\pi_{2}{\cdot}V_{2}\\},\nabla,\theta}{\Gamma,\nabla\cup\\{V_{1}=_{\\#}\pi_{1}^{-1}\pi_{2}{\cdot}V_{2}\\},\theta}}$

$(3a)~{}{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}X\doteq\pi_{2}{\cdot}Y\\},\nabla,\theta\qquad
X\not=Y}{\Gamma[\pi_{1}^{-1}\pi_{2}{\cdot}Y/X],\nabla[\pi_{1}^{-1}\pi_{2}{\cdot}Y/X],\theta\cup\\{X\mapsto\pi_{1}^{-1}\pi_{2}Y\\}}}$

$(3b)~{}{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}X\doteq\pi_{2}{\cdot}V\\},\nabla,\theta}{\Gamma[\pi_{1}^{-1}\pi_{2}{\cdot}V/X],\nabla[\pi_{1}^{-1}\pi_{2}{\cdot}V/X],\theta\cup\\{X\mapsto\pi_{1}^{-1}\pi_{2}V\\}}}$

$(4)~{}{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{(f~{}(\pi_{1}{\cdot}X_{1})\ldots(\pi_{n}{\cdot}X_{n}))\doteq(f~{}(\pi^{\prime}_{1}{\cdot}X^{\prime}_{1})\ldots(\pi^{\prime}_{n}{\cdot}X^{\prime}_{n}))\\}}{\Gamma\cup\\{\pi_{1}{\cdot}X_{1}\doteq\pi^{\prime}_{1}{\cdot}X_{1}^{\prime},\ldots,\pi_{n}{\cdot}X_{n}\doteq\pi^{\prime}_{n}{\cdot}X^{\prime}_{n}\\}}}$

$(5)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{(\lambda
W.\pi_{1}{\cdot}X_{1}\doteq\lambda
W.\pi_{2}{\cdot}X_{2}\\}}{\Gamma\cup\\{\pi_{1}{\cdot}X_{1}\doteq\pi_{2}{\cdot}X_{2}\\}}}$

$(6)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup(\lambda
W_{1}.\pi_{1}{\cdot}X_{1}\doteq\lambda
W_{2}.\pi_{2}{\cdot}X_{2}\\},\nabla}{\Gamma\cup\\{\pi_{1}{\cdot}X_{1}\doteq(W_{1}~{}W_{2}){\cdot}\pi_{2}{\cdot}X_{2}\\},\nabla\cup\\{W_{1}{{\\#}}(\lambda
W_{2}.\pi_{2}{\cdot}X_{2})\\}}}$

$(7)~{}{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\left\\{\begin{array}[]{l}{\tt
letrec}~{}W_{1}.\pi_{1}{\cdot}X_{1};\ldots;W_{n}.\pi_{n}{\cdot}X_{n}~{}{\tt
in}~{}\pi{\cdot}Y\doteq\\\ {\tt
letrec}~{}W^{\prime}_{1}.\pi^{\prime}_{1}{\cdot}X^{\prime}_{1};\ldots;W^{\prime}_{n}.\pi^{\prime}_{n}{\cdot}X^{\prime}_{n}~{}{\tt
in}~{}\pi^{\prime}{\cdot}Y^{\prime}\end{array}\right\\},\nabla}{\begin{array}[]{l}{\begin{array}[]{ll}{\begin{array}[]{c}\left|\begin{array}[]{c}{}\hfil\\\
{}\hfil\\\ {}\hfil\\\ \end{array}\right.\\\
{\\{\rho\\}}\end{array}}&\left(\begin{array}[]{l}\Gamma\,\mathop{\cup}\,\left\\{\begin{array}[]{l}~{}\mathrm{decompose}(n\\!+\\!1,\lambda
W_{1}\ldots\lambda
W_{n}.(\pi_{1}{\cdot}X_{1},\ldots,\pi_{n}{\cdot}X_{n},\pi{\cdot}Y)\\\ \hskip
19.91684pt\doteq\lambda W^{\prime}_{\rho(1)}.\ldots\lambda
W^{\prime}_{\rho(n)}.(\pi^{\prime}_{\rho(1)}{\cdot}X^{\prime}_{\rho(1)},\ldots,\pi^{\prime}_{\rho(n)}{\cdot}X^{\prime}_{\rho(n)},\pi^{\prime}{\cdot}Y^{\prime}))\end{array}\right\\},\\\
{}\\\\[-14.22636pt]
\nabla\cup\left\\{\begin{array}[]{l}~{}\mathrm{decompfresh}(n\\!+\\!1,\lambda
W_{1}\ldots\lambda
W_{n}.(\pi_{1}{\cdot}X_{1},\ldots,\pi_{n}{\cdot}X_{n},\pi{\cdot}Y)\\\ \hskip
19.91684pt\doteq\lambda W^{\prime}_{\rho(1)}.\ldots\lambda
W^{\prime}_{\rho(n)}.(\pi^{\prime}_{\rho(1)}{\cdot}X^{\prime}_{\rho(1)},\ldots,\pi^{\prime}_{\rho(n)}{\cdot}X^{\prime}_{\rho(n)},\pi^{\prime}{\cdot}Y^{\prime}))\end{array}\right\\}\end{array}\right)\end{array}{}}\\\\[5.69054pt]
\mbox{where $\rho$ is a permutation on $\\{1,\ldots,n\\}$ and
$\mathrm{decompose}(n,.)$ is the equation part of $n$-fold }{}\\\ \mbox{
application of rules (4), (5) or (6) and $\mathrm{decomposefresh}(n,.)$ is the
freshness constraint}{}\\\ \mbox{ part of the $n$-fold application of rules
(4), (5) or (6); (in both cases after flattening).}\\\ \end{array}}}$

Figure 7: Standard and decomposition rules with atom variables of
LetrecUnifyAV.

(MMS), (FPS), (ElimFP) and (Output) are almost the same as the ones in Fig 3.

(MMS) ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}X\doteq e_{1},\pi_{2}{\cdot}X\doteq
e_{2}\\},\nabla}{\Gamma\cup\\{\pi_{1}{\cdot}X\doteq
e_{1}\\}\cup\Gamma^{\prime},\nabla\cup\nabla^{\prime}}}$,  if $e_{1},e_{2}$
are not suspensions, where $\Gamma^{\prime}$ is the set of equations generated
by decomposing $\pi_{1}^{-1}{\cdot}e_{1}\doteq\pi_{2}^{-1}{\cdot}e_{2}$ using
(1)–(7), and where $\nabla^{\prime}$ is the corresponding resulting set of
freshness constraints.

(FPS) ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}X\doteq\pi^{\prime}_{1}{\cdot}X,\ldots,\pi_{n}{\cdot}X\doteq\pi^{\prime}_{n}{\cdot}X,\pi{\cdot}X\doteq
e\\},\theta}{\Gamma\cup\\{\pi_{1}\pi^{-1}{\cdot}e\doteq\pi^{\prime}_{1}\pi^{-1}{\cdot}e,\ldots,\pi_{n}\pi^{-1}{\cdot}e\doteq\pi^{\prime}_{n}\pi^{-1}{\cdot}e\\},\theta\cup\\{X\mapsto\pi^{-1}{\cdot}e\\}}}$,

If $X\not\in\mathit{Var}(\Gamma,e)$, and $e$ is not a suspension, and (Cycle)
(see Fig.4) is not applicable.

(ElimFP) ${\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}X\doteq\pi^{\prime}_{1}{\cdot}X,\ldots,\pi_{n}{\cdot}X\doteq\pi^{\prime}_{n}{\cdot}X,\pi{\cdot}X\doteq\pi^{\prime}{\cdot}X\\},\theta}{\Gamma\cup\\{\pi_{1}{\cdot}X\doteq\pi^{\prime}_{1}{\cdot}X,\ldots,\pi_{n}{\cdot}X\doteq\pi^{\prime}_{n}{\cdot}X\\},\theta}}$,

If
$\pi^{-1}\pi^{\prime}\in\langle\pi_{1}^{-1}\pi_{1},\ldots,\pi_{n}^{-1}\pi_{n}\rangle,$

and  $\pi_{i},\pi_{i}^{\prime},\pi,\pi^{\prime}$ are ground, i.e. do not
contain atom variables.

(Output) ${\displaystyle\frac{\Gamma,\nabla,\theta}{(\theta,\nabla,\Gamma)}}$
if $\Gamma$ only consists of fixpoint-equations.

(ElimA)
${\displaystyle\frac{\Gamma,\nabla,\theta}{\begin{array}[]{ll}{\begin{array}[]{c}{\left|\begin{array}[]{c}\end{array}\right.}\\\
{\left\\{\begin{array}[]{ll}\text{atoms in }\Gamma,\nabla,\theta\\\ \text{and
a fresh atom
}a\end{array}\right\\}}\end{array}}&\Gamma[a/A],\nabla[a/A],\theta\cup\\{A\mapsto
a\\}\end{array}}}$

Figure 8: Main rules of LetrecUnifyAV

(Clash) ${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{s\doteq
t\\},\nabla,\theta~{}~{}~{}tops(s)\not=\mathit{tops}(t)\mbox{ and $s$ and $t$
are not suspensions}}{\bot}}$

(ClashA) ${\displaystyle\frac{\\{s\doteq t\\}\mbox{ is in }\Gamma,\mbox{ and
}~{}~{}\begin{array}[]{l}s\text{ is a suspension of an atom or atom
variable}\\\ \mbox{ and $\mathit{tops}(t)$ is a function symbol, $\lambda$ or
letrec }\end{array}}{\bot}}$

(Clashab) ${\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{a\doteq
b\\},\nabla,\theta~{}\hskip 14.22636pta\not=b}{\bot}}$

(Cycle) ${\displaystyle\frac{\begin{array}[]{l}\text{If
}\pi_{1}{\cdot}X_{1}\doteq s_{1},\ldots,\pi_{n}{\cdot}X_{n}\doteq s_{n}\text{
in }\Gamma\text{ where }s_{i}\text{ are not suspensions}\\\ \text{ and
}X_{i+1}\text{ occurs in }s_{i}\text{ for }i=1,\ldots,n-1\text{ and
}X_{1}\text{ occurs in }s_{n}.\end{array}}{\bot}}$

(FailF) ${\displaystyle\frac{a{{\\#}}a\in\nabla}{\bot}}$ (FailFS)
${\displaystyle\frac{a{{\\#}}X\in\nabla~{}~{}~{}\text{ and }a\text{ occurs
free in }(X\theta)}{\bot}}$

Figure 9: Failure Rules of LetrecUnifyAV

###  9.2 Rules of the algorithm LetrecUnifyAV

Now we describe the nominal unification algorithm LetrecUnifyAV for
$\mathit{LRLXA}$. It will extend the algorithm LetrecUnify by a treatment of
atom variables that extend the expressibility. It has flexible rules, such
that a strategy can be added to control the nondeterminism and such that it is
an improvement over a brute-force guessing-algorithm that first guesses all
atom instances of atom-variables and then uses Algorithm LetrecUnify (see
Algorithm 9.16 for such an improvement). The simple idea is to only make these
guesses if a certain space-bound of the whole state is exceeded and then use
the guesses and further rules to shrink the size of the problem
representation. Note that permutations with atom variables may lead to an
exponential blow-up of their size due to iterated application of rules, which
is defeated by a compression mechanism. Note also that equations of the form
$A\doteq e$, in particular $A\doteq\pi{\cdot}A^{\prime}$, cannot be solved by
substitutions ($A\mapsto\pi{\cdot}A^{\prime}$) for two reasons: (i) the atom
variable $A$ may occur in the right hand side, and (ii) due to our compression
mechanism (see below), the substitution may introduce cycles into the
compression, which is forbidden.

Atoms in the input are permitted. In the rules an extra mention of atoms is
only in (2), (3), (ElimFP), (ElimA), (Clashab), (FailF), (FailFS) and in
(ElimFP).

###### Definition 9.8

The algorithm LetrecUnifyAV operates on a tuple $(\Gamma,\nabla,\theta)$,
where the rules are defined in Figs. 7 and 8, and failure rules are in Fig. 9.

The rules (7) and (ElimA) are don’t know non-deterministic, whereas the other
ones are don’t care non-deterministic. The following explanations are in
order:

  1. 1.

$\Gamma$ is assumed to be a set of flattened equations $e_{1}\doteq e_{2}$
(see the remarks after Definition 4.3).

  2. 2.

We assume that $\doteq$ is symmetric,

  3. 3.

$\nabla$ contains freshness constraints, like $a{\\#}e$, $A{\\#}e$, which in
certain cases may be written as equations of the form
$A=_{\\#}\pi{\cdot}A^{\prime}$ (see Remark 9.7, for better readability and
simplicity).

  4. 4.

$\theta$ represents the already computed substitution as a list of
replacements of the form $X\mapsto e$. We assume that the substitution is the
iterated replacement. Initially $\theta$ is empty.

The final state will be reached, i.e. the output, when $\Gamma$ only contains
fixpoint equations of the form $\pi_{1}{\cdot}X\doteq\pi_{2}{\cdot}X$, and the
rule (Output) fires.

In the notation of the rules, we will use $[e/X]$ as substitution that
replaces $X$ by $e$. We may omit $\nabla$ or $\theta$ in the notation of a
rule, if they are not changed. We will also use a notation “$|$” in the
consequence part of rule (6), where all possibilities for $\rho$ have to be
considered (denoted as the set $\\{\rho\\}$), to denote disjunctive (i.e.
don’t know) nondeterminism. There are two nondeterministic rules with
disjunctive nondeterminism: the letrec-decomposition rule (7) exploring all
alternatives of the correspondence between bindings; the other one is (ElimA)
that guesses the instantiation of an atom-variable. In case it is guessed to
be different from all currently used atoms, we remember this fact (for
simplicity) by selecting a fresh atom for instantiation. The other rules can
be applied in any order, where it is not necessary to explore alternatives.

We assume that permutations in the algorithm LetrecUnifyAV are compressed
using a grammar-mechanism, as a variation of grammar-compression in [47, 48].
However, we do not mention it in the rules of the algorithm, but we will use
it in the complexity arguments (see below).

The use of the iterated decomposition in rule (7) appears clumsy at a first
look, however, it is an easy algorithmic representation of the method to
define the permutations (with atom variables) in a recursive fashion, where
the introduction of permutation variables is avoided.

###### Definition 9.9

The components of a permutation grammar $G$, used for compression, are:

  * •

Nonterminals $P_{i}$.

  * •

For every nonterminal $P_{i}$ there is an associated inverse $P_{j}$, which
can also be written as $\overline{P}_{i}$.

  * •

Rules of the form $P_{i}\to w_{1}\ldots w_{n}$, $n\geq 1$ where $w_{i}$ is
either a nonterminal or a terminal. At all times
$\overline{P}_{i}\to\overline{w}_{n}\ldots\overline{w}_{1}$ holds, i.e., if a
nonterminal is added its inverse is added accordingly. Usually, $n\leq 2$, but
also another fixed bound for $n$ is possible.

  * •

Terminal elements are $\emptyset$, $(V_{1}~{}V_{2})$.

The grammar is deterministic: every nonterminal is on the left-hand side of
exactly one rule. It is also non-recursive: the terminal index is such that
$P_{i}$ can only be in right-hand sides of the nonterminal $P_{j}$ with $j<i$.
The function $inv$, mapping $P_{i}\to\overline{P}_{i}$ and $T\to T$ for
terminals $T$ computes the inverse in constant time. This is true by
construction, because if $P\to w_{1}\ldots w_{n}$ then
$inv(P)\to\mathit{inv}(w_{n})\ldots\mathit{inv}(w_{1})$ and
$\mathit{inv}(T)=T$ for terminals. Every nonterminal $P$ represents a
permutation $\mathit{val}(P)$, which is computed from the grammar as follows:

  1. 1.

$\mathit{val}(P)=\mathit{val}(w_{1})~{}\ldots~{}\mathit{val}(w_{n})$ (as a
composition of permutations), if $P\to w_{1}\ldots w_{n}$.

  2. 2.

$\mathit{val}(\emptyset)=\mathit{Id}$.

  3. 3.

$\mathit{val}((P_{1}{\cdot}V_{1}~{}P_{2}{\cdot}V_{2}))=(\mathit{val}(P_{1}){\cdot}V_{1}~{}~{}\mathit{val}(P_{2}){\cdot}V_{2})$.

###### Lemma 9.10

For nonterminals $P$ of a permutation grammar $G$, the permutation
$\mathit{val}(\mathit{inv}(P))$ is the inverse of $\mathit{val}(P)$.

###  9.3 Arguments for correctness and completeness

Let $S$ denote in the following the size of the initial unification problem.

###### Proposition 9.11

Let $G$ be a permutation grammar, and let $P$ be a nonterminal, such that
$\mathit{val}(P)$ contains $n$ atoms, and does not contain any atom variables.
Then $\mathit{val}(P)$ can be transformed into a permutation of length at most
$n$ in polynomial time.

###### Proof 9.12

For every $P$ the size of the set $At(P)$ has an upper bound $S$ and can be
computed in time $O(S\cdot\log(S))$ For every such atom $a\in At(P)$ we
compute its image $P\cdot a$ and save the result in a mapping from atoms to
atoms. The computation of $P\cdot a$ can be done in $O(S^{2})$, yielding a
total of $O(S^{3})$ for the construction of this map, which has size $O(S)$.
At last, the construction of the permutation list can be done in linear time,
i.e. $O(S)$.

Now we consider the operations to extend the grammar during the unification
algorithm. By extension we mean to add non-terminals and rules to the grammar,
where the grammar is used as a compression device.

###### Proposition 9.13

Extending $n$ times the grammar $G$ can be performed in polynomial time in
$n$, and the size of the initial grammar $G$.

###### Proof 9.14

We check the extension operations:
Adding a nonterminal can be done in constant time. Adding an inverse of $P$ is
in constant time, since the inverses of the sub-permutations are already
available. Adding a composition $P=P_{1}{\cdot}P_{2}$ and at the same time the
inverse, can be done in constant time.

This polynomial upper bound will be used in the Proof of Theorem 9.19.

As a summary we obtain: Generating the permutation grammar on the fly during
the execution of the unification rules can be done in polynomial time, since
(as we will show below) the number of rule executions is polynomial in the
size of the initial input. Also the operation of applying a compressed ground
permutation to an atom is polynomial.

Note that (MMS) and (FPS), without further precaution, may cause an
exponential blow-up in the number of fixpoint equations (see Example 4.6). The
rule (ElimFP) will limit the number of fixpoint equations for atom-only
permutations by exploiting knowledge on operations on permutation groups. The
rule (ElimA) can be used according to a dynamic strategy (see below): if the
space requirement for the state is too high, then it can be applied until
simplification rules make $(\Gamma,\nabla)$ smaller.

The rule (Output) terminates an execution on $\Gamma_{0}$ by outputting a
unifier $(\theta,\nabla^{\prime},{\cal X})$, where the solvability of
$\nabla^{\prime}$ needs to be checked using methods as in the algorithm
proposed in [27]. The method is to nondeterministically instantiate atom-
variables by atoms, and then checking the freshness constraints, which is in
NP (see also Theorem 5.3).

We will show that the algorithm runs in polynomial time by applying (ElimA)
following a strategy defined below. There are two rules, which can lead to a
size increase of the unification problem if we ignore the size of the
permutations: (MMS) and (FPS):

  * •

(MMS) Given the equations $X\doteq e_{1},X\doteq e_{2}$, the increase of the
size of $\Gamma$ after the application of the rule has an upper bound $O(S)$.

  * •

(FPS) Given $X\doteq\pi_{1}{\cdot}X,\ldots,X\doteq\pi_{k}{\cdot}X,X\doteq e$,
the size increase has an upper bound $O(S)$. Disregarding the permutations of
only atoms, it is not known whether there exists a polynomial upper bound of
the number of independent permutations with atom variables - but it seems very
unlikely.

###### Definition 9.15

Let $p(x)$ be some easily computable function
$\mathbb{R}^{+}\to\mathbb{R}^{+}$. The rule $\text{ElimAB}(p)$ is defined as
follows:

> $\text{ElimAB}(p)$: If there are $k>p(S)$ fixpoint equations
> $X\doteq\pi_{1}{\cdot}X,\ldots,X\doteq\pi_{k}{\cdot}X$ in $\Gamma$ for some
> variable $X$, then apply (ElimA) for all
> $A\in\mathit{AtVar}(\pi_{1},\dots,\pi_{k})$. Then immediately apply (ElimFP)
> exhaustively.

###### Definition 9.16

The guided version LetrecUnifyAVB$(p)$ of LetrecUnifyAV is obtained by
replacing (ElimA) with $\text{ElimAB}(p)$ where $p(x)$ is some (easily
computable) function $\mathbb{R}^{+}\to\mathbb{R}^{+}$, such that $\forall
x\in\mathbb{R}^{+}:q(x)\geq p(x)\geq x*\log(x)$ holds for some polynomial $q$.
In addition the priority of the rules is as follows, where highest priority
comes first: (1), …, (6), (ElimFP), (MMS), (Output). Then $\text{ElimAB}(p)$,
(FPS), and the nondeterministic rule (7) with lowest priority.

###### Lemma 9.17

Let $\Gamma,\nabla$ be a solvable input. For every function $p(x)$ with
$\forall x\in\mathbb{R}^{+}:p(x)\geq x\log(x)$, the algorithm
LetrecUnifyAVB$(p)$ does not get stuck, and for every intermediate state of
the algorithm LetrecUnifyAVB$(p)$ it holds that the number of fixpoint
equations per expression variable is bounded above by $p(S)$.

###### Proof 9.18

The upper bound of the number of fixpoint equations is proved as follows: Let
$m$ be the number of atoms in the original unification problem. The rule
(ElimA) (called by (ElimAB)) introduces at most $S-m$ new atoms, which implies
at most $S$ atoms at any time. If LetrecUnifyAVB$(p)$ exceeds its upper space
bound and applies $\text{ElimAB}(p)$ on the fixpoint equations
$X\doteq\pi_{1}{\cdot}X,\ldots,X\doteq\pi_{k}{\cdot}X$, the number of fixpoint
equations of $X$ can be reduced to at most $S\log(S)\leq p(S)$ (see the proof
of Theorem 5.3).

Since the input is solvable, the choices can be made accordingly, guided by
the solution, and then it is not possible that there is an occurs-check-
failure for the variables. Hence if the upper line of the preconditions of
(FPS) is a part of $\Gamma$, there will also be a maximal variable $X$, such
that the condition $X\not\in\mathit{Var}(\Gamma,e)$ can be satisfied.

The following theorem shows that the (non-deterministic) algorithm for nominal
unification with letrec and atom-variables can be guided by a strategy that
instantiates atom-variables only if the number of fixpoint equations grows too
large. The problem is that with atom-variables we could not exhibit a
redundancy eliminating rule for fixpoint-constraints as for the case with
atoms. The algorithm LetrecUnifyAVB$(p)$ provides this compromise. It guesses
the instantiation of certain atom-variables if the number of fixpoint
equations is greater than a bound. This strategy prevents for example an
exponential growth of the number of fixpoint-equations. There is flexibility
through the choice of a threshold-function. Thus Theorem 9.19 shows that with
a threshold function satisfying only weak conditions, the algorithm can be
controlled and that there is a chance to find a good practical compromise
between too much non-determinism and space-explosion.

The algorithm is sound and also complete, however, we do not provide explicit
arguments here.

###### Theorem 9.19

Let $\Gamma,\nabla$ be a solvable input. For every function $p(x)$ such that
there is a polynomial $q(x)$ with $\forall x:q(x)\geq p(x)\geq x\log(x)$,
LetrecUnifyAVB$(p)$ does not get stuck and runs in polynomial space and time.

###### Proof 9.20

The proof is inspired by the proof of Theorem 5.3, and uses Lemma 9.17 that
shows that the number of fixpoint-equations for a single variable is at most
$p(S)$.

Below we show some estimates on the size and the number of steps. The
termination measure
$({\\#\mathrm{Var}},{\\#\mathrm{Lr}\lambda\mathrm{FA}},{\\#\mathrm{Eqs}},{\\#\mathrm{EqNonX}})$,
which is ordered lexicographically, is as follows:

${\\#\mathrm{Var}}$

is the number of different variables in $\Gamma$,

${\\#\mathrm{Lr}\lambda\mathrm{FA}}$

is the number of letrec-, $\lambda$, function-symbols and atoms in $\Gamma$,
but not in permutations,

${\\#\mathrm{Eqs}}$

is the number of equations in $\Gamma$, and

${\\#\mathrm{EqNonX}}$

is the number of equations where non of the equated expressions is a variable.

Since shifting permutations down and simplification of freshness constraints
both terminate and do not increase the measures, we only compare states which
are normal forms for shifting down permutations and simplifying freshness
constraints.

The following table shows the effect of the rules: Let $S$ be the size of the
initial $(\Gamma_{0},\nabla_{0})$ where $\Gamma$ is already flattened. Again,
the entries $+W$ represent a size increase of at most $W$ in the relevant
measure component.

$\begin{array}[]{l||l|l|l|l}&{\\#\mathrm{Var}}&{\\#\mathrm{Lr}\lambda\mathrm{FA}}&{\\#\mathrm{Eqs}}&{\\#\mathrm{EqNonX}}\\\
\hline\cr(3)&<&\leq&=&\leq\\\ \mbox{(FPS)}&<&+2p(S)&<&+2p(S)\\\
\mbox{(MMS)}&=&<&+2S&=\\\ (4),(5),(6),(7)&=&<&+S&\leq\\\
\mbox{\text{ElimAB}(p)}&=&=&<&\leq\\\ (1)&\leq&\leq&<&\leq\\\ (2)&=&=&=&<\\\
\end{array}$

The table shows that the rule applications strictly decrease the measure. The
entries can be verified by checking the rules, and using the argument that
there are not more than $p(S)$ fixpoint equations for a single variable $X$.
We use the table to argue on the number of rule applications and hence the
complexity: The rules (3) and (FPS) strictly reduce the number of variables in
$\Gamma$ and can be applied at most $S$ times. The rule (FPS) increases the
second measure at most by $2p(S)$, since the number of symbols may be
increased as often as there are fixpoint-equations, and there are at most
$p(S)$. Thus the measure ${\\#\mathrm{Lr}\lambda\mathrm{FA}}$ will never be
greater than $2Sp(S)$.

The rule (MMS) strictly decreases ${\\#\mathrm{Lr}\lambda\mathrm{FA}}$, hence
${\\#\mathrm{Eqs}}$, i.e. the number of equations, is bounded by $4S^{2}p(S)$.
The same bound holds for ${\\#\mathrm{EqNonX}}$. Hence the number of rule
applications is $O(S^{2}p(S))$. Of course, there may be a polynomial effort in
executing a single rule, and by Proposition 9.13 the contribution of the
grammar-operations is also only polynomial. Finally, since $p(x)$ is
polynomially bounded by $q(x)$, the algorithm can be executed in polynomial
time.

##  10 Nominal letrec matching with environment variables

We extend the language $\mathit{LRLXA}$ by variables $\mathit{E}$ that may
encode (partial) letrec-environments for a nominal matching algorithm, which
leads to a larger coverage of practically occurring nominal matching problems
in reasoning about the (small-step operational) semantics of programming
languages with letrec.

###### Example 10.1

Consider as an example a rule (llet-e) of the operational semantics of a
functional core language, which merges letrec-environments (see [19]): $({\tt
letrec}~{}\mathit{E}_{1}~{}{\tt in}~{}({\tt letrec}~{}\mathit{E}_{2}~{}{\tt
in}~{}X))~{}\to~{}({\tt letrec}~{}\mathit{E}_{1};\mathit{E}_{2}~{}{\tt
in}~{}X).$ It can be applied to an expression $({\tt letrec}~{}a.0;b.1~{}{\tt
in}~{}({\tt letrec}~{}c.(a,b,c)~{}{\tt in}~{}c))$ as follows: The left-hand
side $({\tt letrec}~{}\mathit{E}_{1}~{}{\tt in}$ $({\tt
letrec}~{}\mathit{E}_{2}~{}{\tt in}~{}X))$ of the reduction rule matches
$({\tt letrec}~{}a.0;b.1~{}{\tt in}$ $({\tt letrec}$ $c.(a,b,c)~{}{\tt
in}~{}c))$ with the match:
$\\{\mathit{E}_{1}\mapsto\\{a.0;b.1\\};\mathit{E}_{2}\mapsto\\{c.(a,b,c)\\};X\mapsto
c\\}$, producing the next expression as an instance of the right hand side
$({\tt letrec}~{}\mathit{E}_{1};\mathit{E}_{2}~{}{\tt in}~{}X)$, which is
$({\tt letrec}~{}a.0;b.1;c.(a,b,c)~{}{\tt in}~{}c)$. Note that for application
to extended lambda calculi, more care is needed w.r.t. scoping in order to get
valid reduction results in all cases. The restriction that a single letrec
environment binds different variables becomes more important. The reduction
(llet-e) is correctly applicable, if the target expression satisfies the so-
called distinct variable convention, i.e., if all bound variables are
different and if all free variables in the expression are different from all
bound variables. In this section we will add freshness constraints that
enforce different binders in environments.

An alternative that is used for a similar unification task in [36] requires
the additional construct of non-capture constraints:
$\mathit{NCC}(\mathit{env}_{1},\mathit{env}_{2})$, which means that for every
valid instantiation $\rho$, variables occurring free in $env_{1}\rho$ are not
captured by the top letrec-binders in $env_{2}\rho$. In this paper we focus on
nominal matching for the extension with environment variables, and leave the
investigation of reduction rules and sequences for further work.

###### Definition 10.2

The grammar for the extended language $\mathit{LRLXAE}$ (LetRec Language
eXtended with Atom variables and Environment) variables $E$ is:

$\begin{array}[]{lcl}V&::=&a\mid A\\\ W&::=&\pi\cdot V\\\
\pi&::=&\emptyset\mid(W~{}W)\mid\pi{\circ}\pi\\\ e&::=&\pi{\cdot}X\mid
W\mid\lambda W.e\mid(f~{}e_{1}~{}\ldots e_{\mathit{ar}(f)})~{}|~{}({\tt
letrec}~{}\mathit{env}~{}{\tt in}~{}e)\\\ \mathit{env}&::=&E\mid
W.e\mid\mathit{env};\mathit{env}\mid\emptyset\end{array}$

$(1)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{e{\ \unlhd\
}e\\}}{\Gamma}}$ $(2)~{}{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\\{\pi_{1}{\cdot}A{\ \unlhd\
}a\\},\nabla,\theta}{\Gamma[\pi_{1}^{-1}{\cdot}a/A],\nabla[\pi_{1}^{-1}{\cdot}a/A],\theta\cup\\{A\mapsto\pi_{1}^{-1}{\cdot}a\\}}}$

$(3)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{\pi_{1}{\cdot}X{\
\unlhd\
}e\\},\nabla,\theta}{\Gamma[\pi_{1}^{-1}{\cdot}e/X],\nabla[\pi_{1}^{-1}{\cdot}e/X],\theta\cup\\{X\mapsto\pi_{1}^{-1}{\cdot}e\\}}}$
$(4)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{(f~{}e_{1}\ldots
e_{n})){\ \unlhd\ }(f~{}e_{1}^{\prime}\ldots
e_{n}^{\prime})\\}}{\Gamma\cup\\{e_{1}{\ \unlhd\ }e_{1}^{\prime},\ldots
e_{n}{\ \unlhd\ }e_{n}^{\prime}\\}}}$

$(5)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{(\lambda a.e_{1}{\
\unlhd\ }\lambda a.e_{2}\\}}{\Gamma\cup\\{e_{1}{\ \unlhd\ }e_{2}\\}}}$
$(6)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{(\lambda W.e_{1}{\
\unlhd\ }\lambda a.e_{2}\\},\nabla}{\Gamma\cup\\{(W~{}a){\cdot}e_{1}{\ \unlhd\
}e_{2}\\},\nabla\cup\\{a{\\#}\lambda W.e_{1}\\}}}$

$(7)~{}{\displaystyle\frac{\Gamma\mathaccent
0{\cdot}\cup\left\\{\begin{array}[]{l}{\tt
letrec}~{}W_{1}.e_{1};\ldots;W_{n}.e_{n}~{}{\tt in}~{}e{\ \unlhd}\\\ {\tt
letrec}~{}a_{1}.e^{\prime}_{1};\ldots;a_{n}.e^{\prime}_{n}~{}{\tt
in}~{}e^{\prime}\end{array}\right\\},\nabla\qquad\begin{array}[]{l}\mbox{If
the left hand side environment}\\\ \mbox{does not contain environment
variables.}\end{array}}{\begin{array}[]{l}{\begin{array}[]{ll}{\begin{array}[]{c}\left|\begin{array}[]{c}{}\hfil\\\
{}\hfil\\\ {}\hfil\\\ \end{array}\right.\\\
{\\{\rho\\}}\end{array}}&\left(\begin{array}[]{l}\Gamma\,\mathop{\cup}\,\left\\{\begin{array}[]{l}~{}\mathrm{decompose}(n\\!+\\!1,\lambda
W_{1}\ldots\lambda W_{n}.(e_{1},\ldots,e_{n},e))\\\ \hskip 19.91684pt{\
\unlhd\ }\lambda a_{\rho(1)}.\ldots\lambda
a_{\rho(n)}.(e^{\prime}_{\rho(1)},\ldots,e^{\prime}_{\rho(n)},e^{\prime}))\end{array}\right\\},\\\
{}\\\\[-14.22636pt]
\nabla\cup\left\\{\begin{array}[]{l}~{}\mathrm{decompfresh}(n\\!+\\!1,\lambda
W_{1}\ldots\lambda W_{n}.(e_{1},\ldots,e_{n},e))\\\ \hskip
19.91684pt\doteq\lambda a_{\rho(1)}.\ldots\lambda
a_{\rho(n)}.e^{\prime}_{\rho(1)},\ldots,e^{\prime}_{\rho(n)},e^{\prime}))\end{array}\right\\}\end{array}\right)\end{array}{}}\\\\[5.69054pt]
\mbox{where $\rho$ is a permutation on $\\{1,\ldots,n\\}$ and
$\mathrm{decompose}(n,.)$ is the equation part of $n$-fold }{}\\\ \mbox{
application of rules (4), (5) or (6) and $\mathrm{decomposefresh}(n,.)$ is the
freshness constraint}{}\\\ \mbox{ part of the $n$-fold application of rules
(4), (5) or (6).}\\\ \end{array}}}$

$(8)~{}{\displaystyle\frac{\Gamma\mathaccent 0{\cdot}\cup\\{{\tt
letrec}~{}W_{1}.e_{1};\ldots;E;\ldots;W_{n}.e_{n}~{}{\tt in}~{}e{\ \unlhd\
}{\tt letrec}~{}a_{1}.e^{\prime}_{1};\ldots;a_{n}.e^{\prime}_{m}~{}{\tt
in}~{}e^{\prime}\\},\nabla,\theta}{\begin{array}[]{@{}l@{}}\begin{array}[]{@{}l@{}l@{}}{\begin{array}[]{@{}c@{}}\left|\begin{array}[]{@{}c@{}}{}\hfil\\\
\end{array}\right.\\\ {\\{\sigma\\}}\end{array}}&((\Gamma{\cup}\\{{\tt
letrec}~{}W_{1}.e_{1};\ldots;E;\ldots;W_{n}.e_{n}~{}{\tt in}~{}e{\ \unlhd\
}{\tt letrec}~{}a_{1}.e^{\prime}_{1};\ldots;a_{n}.e^{\prime}_{m}~{}{\tt
in}~{}e^{\prime}\\})\sigma,\nabla\sigma,\theta{\cup}\sigma{}\\\\[5.69054pt]
&\mbox{where $\sigma=\\{E\mapsto A_{1}.X_{1},\ldots A_{k}.X_{k}\\}$ where
$A_{i},X_{i}$ are fresh variables and $k\leq m-n$.}\end{array}\end{array}}}$

Figure 10: Standard and decomposition matching rules with environment
variables of LetrecEnvMatch.

We define a nominal matching algorithm, where in addition environment
variables may occur (also non-linear) in left hand sides, but not in the right
hand sides.

The matching algorithm with environment variables is described below. It can
be obtained from the algorithm LetrecUnifyAV by adding a rule that
(nondeterministically) instantiates environment variables by environments of
the form $W_{1}.X_{1};\ldots;W_{k}.X_{k}$. This can eliminate all environment
variables. After this operation of eliminating all environment variables, it
is possible to use the algorithm LetrecUnifyAV. However, since the equations
are match-equations, it is possible to derive simplified and optimized rules
of LetrecUnifyAV. We describe the rules explicitly, in order to exhibit the
optimization possibilities of a matching algorithm compared with a unification
algorithm.

###### Definition 10.3

The matching algorithm LetrecEnvMatch is described in Fig. 10. Permitted
inputs are matching equations between expressions, i.e. variables are only
permitted in left hand sides of (matching) equations. The don’t know-
nondeterminism is indicated in the respective rules.
It is assumed that in the input as well as after instantiating the
$\mathit{env}$-variables, the freshness constraints contain constraints that
prevent that a letrec-environment contains bindings with the same binder (see
Remark 9.3). The result is a substitution, a freshness constraint and a
substitution.

We omit failure rules, since these obviously follow from the nominal matching
algorithm. Guessing the number of instances into environment variables may
lead to clashes due to a wrong number of bindings in environments. An
implementation can be more clever by checking the possible number of bindings
before guessing.

It is easy to see that the problem itself is in NP, by the following argument:
Guess atom-variables in the left hand side, where we only have to choose from
the already existing atom-variables in the problem and a fresh atom, and
iterate this until all atom-variables are replaced. Then we guess the
environment variables in a general way, as in rule (8), where the number of
bindings is at most the maximal number of bindings in the letrec-environments
in the right hand side. This (non-deterministic) guessing and replacement is
polynomial. Then we can apply Theorem 5.7. Since the rules of LetrecEnvMatch
are simplified rules of the algorithm LetrecUnifyAV, we obtain:

###### Theorem 10.4

The nominal matching algorithm LetrecEnvMatch is sound and complete and runs
in NP time.

##  11 Conclusion and future research

We construct nominal unification algorithms for expressions with letrec, for
the case where only atoms are permitted, and also for the case where in
addition atom variables are permitted. We also describe several nominal letrec
matching algorithms for variants, in particular also for expressions with
environment variables. All algorithms run in (nondeterministic) polynomial
time. Future research is to investigate extensions of nominal unification with
environment variables $\mathit{E}$, perhaps as an extension of the matching
algorithm.

Future work is also an investigation into the connection with equivariant
nominal unification [15, 16, 17], and to investigate nominal matching together
with equational theories. Also applications of nominal techniques to reduction
steps in operational semantics of calculi with letrec and transformations
should be more deeply investigated. Also nominal unification in the
combination of letrec, environment variables and atom variables is subject to
future research.

### Acknowledgements

The research of Manfred Schmidt-Schauß was partially supported by the Deutsche
Forschungsgemeinschaft (DFG) under grant SCHM 986/11-1.

The research for the author Temur Kutsia was partially supported by the
Austrian Science Fund (FWF) project P 28789-N32.

The research of Jordi Levy was partially supported by the MINECO/FEDER
projects RASO (TIN2015-71799-C2-1-P) and LoCoS (TIN2015-66293-R).

The research of Mateu Villaret was partially supported by UdG project
MPCUdG2016/055.

We thank the reviewers for their detailed comments that greatly helped to
improve the paper.

## References

  * [1] Schmidt-Schauß M, Kutsia T, Levy J, Villaret M.  Nominal Unification of Higher Order Expressions with Recursive Let.  In: Hermenegildo MV, López-García P (eds.), Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers, volume 10184 of _Lecture Notes in Computer Science_. Springer, 2016 pp. 328–344.  10.1007/978-3-319-63139-4_19.
  * [2] Baader F, Snyder W.  Unification Theory.  In: Robinson JA, Voronkov A (eds.), Handbook of Automated Reasoning, pp. 445–532. Elsevier and MIT Press, 2001.
  * [3] Huet GP.  A Unification Algorithm for Typed lambda-Calculus.  _Theor. Comput. Sci._ , 1975.  1(1):27–57.  10.1016/0304-3975(75)90011-0.
  * [4] Goldfarb WD.  The Undecidability of the Second-Order Unification Problem.  _Theor. Comput. Sci._ , 1981.  13:225–230.  10.1016/0304-3975(81)90040-2.
  * [5] Levy J, Veanes M.  On the Undecidability of Second-Order Unification.  _Inf. Comput._ , 2000.  159(1-2):125–150.  10.1006/inco.2000.2877.
  * [6] Urban C, Pitts AM, Gabbay M.  Nominal Unification.  In: 17th CSL, 12th EACSL, and 8th KGC, volume 2803 of _LNCS_. Springer, 2003 pp. 513–527.  10.1007/978-3-540-45220-1_41.
  * [7] Urban C, Pitts AM, Gabbay MJ.  Nominal unification.  _Theor. Comput. Sci._ , 2004.  323(1–3):473–497.  10.1016/j.tcs.2004.06.016.