replemma[1]

###### Lemma 0.1

reptheorem[1]

###### Theorem 0.1

11institutetext: St Petersburg University and JetBrains Research, Russia
11email<EMAIL_ADDRESS>11email<EMAIL_ADDRESS>
# Scheduling Complexity of Interleaving Search

Dmitry Rozplokhas  0000-0001-7882-4497
Dmitry Boulytchev  0000-0001-8363-7143

###### Abstract

miniKanren is a lightweight embedded language for logic and relational
programming. Many of its useful features come from a distinctive search
strategy, called _interleaving search_. However, with interleaving search
conventional ways of reasoning about the complexity and performance of logical
programs become irrelevant. We identify an important key component —
_scheduling_ — which makes the reasoning for miniKanren so different, and
present a semi-automatic technique to estimate the scheduling impact via
symbolic execution for a reasonably wide class of programs.

###### Keywords:

miniKanren, interleaving search, time complexity, symbolic execution

##  1 Introduction

⬇ appendo = $\lambda\;\;$ a b ab . ((a $\,\equiv\,$ Nil) /\ (ab $\,\equiv\,$ b)) \/ (fresh (h t tb) (a $\,\equiv\,$ Cons(h, t)) /\ (appendo t b tb) /\ (ab $\,\equiv\,$ Cons(h, tb))) |
---|---
⬇ append${}^{o}_{opt}$ = $\lambda\;\;$ a b ab . ((a $\,\equiv\,$ Nil) /\ (ab
$\,\equiv\,$ b)) \/ (fresh (h t tb) (a $\,\equiv\,$ Cons(h, t)) /\ (ab
$\,\equiv\,$ Cons(h, tb) /\ (append${}^{o}_{opt}$ t b tb)))

Figure 1: Two implementations of list concatenation and their performance for
$a=[1,\dots,n]$, $b=[1,\dots,100]$, and $ab$ left free.

A family of embedded languages for logic and, more specifically, relational
programming miniKanren [10] has demonstrated an interesting potential in
various fields of program synthesis and declarative programming [5, 6, 14]. A
distinctive feature of miniKanren is _interleaving search_ [13] which, in
particular, delivers such an important feature as completeness.

However, being a different search strategy than conventional BFS/DFS/iterative
deepening, etc., interleaving search makes the conventional ways of reasoning
about the complexity of logical programs not applicable. Moreover, some
intrinsic properties of interleaving search can manifest themselves in a
number of astounding and, at the first glance, unexplainable performance
effects.

As an example, let’s consider two implementations of list concatenation
relation (Fig. 1, left side); we respect here a conventional tradition for
miniKanren programming to superscript all relational names with “o”. The only
difference between the two is the position of the recursive call. The
evaluation of these implementations on the same problem (Fig. 1, right side)
shows that the first implementation works significantly slower, although it
performs exactly the same number of unifications. As a matter of fact, these
two implementations even have different _asymptotic_ complexity under the
assumption that occurs check is disabled.111The role of occurs check is
discussed in Section 5. Although the better performance of the
append${}_{opt}^{o}$ relation is expected even under conventional strategies
due to tail recursion, the asymptotic difference is striking.

A careful analysis discovers that the difference is caused not by
unifications, but by the process of _scheduling_ goals during the search. In
miniKanren a lazy structure is maintained to decompose the goals into
unifications, perform these unifications in a certain order, and thread the
results appropriately. For the append${}_{opt}^{o}$ relation the size of this
structure is constant, while for the appendo this structure becomes linear in
size, reducing the performance.

This paper presents a formal framework for scheduling cost complexity analysis
for interleaving search in miniKanren. We use the reference operational
semantics, reflecting the behaviour of actual implementations [15], and prove
the soundness of our approach w.r.t. this semantics. The roadmap of the
approach is as follows: we identify two complexity measures (one of which
captures _scheduling complexity_) and give exact and approximate recursive
formulae to calculate them (Section 3); then we present a procedure to
automatically extract inequalities for the measures for a given goal using
symbolic execution (Section 4). These inequalities have to be reformulated and
solved manually in terms of a certain _metatheory_ , which, on success,
provides asymptotic bounds for the scheduling complexity of a goal evaluation.
Our approach puts a number of restrictions on the goal being analyzed as well
as on the relational program as a whole. We explicitly state these
restrictions in Section 2 and discuss their impact in Section 7. The proofs of
all lemmas and theorems can be found in Appendix 0.A.

##  2 Background: Syntax and Semantics of miniKanren

In this section, we recollect some known formal descriptions for miniKanren
language that will be used as a basis for our development. The descriptions
here are taken from [15] (with a few non-essential adjustments for
presentation purposes) to make the paper self-contained, more details and
explanations can be found there.

The syntax of core miniKanren is shown in Fig. 2. All data is presented using
terms $\mathcal{T}_{X}$ built from a fixed set of constructors $\mathcal{C}$
with known arities and variables from a given set $X$. We parameterize the
terms with an alphabet of variables since in the semantic description we will
need _two_ kinds of variables: _syntactic_ variables $\mathcal{X}$, used for
bindings in the definitions, and _logic_ variables $\mathcal{A}$, which are
introduced and unified during the evaluation. We assume the set $\mathcal{A}$
is ordered and use the notation $\alpha_{i}$ to specify a position of a
logical variable w.r.t. this order.

There are five types of goals: unification of two terms, conjunction and
disjunction of goals, fresh logic variable introduction, and invocation of
some relational definition. For the sake of brevity, in code snippets, we
abbreviate immediately nested “fresh” constructs into the one, writing “fresh
x y $\dots$ . $g$” instead of “fresh x . fresh y . $\dots$ $g$”. The
_specification_ $\mathcal{S}$ consists of a set of relational definitions and
a top-level goal. A top-level goal represents a search procedure that returns
a stream of substitutions for the free variables of the goal.

${\begin{array}[]{ccll}\mathcal{C}&=&\\{C_{i}^{k_{i}}\\}&\mbox{constructors}\\\
\mathcal{T}_{X}&=&X\cup\\{C_{i}^{k_{i}}(t_{1},\dots,t_{k_{i}})\mid
t_{j}\in\mathcal{T}_{X}\\}&\mbox{terms over the set of variables $X$}\\\
\mathcal{D}&=&\mathcal{T}_{\varnothing}&\mbox{ground terms}\\\
\mathcal{X}&=&\\{\mbox{{x}},\mbox{{y}},\mbox{{z}},\dots\\}&\mbox{syntactic
variables}\\\ \mathcal{A}&=&\\{x,y,z\dots\\}&\mbox{logic variables}\\\
\mathcal{R}&=&\\{R_{i}^{k_{i}}\\}&\mbox{relational symbols with
arities}\\\\[5.69054pt]
\mathcal{G}&=&\mathcal{T_{X}}\equiv\mathcal{T_{X}}&\mbox{equality}\\\
&&\mathcal{G}\wedge\mathcal{G}&\mbox{conjunction}\\\
&&\mathcal{G}\vee\mathcal{G}&\mbox{disjunction}\\\
&&\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{{f}resh}}}}}}\;\mathcal{X}\;.\;\mathcal{G}&\mbox{fresh
variable introduction}\\\
&&R_{i}^{k_{i}}(t_{1},\dots,t_{k_{i}}),\;t_{j}\in\mathcal{T_{X}}&\mbox{relational
symbol invocation}\\\\[5.69054pt]
\mathcal{S}&=&\\{R_{i}^{k_{i}}=\lambda\;\mbox{{x}}_{1}^{i}\dots\mbox{{x}}_{k_{i}}^{i}\,.\,g_{i};\\}\;g,\;g_{i},g\in\mathcal{G}\phantom{XXX}&\mbox{specification}\end{array}$
Figure 2: The syntax of miniKanren

During the evaluation of miniKanren program an environment, consisting of a
substitution for logic variables and a counter of allocated logic variables,
is threaded through the computation and updated in every unification and fresh
variable introduction. The substitution in the environment at a given point
and given branch of evaluation contains all the information about relations
between the logical variables at this point. Different branches are combined
via _interleaving search_ procedure [13]. The answers for a given goal are
extracted from the final environments.

$\begin{array}[]{ccllcccll}\Sigma&=&\mathcal{A}\to\mathcal{T}_{\mathcal{A}}&\mbox{substitutions}&&S&=&\langle\mathcal{G},\,E\rangle&\mbox{task}\\\
E&=&\Sigma\times\mathbb{N}&\mbox{environments}&&&&S\oplus S&\mbox{sum}\\\
&&&&&&&S\otimes\mathcal{G}&\mbox{product}\\\
L&=&\circ\;\mid\;E&\mbox{labels}&&\hat{S}&=&\diamond\;\mid\;S&\mbox{states}\\\
\end{array}$ Figure 3: States and labels in the LTS for miniKanren

This search procedure is formally described by operational semantics in the
form of a labeled transition system. This semantics corresponds to the
canonical implementation of interleaving search.

The form of states and labels in the transition system is defined in Fig. 3.
Non-terminal states $S$ have a tree-like structure with intermediate nodes
corresponding to partially evaluated conjunctions (“$\otimes$”) or
disjunctions (“$\oplus$”). A leaf in the form $\langle g,\,e\rangle$
determines a task to evaluate a goal $g$ in an environment $e$. For a
conjunction node, its right child is always a goal since it cannot be
evaluated unless some result is provided by the left conjunct. We also need a
terminal state $\diamond$ to represent the end of the evaluation. The label
“$\circ$” is used to mark those steps which do not provide an answer;
otherwise, a transition is labeled by an updated environment.

${\begin{array}[]{crcr}\lx@intercol\hfil\langle t_{1}\equiv
t_{2},\,(\sigma,n)\rangle\xrightarrow{\circ}\Diamond,\,\,\nexists\;mgu\,(t_{1}\sigma,t_{2}\sigma)\hfil\lx@intercol&\mbox{[{UnifyFail}]}\\\
\lx@intercol\hfil\langle t_{1}\equiv
t_{2},\,(\sigma,n)\rangle\xrightarrow{(mgu\,(t_{1}\sigma,t_{2}\sigma)\circ\sigma),\,n)}\Diamond\hfil\lx@intercol&\mbox{[{UnifySuccess}]}\\\
\lx@intercol\hfil\langle\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{{f}resh}}}}}}\,\mbox{{x}}\,.\,g,\,(\sigma,n)\rangle\xrightarrow{\circ}\langle
g\,[{\raisebox{1.99997pt}{$\alpha_{n+1}$}\left/\raisebox{-1.99997pt}{$\mbox{{x}}$}\right.}],\,(\sigma,n+1)\rangle\hfil\lx@intercol&\mbox{[{Fresh}]}\\\
\lx@intercol\hfil\dfrac{R_{i}^{k_{i}}=\lambda\,\mbox{{x}}_{1}\dots\mbox{{x}}_{k_{i}}\,.\,g}{\langle
R_{i}^{k_{i}}\,(t_{1},\dots,t_{k_{i}}),\,e\rangle\xrightarrow{\circ}\langle
<EMAIL_ADDRESS>\langle g_{1}\lor g_{2},\,e\rangle\xrightarrow{\circ}\langle
g_{1},\,e\rangle\oplus\langle g_{2},\,e\rangle&\mbox{[{Disj}]}&\langle
g_{1}\land g_{2},\,e\rangle\xrightarrow{\circ}\langle g_{1},\,e\rangle\otimes
g_{2}&\mbox{[{Conj}]}\\\ \dfrac{s_{1}\xrightarrow{l}\Diamond}{(s_{1}\oplus
s_{2})\xrightarrow{l}s_{2}}&\mbox{[{DisjStop}]}&\dfrac{s_{1}\xrightarrow{l}s^{\prime}_{1}}{(s_{1}\oplus
s_{2})\xrightarrow{l}(s_{2}\oplus s^{\prime}_{1})}&\mbox{[{DisjStep}]}\\\
\dfrac{s\xrightarrow{\circ}\Diamond}{(s\otimes
g)\xrightarrow{\circ}\Diamond}&\mbox{[{ConjStop}]}&\dfrac{s\xrightarrow{e}\Diamond}{(s\otimes
g)\xrightarrow{\circ}\langle g,\,e\rangle}&\mbox{[{ConjStopAns}]}\\\
\dfrac{s\xrightarrow{\circ}s^{\prime}}{(s\otimes
g)\xrightarrow{\circ}(s^{\prime}\otimes
g)}&\mbox{[{ConjStep}]}&\dfrac{s\xrightarrow{e}s^{\prime}}{(s\otimes
g)\xrightarrow{\circ}(\langle g,\,e\rangle\oplus(s^{\prime}\otimes
g))}&\mbox{[{ConjStepAns}]}\end{array}$ Figure 4: Operational semantics of
interleaving search

The transition rules are shown in Fig. 4. The first six rules define the
evaluation of leaf states. For the disjunction and conjunction, the
corresponding node states are constructed. For other types of goals the
environment and the evaluated goal are updated in accordance with the task
given by the goal: for an equality the most general unifier of the terms is
incorporated into the substitution (or execution halts if the terms are non-
unifiable); for a fresh construction a new variable is introduced and the
counter of allocated variables is incremented; for a relational call the body
of the relation is taken as the next goal. The rest of the rules define
composition of evaluation of substates for partial disjunctions and
conjunctions. For a partial disjunction, the first constituent is evaluated
for one step, then the constituents are swapped (which constitutes the
_interleaving_), and the label is propagated. When the evaluation of the first
constituent of partial disjunction halts, the evaluation proceeds with the
second constituent. For a partial conjunction, the first constituent is
evaluated until the answer is obtained, then the evaluation of the second
constituent with this answer as the environment is scheduled for evaluation
together with the remaining partial conjunction (via partial disjunction
node). When the evaluation of the first constituent of partial conjunction
halts, the evaluation of the conjunction halts, too.

The introduced transition system is completely deterministic, therefore a
derivation sequence for a state $s$ determines a certain _trace_ — a sequence
of states and labeled transitions between them. It may be either finite
(ending with the terminal state $\Diamond$) or infinite. We will denote by
$\mathcal{T}r^{st}(s)$ the sequence of states in the trace for initial state
$s$ and by $\mathcal{T}r^{ans}(s)$ the sequence of answers in the trace for
initial state $s$. The sequence $\mathcal{T}r^{ans}(s)$ corresponds to the
stream of answers in the reference miniKanren implementations.

In the following we rely on the following property of leaf states:

###### Definition 1

A leaf state $\langle g,\,(\sigma,\,n)\rangle$ is well-formed iff
$\mathcal{FV}\,({g})\cup\mathcal{D}om\,(\sigma)\cup\mathcal{VR}an\,(\sigma)\subseteq\\{\alpha_{1},\dots,\alpha_{n}\\}$,
where $\mathcal{FV}\,({g})$ denotes the set of free variables in a goal $g$,
$\mathcal{D}om\,(\sigma)$ and $\mathcal{VR}an\,(\sigma)$ — the domain of a
substitution $\sigma$ and a set of all free variables in its image
respectively.

Informally, in a well-formed leaf state all free variables in goals and
substitution respect the counter of free logical variables. This definition is
in fact an instance of a more general definition of well-formedness for all
states, introduced in [15], where it is proven that the initial state is well-
formed and any transition from a well-formed state results in a well-formed
one.

Besides operational semantics, we will make use of a denotational one
analogous to the least Herbrand model. For a relation $R^{k}$, its
denotational semantics $\llbracket R^{k}\rrbracket$ is treated as a $k$-ary
relation on the set of all ground terms, where each “dimension” corresponds to
a certain argument of $R^{k}$. For example,
${\llbracket\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{append}}{\@listingGroup{}{$^{o}$}}}}}\rrbracket$
is a set of all triplets of ground lists, in which the third component is a
concatenation of the first two. The concrete description of the denotational
semantics is given in [15] as well as the proof of the soundness and
completeness of the operational semantics w.r.t. to the denotational one.

${\begin{array}[]{ccll}B_{nf}&=&\mathcal{T}_{\mathcal{X}}\equiv\mathcal{T}_{\mathcal{X}}\;\mid\;R^{k}\,(\mathcal{T}_{\mathcal{X}},\,\dots,\,\mathcal{T}_{\mathcal{X}})\\\
C_{nf}&=&B_{nf}\;\mid\;C_{nf}\land B_{nf}\\\
F_{nf}&=&C_{nf}\;\mid\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{{f}resh}}}}}}\,X\;.\;F_{nf}\\\
D_{nf}&=&F_{nf}\;\mid\;D_{nf}\lor F_{nf}\end{array}$ Figure 5: Disjunctive
Normal Form for goals

Finally, we explicitly enumerate all the restrictions required by our method
to work:

  * •

All relations have to be in DNF (set $D_{nf}$ in Fig.5).

  * •

We only consider goals which converge with a finite number of answers.

  * •

All answers have to be ground (_groundness_ condition) for all relation
invocations encountered during the evaluation.

  * •

All answers have to be unique (_answer uniqueness_ condition) for all relation
invocations encountered during the evaluation.

##  3 Scheduling Complexity

We may notice that the operational semantics described in the previous section
can be used to calculate the exact number of elementary scheduling steps. Our
first idea is to take the number of states $d\,(s)$ in the finite trace for a
given state $s$:

$d\,(s)\;\overset{\mathrm{def}}{=}\;|\mathcal{T}r^{st}(s)|$

However, it turns out that this value alone does not provide an accurate
scheduling complexity estimation. The reason is that some elementary steps in
the semantics are not elementary in existing implementations. Namely, a
careful analysis discovers that each semantic step involves navigation to the
leftmost leaf of the state which in implementations corresponds to multiple
elementary actions, whose number is proportional to the height of the leftmost
branch of the state in question. Here we provide an _ad-hoc_ definition for
this value, $t\,(s)$, which we call the _scheduling factor_ :

$t\,(s)\overset{\mathrm{def}}{=}\sum\limits_{s_{i}\in\mathcal{T}r^{st}(s)}lh\,(s_{i})$

where $lh\,(s_{i})$ is the height of the leftmost branch of the state.

In the rest of the section, we derive recurrent equations which would relate
the scheduling complexity for states to the scheduling complexity for their
(immediate) substates. It turns out that to come up with such equations both
$t$ and $d$ values have to be estimated simultaneously.

The next lemma provides the equations for $\oplus$-states:

lem:sum_measure_equations For any two states $s_{1}$ and $s_{2}$

$\begin{array}[]{rcl}d\,(s_{1}\oplus s_{2})&=&d\,(s_{1})+d\,(s_{2})\\\
t\,(s_{1}\oplus s_{2})&=&t\,(s_{1})+t\,(s_{2})+cost_{\oplus}(s_{1}\oplus
s_{2})\end{array}$

where $cost_{\oplus}(s_{1}\oplus s_{2})=\min\,\\{2\cdot d\,(s_{1})-1,2\cdot
d\,(s_{2})\\}$

Informally, for a state in the form $s_{1}\oplus s_{2}$ the substates are
evaluated separately, one step at a time for each substate, so the total
number of semantic steps is the sum of those for the substates. However, for
the scheduling factor, there is an extra summand $cost_{\oplus}(s_{1}\oplus
s_{2})$ since the “leftmost heights” of the states in the trace are one node
greater than those for the original substates due to the introduction of one
additional $\oplus$-node on the top. This additional node persists in the
trace until the evaluation of one of the substates comes to an end, so the
scheduling factor is increased by the number of steps until that.

The next lemma provides the equations for $\otimes$-states:222We assume
$\Diamond\otimes g=\Diamond$

lem:times_measure_equations For any state $s$ and any goal $g$

$\begin{array}[]{rclr}d\,(s\otimes
g)&=&d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)&\qquad(\star)\\\ t\,(s\otimes
g)&=&t\,(s)+cost_{\otimes}(s\otimes
g)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}(t\,(\langle
g,\,a_{i}\rangle)+cost_{\oplus}(\langle
g,\,a_{i}\rangle\oplus(s^{\prime}_{i}\otimes g)))&\qquad(\dagger)\end{array}$

where

$\begin{array}[]{rcl}cost_{\otimes}(s\otimes g)&=&d\,(s)\\\
s^{\prime}_{i}&=&\mbox{the first state in the trace for $s$ after}\\\
&&\mbox{a transition delivering the answer $a_{i}$}\\\ \end{array}$

For the states of the form $s\otimes g$ the reasoning is the same, but the
resulting equations are more complicated. In an $\otimes$-state the left
substate is evaluated until an answer is found, which is then taken as _an
environment_ for the evaluation of the right subgoal. Thus, in the equations
for $\otimes$-states the evaluation times of the second goal _for all the
answers_ generated for the first substate are summed up. The evaluation of the
right subgoal in different environments is added to the evaluation of the left
substate via creation of an $\oplus$-state, so for the scheduling factor there
is an additional summand $cost_{\oplus}(\langle g,\,a_{i}\rangle\oplus
s^{\prime}_{i})$ for each answer with $s^{\prime}_{i}$ being the state after
discovering the answer. There is also an extra summand
$cost_{\otimes}(s\otimes g)$ for the scheduling factor because of the
$\otimes$-node that increases the height in the trace, analogous to the one
caused by $\oplus$-nodes. Note, a $\otimes$-node is always placed immediately
over the left substate so this addition is exactly the number of steps for the
left substate.

Unfolding costs definitions in $(\dagger)$ gives us a cumbersome formula that
includes some intermediate states $s^{\prime}_{i}$ encountered during the
evaluation. However, as ultimately we are interested in asymptotic
estimations, we can approximate these costs up to a multiplicative constant.
We can notice that the value $d\,(s^{\prime}_{i}\otimes g)$ occurring in the
second argument of $cost_{\oplus}$ includes values $d\,(\langle
g,\,a_{j}\rangle)$ (like in the first argument) for all answers $a_{j}$ after
this intermediate state. So in the sum of all $cost_{\oplus}$ values
$d\,(\langle g,\,a_{i}\rangle)$ may be excluded for at most one answer, and in
fact, if we take the maximal one of these values we will get a rather precise
approximation. Specifically, we can state the following approximation333We
assume the following definition for $f\,(x)=g\,(x)+\Theta\,(h\,(x))$:
$\exists C_{1},C_{2}\in\mathcal{R^{+}},\,\forall x:g\,(x)+C_{1}\cdot
h\,(x)\leq f\,(x)\leq g\,(x)+C_{2}\cdot h\,(x)$ for $t\,(s\otimes g)$.

lem:otimes_t_approximation

$t\,(s\otimes
g)=t\,(s)+\left({\sum\limits_{a_{i}\in\mathcal{T}r^{ans}(s)}}t\,(\langle
g,\,a_{i}\rangle)\right)+\Theta\,(d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)-\smashoperator[]{\max^{\bullet}_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle))$

Hereafter we use the following notation:
$\displaystyle{\max^{\bullet}}\,S=\max\,(S\cup\\{0\\})$. We can see that the
part under $\Theta$ is very similar to the $(\star)$ except that here we
exclude $d$ value for one of the answers from the sum. This difference is
essential and, as we will see later, it is in fact responsible for the
difference in complexities for our motivating example.

##  4 Complexity Analysis via Symbolic Execution

Our approach to complexity analysis is based on a semi-automatic procedure
involving symbolic execution. In the previous section, we presented formulae
to compositionally estimate the complexity factors for _non-leaf states_ of
operational semantics under the assumption that corresponding estimations for
_leaf states_ are given. In order to obtain corresponding estimations for
relations as a whole, we would need to take into account the effects of
relational invocations, including the recursive ones.

Another observation is that as a rule we are interested in complexity
estimations in terms of some _metatheory_. For example, dealing with relations
on lists we would be interested in estimations in terms of list lengths, with
trees — in terms of depth or number of nodes, with numbers — in terms of their
values, etc. It is unlikely that a generic term-based framework would provide
such specific information automatically. Thus, a viable approach would be to
extract some inequalities involving the complexity factors of certain
relational calls automatically and then let a human being solve these
inequalities in terms of a relevant metatheory.

For the sake of clarity we will provide a demonstration of complexity analysis
for a specific example — appendo relation from the introduction — throughout
the section.

The extraction procedure utilizes a symbolic execution technique and is
completely automatic. It turns out that the semantics we have is already
abstract enough to be used for symbolic execution with minor adjustments. In
this symbolic procedure, we mark some of the logic variables as “grounded” and
at certain moments substitute them with ground terms. Informally, for some
goal with some free logic variables we consider the complexity of a search
procedure which finds the bindings for all non-grounded variables based on the
ground values substituted for the grounded ones. This search procedure is
defined precisely by the operational semantics; however, as the concrete
values of grounded variables are unknown (only the fact of their
_groundness_), the whole procedure becomes symbolic. In particular, in
unification the groundness can be propagated to some non-grounded free
variables. Thus, the symbolic execution is determined by a set of grounded
variables (hereafter denoted as $V\subset\mathcal{A}$). The initial choice of
$V$ determines the problem we analyze.

In our example the objective is to study the execution when we specialize the
first two arguments with ground values and leave the last argument free. Thus,
we start with the goal appendo $a$ $b$ $ab$ (where $a$, $b$ and $ab$ are
distinct free logic variables) and set the initial $V=\\{a,b\\}$.

We can make an important observation that both complexity factors ($d$ and
$t$) are stable w.r.t. the renaming of free variables; moreover, they are also
stable w.r.t. the change of the fresh variables counter as long as it stays
adequate, and change of current substitution, as long as it gives the same
terms after application. Formally, the following lemma holds.

lem:measures_changing_env Let $s=\langle g,\,(\sigma,\,n)\rangle$ and
$s^{\prime}=\langle g^{\prime},\,(\sigma^{\prime},\,n^{\prime})\rangle$ be two
well-formed states. If there exists a bijective substitution $\pi\colon
FV\,(g\sigma)\to FV\,(g^{\prime}\sigma^{\prime})$ such that
$g\sigma\pi=g^{\prime}\sigma^{\prime}$, then $d\,(s)=d\,(s^{\prime})$ and
$t\,(s)=t\,(s^{\prime})$.

The lemma shows that the set of states for which a call to relation has to be
analyzed can be narrowed down to a certain family of states.

###### Definition 2

Let $g$ be a goal. An initial state for $g$ is $init\,(g)=\langle
g,\,(\varepsilon,n_{init}\,(g))\rangle$ with $n_{init}\,(g)=\min\,\\{n\mid
FV\,(g)\subseteq\\{\alpha_{1}\dots\alpha_{n}\\}\\}$

Due to the Lemma LABEL:lem:measures_changing_env it is sufficient for analysis
of a relational call to consider only the family of initial states since an
arbitrary call state encountered throughout the execution can be transformed
into an initial one while preserving both complexity factors. Thus, the
analysis can be performed in a compositional manner where each call can be
analyzed separately. For our example the family of initial states is
${q^{app}(\mathbf{a},\mathbf{b})=init\,(\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{append}}{\@listingGroup{}{$^{o}$}}{\@listingGroup{ltx_lst_space}{}}{\@listingGroup{}{$\mathbf{a}$}}{\@listingGroup{ltx_lst_space}{}}{\@listingGroup{}{$\mathbf{b}$}}{\@listingGroup{ltx_lst_space}{}}{\@listingGroup{}{$ab$}}}}})$
for arbitrary ground terms $\mathbf{a}$ and $\mathbf{b}$.

As we are aiming at the complexity estimation depending on specific ground
values substituted for grounded variables, in general case extracted
inequalities have to be parameterized by _valuations_ — mappings from the set
of grounded variables to ground terms. As the new variables are added to this
set during the execution, the valuations need to be extended for these new
variables. The following definition introduces this notion.

###### Definition 3

Let $V\subset U\subset\mathcal{A}$ and $\rho\colon
V\to\mathcal{T}_{\varnothing}$ and $\rho^{\prime}\colon
U\to\mathcal{T}_{\varnothing}$ be two valuations. We say that $\rho^{\prime}$
extends $\rho$ (denotation: $\rho^{\prime}\succ\rho$) if
$\rho^{\prime}\,(x)=\rho\,(x)$ for all $x\in V$.

The main objective of the symbolic execution in our case is to find
constraints on valuations for every leaf goal in the body of a relation that
determine whether the execution will continue and how a valuation changes
after this goal. For internal relational calls, we describe constraints in
terms of denotational semantics (to be given some meaning in terms of
metatheory later). We can do it because of a precise equivalence between the
answers found by operational semantics and values described by denotational
semantics thanks to soundness and completeness as well as our requirements of
grounding and uniqueness of answers. Our symbolic treatment of equalities
relies on the fact that substitutions of ground terms commute, in a certain
sense, with unifications. More specifically, we can use the most general
unifier for two terms to see how unification goes for two terms with some free
variables substituted with ground terms. The most general unifier may contain
bindings for both grounded and non-grounded variables. A potential most
general unifier for terms after substitution contains the same bindings for
non-grounding terms (with valuation applied to their rhs), while bindings for
grounding variables turn into equations that should be satisfied by the
unifier with ground value on the left and bound term on the right. In
particular, this means that all variables in bindings for grounded variables
become grounded, too. We can use this observation to define an iterative
process that determines the updated set of grounded variables
$\mbox{{upd}}\,(U,\,\delta)$ for a current set $U$ and a most general unifier
$\delta$ and a set of equations $\mbox{{constr}}\,(\delta,\,U)$ that should be
respected by the valuation.

$\begin{array}[]{rcl}\mbox{{upd}}\,(U,\,\delta)&=&\begin{cases}U&\quad\forall
x\in U:FV\,(\delta\,(x))\subset U\\\
\mbox{{upd}}\,(U\cup\displaystyle\bigcup\limits_{x\in
U}FV\,(\delta\,(x)),\,\delta)&\quad\mbox{otherwise}\end{cases}\\\
\mbox{{constr}}\,(\delta,\,U)&=&\\{x=\delta\,(x)\mid x\in
U\cap\mathcal{D}om\,(\delta)\\}\end{array}$

Using these definitions we can describe symbolic unification by the following
lemma.

lem:symbolic_unification_soundness Let $t_{1}$, $t_{2}$ be terms,
$V\subset\mathcal{A}$ and $\rho\colon V\to\mathcal{T}_{\varnothing}$ be a
valuation. If $mgu\,(t_{1},t_{2})=\delta$ and $U=\mbox{{upd}}\,(V,\,\delta)$
then $t_{1}\rho$ and $t_{2}\rho$ are unifiable iff there is some
$\rho^{\prime}\colon U\to\mathcal{T}_{\varnothing}$ such that
$\rho^{\prime}\succ\rho$ and
$\forall(y=t)\in\mbox{{constr}}\,(\delta,\,U)\,:\,\rho^{\prime}(y)=t\rho^{\prime}$.
In such case $\rho^{\prime}$ is unique and $\rho\circ
mgu\,(t_{1}\rho,t_{2}\rho)=\delta\circ\rho^{\prime}$ up to alpha-equivalence
(e.g. there exists a bijective substitution $\pi:FV(t_{1})\to FV(t_{2})$, s.t.
$\rho\circ mgu\,(t_{1}\rho,t_{2}\rho)=\delta\circ\rho^{\prime}\circ\pi$).

$\begin{array}[]{cccp{1cm}c}{\mathfrak{S}}^{\Upsilon}&=&\leavevmode\hbox
to37.29pt{\vbox to15.41pt{\pgfpicture\makeatletter\hbox{\hskip
18.64413pt\lower-5.24634pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.31113pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathcal{T}_{\mathcal{A}}\equiv\mathcal{T}_{\mathcal{A}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}&&\leavevmode\hbox
to69.44pt{\vbox to17.94pt{\pgfpicture\makeatletter\hbox{\hskip
34.71939pt\lower-5.83301pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.38638pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$R^{k}\,(\mathcal{T}_{\mathcal{A}},\,\dots,\,\mathcal{T}_{\mathcal{A}})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>&&\leavevmode\hbox to59.26pt{\vbox
to29.21pt{\pgfpicture\makeatletter\hbox{\hskip
29.62811pt\lower-27.70633pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}{{{{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.2951pt}{-24.37332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\mathfrak{S}}^{\Upsilon}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{{}}{}{{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{}{}{}{{
{\pgfsys@beginscope{} {}{}{} {} {}{}{}
\pgfsys@moveto{3.59995pt}{0.0pt}\pgfsys@curveto{2.53328pt}{0.2pt}{0.79999pt}{0.79999pt}{-0.4pt}{1.49997pt}\pgfsys@lineto{-0.4pt}{-1.49997pt}\pgfsys@curveto{0.79999pt}{-0.79999pt}{2.53328pt}{-0.2pt}{3.59995pt}{0.0pt}\pgfsys@fill\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{-10.27895pt}{-9.63213pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.72969}{-0.68378}{0.68378}{-0.72969}{-10.27893pt}{-9.63211pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.38402pt}{-24.37332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\mathfrak{S}}^{\Upsilon}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{{}}{}{{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{10.27899pt}{-9.63213pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.72969}{-0.68378}{0.68378}{0.72969}{10.27898pt}{-9.63211pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}&&\leavevmode\hbox
to48.86pt{\vbox to45.41pt{\pgfpicture\makeatletter\hbox{\hskip
18.64413pt\lower-37.70633pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.31113pt}{-2.45999pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathcal{T}_{\mathcal{A}}\equiv\mathcal{T}_{\mathcal{A}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.95557pt}{-34.37332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\mathfrak{S}}^{\Upsilon}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-7.90633pt}\pgfsys@lineto{0.0pt}{-18.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-18.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{-17.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\tiny{$\\{\mathcal{A}=\mathcal{T}_{\mathcal{A}}\\}$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>&&\lx@intercol\hfil\leavevmode\hbox to86.86pt{\vbox
to46.68pt{\pgfpicture\makeatletter\hbox{\hskip
34.71939pt\lower-37.70633pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.38638pt}{-3.13887pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$R^{k}\,(\mathcal{T}_{\mathcal{A}},\,\dots,\,\mathcal{T}_{\mathcal{A}})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.95557pt}{-34.37332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\mathfrak{S}}^{\Upsilon}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-9.17188pt}\pgfsys@lineto{0.0pt}{-18.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-18.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{-17.2022pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\tiny{$(\mathcal{T}_{\mathcal{A}},\dots,\mathcal{T}_{\mathcal{A}})\in\llbracket
R^{k}\rrbracket$}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\hfil\lx@intercol\end{array}$
Figure 6: Symbolic Scheme Forms

In our description of the extraction process, we use a visual representation
of symbolic execution of a relation body for a given set of grounded variables
in a form of a _symbolic scheme_. A symbolic scheme is a tree-like structure
with different branches corresponding to execution of different disjuncts and
nodes corresponding to equalities and relational calls in the body augmented
with subsets of grounded variables at the point of execution.444Note the
difference with conventional symbolic execution graphs with different branches
representing mutually exclusive paths of evaluation, not the different parts
within one evaluation. Constraints for substituted grounded variables that
determine whether the execution continues are presented as labels on the edges
of a scheme.

Each scheme is built as a composition of the five patterns, shown in Fig. 6
(all schemes are indexed by subsets of grounded variables with
$\Upsilon=2^{\mathcal{A}}$ denoting such subsets).

Note, the constraints after nodes of different types differ: unification puts
a constraint in a form of a set of equations on substituted ground values that
should be respected while relational call puts a constraint in a form of a
tuple of ground terms that should belong to the denotational semantics of a
relation.

The construction of a scheme for a given goal (initially, the body of a
relation) mimics a regular execution of a relational program. The derivation
rules for scheme formation have the following form
$\left<\Gamma,\,\sigma,\,n,\,V\right>\;\vdash\;g\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces{\mathfrak{S}}^{V}$.
Here $g$ is a goal, $\Gamma$ is a list of _deferred_ goals (these goals have
to be executed after the execution of $g$ in every branch in the same order,
initially this list is empty; this resembles continuations, but the analogy is
not complete), $\sigma$ and $n$ are substitution and counter from the current
environment respectively, $V$ is a set of grounded variables at the moment.

${\begin{array}[]{cr}\dfrac{\left<g_{2}:\Gamma,\,\sigma,\,n,\,V\right>\;\vdash\;g_{1}\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces{\mathfrak{S}}^{V}}{\left<\Gamma,\,\sigma,\,n,\,V\right>\;\vdash\;g_{1}\land
g_{2}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces{\mathfrak{S}}^{V}}&\mbox{[{Conj${}_{\mathfrak{S}}$}]}\\\\[14.22636pt]
\dfrac{\left<\Gamma,\,\sigma,\,n,\,V\right>\;\vdash\;g_{1}\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces{\mathfrak{S_{1}}}^{V},\;\left<\Gamma,\,\sigma,\,n,\,V\right>\;\vdash\;g_{2}\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces{\mathfrak{S_{2}}}^{V}}{\left<\Gamma,\,\sigma,\,n,\,V\right>\;\vdash\;g_{1}\lor
g_{2}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\parbox[m]{56.9055pt}{
\leavevmode\hbox to62.21pt{\vbox
to28.81pt{\pgfpicture\makeatletter\hbox{\hskip
31.10588pt\lower-28.60855pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}{{{{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-27.77287pt}{-23.4711pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\mathfrak{S_{1}}}^{V}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{{}}{}{{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{-9.31648pt}{-8.72995pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.7297}{-0.68376}{0.68376}{-0.7297}{-9.31647pt}{-8.72995pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.90625pt}{-23.4711pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\mathfrak{S_{2}}}^{V}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{{}}{}{{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.31653pt}{-8.72995pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7297}{-0.68376}{0.68376}{0.7297}{9.31651pt}{-8.72995pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\dfrac{\left<\Gamma,\,\sigma,\,n+1,\,V\right>\;\vdash\;g\,[{\raisebox{1.99997pt}{$\alpha_{n}$}\left/\raisebox{-1.99997pt}{$\mbox{{x}}$}\right.}]\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces{\mathfrak{S}}^{V}}{\left<\Gamma,\,\sigma,\,n,\,V\right>\;\vdash\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{{f}resh}}}}}}\,\mbox{{x}}\;.\;g\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces{\mathfrak{S}}^{V}}&\mbox{[{Fresh${}_{\mathfrak{S}}$}]}\\\\[14.22636pt]
\left<\epsilon,\,\sigma,\,n,\,V\right>\;\vdash\;t_{1}\equiv
t_{2}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\parbox[m]{56.9055pt}{
\leavevmode\hbox to44.25pt{\vbox
to14.62pt{\pgfpicture\makeatletter\hbox{\hskip 22.12486pt\lower-5.13745pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-18.79185pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t_{1}\sigma\equiv
t_{2}\sigma$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}
}&\mbox{[{UnifyLeaf${}_{\mathfrak{S}}$}]}\\\\[14.22636pt]
\left<\epsilon,\,\sigma,\,n,\,V\right>\;\vdash\;R^{k}\,(t_{1},\,\dots,\,t_{k})\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\parbox[m]{56.9055pt}{
\leavevmode\hbox to70.58pt{\vbox
to17.94pt{\pgfpicture\makeatletter\hbox{\hskip 35.29045pt\lower-5.83301pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.95744pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$R^{k}\,(t_{1}\sigma,\,\dots,\,t_{k}\sigma)$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}
}&\mbox{[{InvokeLeaf${}_{\mathfrak{S}}$}]}\\\\[14.22636pt] \dfrac{\nexists
mgu\,(t_{1}\sigma,t_{2}\sigma)}{\left<g:\Gamma,\,\sigma,\,n,\,V\right>\;\vdash\;t_{1}\equiv
t_{2}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\parbox[m]{56.9055pt}{
\leavevmode\hbox to44.25pt{\vbox
to14.62pt{\pgfpicture\makeatletter\hbox{\hskip 22.12486pt\lower-5.13745pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-18.79185pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t_{1}\sigma\equiv
t_{2}\sigma$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}
}}&\mbox{[{UnifyFail${}_{\mathfrak{S}}$}]}\\\\[14.22636pt]
\dfrac{mgu\,(t_{1}\sigma,t_{2}\sigma)=\delta,\;U=\mbox{{upd}}\,(V,\,\delta),\;\left<\Gamma,\,\sigma\delta,\,n,\,U\right>\;\vdash\;g\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces{\mathfrak{S}}^{U}}{\left<g:\Gamma,\,\sigma,\,n,\,V\right>\;\vdash\;t_{1}\equiv
t_{2}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\parbox[m]{56.9055pt}{
\leavevmode\hbox to58.55pt{\vbox
to45.02pt{\pgfpicture\makeatletter\hbox{\hskip
22.12486pt\lower-37.70633pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-18.79185pt}{-2.17317pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t_{1}\sigma\equiv
t_{2}\sigma$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.99483pt}{-34.37332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${\mathfrak{S}}^{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-7.51062pt}\pgfsys@lineto{0.0pt}{-18.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-18.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{-16.05214pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\tiny{$\mbox{{constr}}\,(\delta,\,U)$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\dfrac{\mbox{\phantom{XXXXXX}}U=V\cup\displaystyle\bigcup\limits_{i}FV\,(t_{i}\sigma),\;\left<\Gamma,\,\sigma,\,n,\,U\right>\;\vdash\;g\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces{\mathfrak{S}}^{U}\mbox{\phantom{XXXXXX}}}{\left<g:\Gamma,\,\sigma,\,n,\,V\right>\;\vdash\;R^{k}\,(t_{1},\,\dots,\,t_{k})\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\parbox[m]{56.9055pt}{
\leavevmode\hbox to89.67pt{\vbox
to46.68pt{\pgfpicture\makeatletter\hbox{\hskip
35.29045pt\lower-37.70633pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.95744pt}{-3.13887pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$R^{k}\,(t_{1}\sigma,\,\dots,\,t_{k}\sigma)$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.99483pt}{-34.37332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${\mathfrak{S}}^{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-9.17188pt}\pgfsys@lineto{0.0pt}{-18.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-18.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{-17.2022pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\tiny{$(t_{1}\sigma,\dots,t_{k}\sigma)\in\llbracket
R^{k}\rrbracket$}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}&\mbox{[{Invoke${}_{\mathfrak{S}}$}]}\end{array}$
Figure 7: Scheme Formation Rules

The rules are shown in Fig. 7. [ConjS] and [DisjS] are structural rules: when
investigating conjunctions we defer the second conjunct by adding it to
$\Gamma$ and continue with the first conjunct; disjunctions simply result in
forks. [FreshS] introduces a fresh logic variable (not grounded) and updates
the counter of occupied variables. When the investigated goal is equality or
relational call it is added as a node to the scheme. If there are no deferred
goals, then this node is a leaf (rules [UnifyLeafS] and [InvokeLeafS]).
Equality is also added as a leaf if there are some deferred goals, but the
terms are non-unifiable and so the execution stops (rule [UnifyFailS]). If the
terms in the equality are unifiable and there are deferred goals (rule
[UnifySuccessS]), the equality is added as a node and the execution continues
for the deferred goals, starting from the leftmost one; also the set of
grounded variables is updated and constraint labels are added for the edge in
accordance with Lem. LABEL:lem:symbolic_unification_soundness. For relational
calls the proccess is similar: if there are some deferred goals (rule
[InvokeS]), all variables occurring in a call become grounded (due to the
grounding condition we imposed) and should satisfy the denotational semantics
of the invoked relation.

The scheme constructed by these rules for our appendo example is shown in Fig.
8. For simplicity, we do not show the set of grounded variables for each node,
but instead overline grounded variables in-place. Note, all variables that
occur in constraints on the edges are grounded after parent node execution.

Now, we can use schemes to see how the information for leaf goals in relation
body is combined with conjunctions and disjunctions. Then we can apply
formulae from Section 3 to get recursive inequalities (providing lower and
upper bounds simultaneously) for both complexity factors.

In these inequalities we need to sum up the values of $d$ and $t$-factor for
all leaf goals of a body and for all environments these goals are evaluated
for. The leaf goals are the nodes of the scheme and evaluated environments can
be derived from the constraints attached to the edges. So, for this summation
we introduce the following notions: $\mathcal{D}$ is the sum of $d$-factor
values and $\mathcal{T}$ is the sum of $t$-factor values for the execution of
the body with specific valuation $\rho$.

$\overline{a}\equiv\texttt{Nil}$$ab\equiv\overline{b}$${a}=\texttt{Nil}$$\overline{a}\equiv\texttt{Cons($h$,
$t$)}$appendo $\overline{t}$ $\overline{b}$
$tb$$ab\equiv\texttt{Cons($\overline{h}$,
$\overline{tb}$)}$$({t},{b},{tb})\in\llbracket\texttt{append${}^{o}$}\rrbracket$${a}=\texttt{Cons(${h}$,
${t}$)}$ Figure 8: Symbolic execution scheme for the goal appendo $\,a\;$
$b\;$ $ab$ with initial set of grounded variables $V=\\{a,b\\}$. For each
node, variables that are grounded at the point of execution of this node are
overlined.

Their definitions are shown in Fig. 9 (both formulas are given in the same
figure as the definitions coincide modulo factor denotations). For nodes, we
take the corresponding value (for equality it always equals $1$). When going
through an equality we sum up the rest with an updated valuation (by Lem.
LABEL:lem:symbolic_unification_soundness this sum always has one or zero
summands depending on whether the unification succeeds or not). When going
through a relational call we take a sum of all valuations that satisfy the
denotational semantics (these valuations will correspond exactly to the set of
all answers produced by the call since operational semantics is sound and
complete w.r.t. the denotational one and because we require all answers to be
unique). For disjunctions, we take the sum of both branches.

$\begin{array}[]{rclcl}\mathcal{\nicefrac{{D}}{{T}}}\,(&\parbox[m]{36.98866pt}{
\leavevmode\hbox to30.04pt{\vbox
to14.62pt{\pgfpicture\makeatletter\hbox{\hskip 15.02188pt\lower-5.13745pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.68887pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t_{2}\equiv t_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }&)(\rho)&=&1\\\
\mathcal{\nicefrac{{D}}{{T}}}\,(&\parbox[m]{71.13188pt}{ \leavevmode\hbox
to59.71pt{\vbox to17.94pt{\pgfpicture\makeatletter\hbox{\hskip
29.85411pt\lower-5.83301pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.5211pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$R^{k}\,(t_{1},\,\dots,\,t_{k})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}
}&)(\rho)&=&\nicefrac{{d}}{{t}}\,(init\,(R^{k}\,(t_{1}\rho,\,\dots,\,t_{k}\rho)))\\\
\mathcal{\nicefrac{{D}}{{T}}}\,(&\parbox[m]{56.9055pt}{ \leavevmode\hbox
to30.04pt{\vbox to45.02pt{\pgfpicture\makeatletter\hbox{\hskip
15.02188pt\lower-37.70633pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.68887pt}{-2.17317pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t_{1}\equiv t_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.99483pt}{-34.37332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${\mathfrak{S}}^{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-7.51062pt}\pgfsys@lineto{0.0pt}{-18.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-18.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{-16.51047pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\tiny{$Cs$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}&)(\rho)&=&1+\smashoperator[]{\sum_{\begin{subarray}{c}\rho^{\prime}\colon
V\to\mathcal{T}_{\varnothing}\\\ \rho^{\prime}\succ\rho\\\ \forall(y,t)\in
Cs\,:\,\rho^{\prime}\,(y)=t\,\rho^{\prime}\end{subarray}}^{}}\mathcal{\nicefrac{{D}}{{T}}}\,({\mathfrak{S}}^{U})(\rho^{\prime})\\\
\mathcal{\nicefrac{{D}}{{T}}}\,(&\parbox[m]{113.81102pt}{ \leavevmode\hbox
to80.46pt{\vbox to46.68pt{\pgfpicture\makeatletter\hbox{\hskip
29.85411pt\lower-37.70633pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.5211pt}{-3.13887pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$R^{k}\,(t_{1},\,\dots,\,t_{k})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.99483pt}{-34.37332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${\mathfrak{S}}^{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-9.17188pt}\pgfsys@lineto{0.0pt}{-18.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-18.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{-17.2022pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\tiny{
$(t_{1},\dots,t_{k})\in\llbracket R^{k}\rrbracket$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}&)(\rho)&=&\nicefrac{{d}}{{t}}\,(init\,(R^{k}\,(t_{1}\rho,\,\dots,\,t_{k}\rho)))+\smashoperator[]{\sum_{\begin{subarray}{c}\rho^{\prime}\colon
V\to\mathcal{T}_{\varnothing}\\\ \rho^{\prime}\succ\rho\\\
(t_{1}\rho^{\prime},\dots,t_{k}\rho^{\prime})\in\llbracket
R^{k}\rrbracket\end{subarray}}^{}}\mathcal{\nicefrac{{D}}{{T}}}\,({\mathfrak{S}}^{U})(\rho^{\prime})\\\
\mathcal{\nicefrac{{D}}{{T}}}\,(&\parbox[m]{71.13188pt}{ \leavevmode\hbox
to62.21pt{\vbox to28.81pt{\pgfpicture\makeatletter\hbox{\hskip
31.10588pt\lower-28.60855pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}{{{{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-27.77287pt}{-23.4711pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\mathfrak{S}_{1}}^{V}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{{}}{}{{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{-9.31648pt}{-8.72995pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.7297}{-0.68376}{0.68376}{-0.7297}{-9.31647pt}{-8.72995pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.90625pt}{-23.4711pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\mathfrak{S}_{2}}^{V}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{{}}{}{{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.31653pt}{-8.72995pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7297}{-0.68376}{0.68376}{0.7297}{9.31651pt}{-8.72995pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}&)(\rho)&=&\mathcal{\nicefrac{{D}}{{T}}}\,({\mathfrak{S}_{1}}^{V})(\rho)+\mathcal{\nicefrac{{D}}{{T}}}\,({\mathfrak{S}_{2}}^{V})(\rho)\end{array}$
Figure 9: Complexity Factors Extraction: $\mathcal{D}$ and $\mathcal{T}$
$\begin{array}[]{rclcl}\mathcal{L}\,(&\parbox[m]{36.98866pt}{ \leavevmode\hbox
to30.04pt{\vbox to14.62pt{\pgfpicture\makeatletter\hbox{\hskip
15.02188pt\lower-5.13745pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.68887pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t_{2}\equiv t_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}
}&)(\rho)&=&\\{init\,(t_{2}\equiv t_{2})\\}\\\
\mathcal{L}\,(&\parbox[m]{71.13188pt}{ \leavevmode\hbox to59.71pt{\vbox
to17.94pt{\pgfpicture\makeatletter\hbox{\hskip 29.85411pt\lower-5.83301pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.5211pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$R^{k}\,(t_{1},\,\dots,\,t_{k})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}
}&)(\rho)&=&\\{init\,(R^{k}\,(t_{1}\rho,\,\dots,\,t_{k}\rho))\\}\\\
\mathcal{L}\,(&\parbox[m]{56.9055pt}{ \leavevmode\hbox to30.04pt{\vbox
to45.02pt{\pgfpicture\makeatletter\hbox{\hskip
15.02188pt\lower-37.70633pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.68887pt}{-2.17317pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t_{1}\equiv t_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.99483pt}{-34.37332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${\mathfrak{S}}^{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-7.51062pt}\pgfsys@lineto{0.0pt}{-18.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-18.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{-16.51047pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\tiny{$Cs$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}&)(\rho)&=&\smashoperator[]{\bigcup_{\begin{subarray}{c}\rho^{\prime}\colon
V\to\mathcal{T}_{\varnothing}\\\ \rho^{\prime}\succ\rho\\\ \forall(y,t)\in
Cs\,:\,\rho^{\prime}\,(y)=t\,\rho^{\prime}\end{subarray}}^{}}\mathcal{L}\,({\mathfrak{S}}^{U})(\rho^{\prime})\\\
\mathcal{L}\,(&\parbox[m]{113.81102pt}{ \leavevmode\hbox to80.46pt{\vbox
to46.68pt{\pgfpicture\makeatletter\hbox{\hskip
29.85411pt\lower-37.70633pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.5211pt}{-3.13887pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$R^{k}\,(t_{1},\,\dots,\,t_{k})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.99483pt}{-34.37332pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${\mathfrak{S}}^{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-9.17188pt}\pgfsys@lineto{0.0pt}{-18.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-18.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{-17.2022pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\tiny{
$(t_{1},\dots,t_{k})\in\llbracket R^{k}\rrbracket$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}&)(\rho)&=&\smashoperator[]{\bigcup_{\begin{subarray}{c}\rho^{\prime}\colon
V\to\mathcal{T}_{\varnothing}\\\ \rho^{\prime}\succ\rho\\\
(t_{1}\rho^{\prime},\dots,t_{k}\rho^{\prime})\in\llbracket
R^{k}\rrbracket\end{subarray}}^{}}\mathcal{L}\,({\mathfrak{S}}^{U})(\rho^{\prime})\\\
\mathcal{L}\,(&\parbox[m]{71.13188pt}{ \leavevmode\hbox to62.21pt{\vbox
to28.81pt{\pgfpicture\makeatletter\hbox{\hskip
31.10588pt\lower-28.60855pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}{{{{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-27.77287pt}{-23.4711pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\mathfrak{S}_{1}}^{V}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{{}}{}{{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{-9.31648pt}{-8.72995pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.7297}{-0.68376}{0.68376}{-0.7297}{-9.31647pt}{-8.72995pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.90625pt}{-23.4711pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\mathfrak{S}_{2}}^{V}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{{}}{}{{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.31653pt}{-8.72995pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7297}{-0.68376}{0.68376}{0.7297}{9.31651pt}{-8.72995pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}&)(\rho)&=&\mathcal{L}\,({\mathfrak{S}_{1}}^{V})(\rho)\cup\mathcal{L}\,({\mathfrak{S}_{2}}^{V})(\rho)\end{array}$
Figure 10: Complexity Factors Extraction: $\mathcal{L}$

As we saw in Section 3 when computing the scheduling factors we need to
exclude from the additional cost the value of $d$-factor for one of the
environments (the largest one). This is true for the generalized formula for a
whole scheme, too. This time we need to take all executed environments for all
the leaves of a scheme and exclude the $d$-factor value for a maximal one (the
formula for conjunction ensures that we make the exclusion for the leaf, and
the formula for disjunction ensures that we make it for only one of the
leaves). So, we will need additional notion $\mathcal{L}$, similar to
$\mathcal{D}$ and $\mathcal{T}$ that will collect all the goals of the form
$init\,(g_{i}\rho)$, where $g_{i}$ is a leaf goal and $\rho$ is a valuation
corresponding to one of the environments this leaf is evaluated for. The
definition of $\mathcal{L}$ is shown in Fig. 10.

Now we can formulate the following main theorem that provides the principal
recursive inequalities, extracted from the scheme for a given goal.

extracted_approximations Let $g$ be a goal, and let
$\left<\epsilon,\,\varepsilon,\,n_{init}(g),\,V\right>\;\vdash\;g\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
17.22636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces{\mathfrak{S}}^{V}$.
Then

$\begin{array}[]{rcl}d\,(init\,(g\,\rho))&=&\mathcal{D}\,({\mathfrak{S}}^{V})(\rho)+\Theta\,(1)\\\
t\,(init\,(g\,\rho))&=&\mathcal{T}\,({\mathfrak{S}}^{V})(\rho)+\Theta\,(\mathcal{D}\,({\mathfrak{S}}^{V})(\rho)-\smashoperator[]{\max^{\bullet}_{\langle
g_{i},\,e_{i}\rangle\in\mathcal{L}({\mathfrak{S}}^{V})(\rho)}^{}}d\,(\langle
g_{i},\,e_{i}\rangle)+1)\end{array}$

being considered as functions on $\rho\colon V\to T_{\varnothing}$

The theorem allows us to extract two inequalities (upper and lower bounds) for
both factors with a multiplicative constant that is the same for all
valuations.

For our example, we can extract the following recursive inequalities from the
scheme in Fig. 8. For presentation purposes, we will not show valuation in
inequalities explicitly, but instead show the ground values of grounded
variables (using variables in bold font) that determine each valuation. We can
do such a simplification for any concrete relation.

$d\,(q^{app}\,(\mathbf{a},\mathbf{b}))=(1+\sum\limits_{\mathbf{a}=\texttt{Nil}}1)+(1+\smashoperator[]{\sum_{\mathbf{h},\mathbf{t}:\mathbf{a}=\texttt{Cons($\mathbf{h}$,
$\mathbf{t}$)}}^{}}(d\,(q^{app}\,(\mathbf{t},\mathbf{b}))+\smashoperator[]{\sum_{\mathbf{tb}:(\mathbf{t},\mathbf{b},\mathbf{tb})\in\llbracket\texttt{append${}^{o}$}\rrbracket}^{}}1))+\Theta\,(1)$
$\begin{array}[]{lclc}t\,(q^{app}\,(\mathbf{a},\mathbf{b}))&=&(1+\sum\limits_{\mathbf{a}=\texttt{Nil}}1)+(1+\smashoperator[]{\sum_{\mathbf{h},\mathbf{t}:\mathbf{a}=\texttt{Cons($\mathbf{h}$,
$\mathbf{t}$)}}^{}}(t\,(q^{app}\,(\mathbf{t},\mathbf{b}))+\smashoperator[]{\sum_{\mathbf{tb}:(\mathbf{t},\mathbf{b},\mathbf{tb})\in\llbracket\texttt{append${}^{o}$}\rrbracket}^{}}1))&+\\\
&&\Theta((1+\sum\limits_{\mathbf{a}=\texttt{Nil}}1)+(1+\smashoperator[]{\sum_{\mathbf{h},\mathbf{t}:\mathbf{a}=\texttt{Cons($\mathbf{h}$,
$\mathbf{t}$)}}^{}}(d\,(q^{app}\,(\mathbf{t},\mathbf{b}))+\smashoperator[]{\sum_{\mathbf{tb}:(\mathbf{t},\mathbf{b},\mathbf{tb})\in\llbracket\texttt{append${}^{o}$}\rrbracket}^{}}1))&-\\\
&&\smashoperator[]{\max^{\bullet}_{\begin{subarray}{c}\mathbf{h},\mathbf{t},\mathbf{tb}:\mathbf{a}=\texttt{Cons($\mathbf{h}$,
$\mathbf{t}$)}\land\\\
(\mathbf{t},\mathbf{b},\mathbf{tb})\in\llbracket\texttt{append${}^{o}$}\rrbracket\end{subarray}}^{}}\\{d\,(init\,(ab\equiv\mathbf{b})),d\,(init\,(ab\equiv\texttt{Cons($\mathbf{h}$,
$\mathbf{tb}$)}))\\}&+1)\end{array}$

Automatically extracted recursive inequalities, as a rule, are cumbersome, but
they contain all the information on how scheduling affects the complexity.
Often they can be drastically simplified by using metatheory-level reasoning.

For our example, we are only interested in the case when substituted values
represent some lists. We thus perform the usual for lists case analysis
considering the first list empty or non-empty. We can also notice that the
excluded summand equals one. So we can rewrite the inequalities in the
following way:

$\begin{array}[]{lcl}d\,(q^{app}\,(\texttt{Nil},\mathbf{b}))&=&\Theta\,(1)\\\
d\,(q^{app}\,(\texttt{Cons($\mathbf{h}$,
$\mathbf{t}$)},\mathbf{b}))&=&d\,(q^{app}\,(\mathbf{t},\mathbf{b}))+\Theta\,(1)\\\
t\,(q^{app}\,(\texttt{Nil},\mathbf{b}))&=&\Theta\,(1)\\\
t\,(q^{app}\,(\texttt{Cons($\mathbf{h}$,
$\mathbf{t}$)},\mathbf{b}))&=&t\,(q^{app}\,(\mathbf{t},\mathbf{b}))+\Theta\,(d\,(q^{app}\,(\mathbf{t},\mathbf{b})))\\\
\end{array}$

These trivial linear inequalities can be easily solved:

$\begin{array}[]{lcl}d\,(q^{app}\,(\mathbf{a},\mathbf{b}))&=&\Theta\,(len\,(\mathbf{a}))\\\
t\,(q^{app}\,(\mathbf{a},\mathbf{b}))&=&\Theta\,(len^{2}\,(\mathbf{a}))\\\
\end{array}$

In this case, scheduling makes a big difference and changes the asymptotics.
Note, we expressed the result using notions from metatheory ($len$ for the
length of the list represented by a term).

In contrast, if we consider the optimal definition append${}_{opt}^{o}$ the
analysis of the call
$q^{app\text{-}opt}\,(\mathbf{a},\mathbf{b})=init\,(\texttt{append${}_{opt}^{o}$}\,\mathbf{a}\,\mathbf{b}\,ab)$
is analogous, but among the candidates for exclusion there is the value
$d\,(q^{app\text{-}opt}\,(\mathbf{t},\mathbf{b}))$ since the recursive call is
placed in a leaf. So the last simplified recursive approximation is the
following (the rest is the same as in our main example):

$t\,(q^{app\text{-}opt}\,(\texttt{Cons\,($\mathbf{h}$,
$\mathbf{t}$)},\mathbf{b}))=t\,(q^{app\text{-}opt}\,(\mathbf{t},\mathbf{b}))+\Theta\,(1)$

So in this case the complexity of both factors is linear on
$len\,(\mathbf{a})$.

##  5 Evaluation

The theory we have built was so far applied to only one relation — appendo —
which we used as a motivating example. With our framework, it turned out to be
possible to explain the difference in performance between two nearly identical
implementations, and the difference — linear vs. quadratic asymptotic
complexity — was just as expected from the experimental performance
evaluation. In this section, we present some other results of complexity
estimations and discuss the adequacy of these estimations w.r.t. the real
miniKanren implementations.

Derived complexity estimations for a few other relations are shown in Fig. 11.
Besides concatenation, we deal with naive list reversing and Peano numbers
addition and multiplication. We show both $d-$ and $t-$ factors since the
difference between the two indicates the cases when scheduling strikes in. We
expect that for simple relations like those presented the procedure of
deriving estimations should be easy; however, for more complex ones the
dealing with extracted inequalities may involve a non-trivial metatheory
reasoning.

The justification of the adequacy of our complexity estimations w.r.t. the
existing miniKanren implementations faces the following problem: it is not an
easy task to separate the contribution of scheduling from other components of
the search procedure — unification and occurs check. However, it is common
knowledge among Prolog users that in practice unification takes a constant
time almost always; some theoretical basis for this is given in [1]. There are
some specifics of unification implementation in miniKanren. First, for the
simplicity of backtracking in a non-mutable fashion triangular substitution
[3] is used instead of the idempotent one. It brings in an additional overhead
which is analyzed in some detail in [4], but the experience shows that in the
majority of practical cases this overhead is insignificant. Second, miniKanren
by default performs the “occurs check”, which contributes a significant
overhead and often subsumes the complexity of all other search components.
Meanwhile, it is known, that occurs checks are rarely violated [2]. Having
said this, we expect that in the majority of the cases the performance of
miniKanren programs with the occurs check disabled are described by scheduling
complexity alone. In particular, this is true for all cases in Fig. 11. To
confirm the adequacy of our model we evaluated the running time of these and
some other goals (under the conditions we’ve mentioned) and found that it
confirms the estimations derived using our framework. The details of
implementation, evaluation, and results can be found in an accompanying
repository.
555https://www.dropbox.com/sh/ciceovnogkeeibz/AAAoclpTSDeY3OMagOBJHNiSa?dl=0

| $d$ | $t$ |  | $d$ | $t$
---|---|---|---|---|---
appendo $\mathbf{a}$ $\mathbf{b}$ ${ab}$ | $len\,(\mathbf{a})$ | $len^{2}\,(\mathbf{a})$ | pluso $\mathbf{n}$ $\mathbf{m}$ ${r}$ | $|\mathbf{n}|$ | $|\mathbf{n}|$
append${}_{opt}^{o}$ $\mathbf{a}$ $\mathbf{b}$ ${ab}$ | $len\,(\mathbf{a})$ | $len\,(\mathbf{a})$ | pluso $\mathbf{n}$ ${m}$ $\mathbf{r}$ | $\min\,\\{|\mathbf{n}|,|\mathbf{r}|\\}$ | $\min\,\\{|\mathbf{n}|,|\mathbf{r}|\\}$
append${}_{opt}^{o}$ ${a}$ ${b}$ $\mathbf{ab}$ | $len\,(\mathbf{ab})$ | $len\,(\mathbf{ab})$ | pluso ${n}$ ${m}$ $\mathbf{r}$ | $|\mathbf{r}|$ | $|\mathbf{r}|$
reverso $\mathbf{a}$ ${r}$ | $len^{2}\,(\mathbf{a})$ | $len^{3}\,(\mathbf{a})$ | multo $\mathbf{n}$ $\mathbf{m}$ ${r}$ | $|\mathbf{n}|\cdot|\mathbf{m}|$ | $|\mathbf{n}|^{2}\cdot|\mathbf{m}|$
reverso ${a}$ $\mathbf{r}$ | $len^{2}\,(\mathbf{r})$ | $len^{2}\,(\mathbf{r})$ | multo (S ${n}$) (S ${m}$) $\mathbf{r}$ | $|\mathbf{r}|^{2}$ | $|\mathbf{r}|^{2}$
Figure 11: Derived $d$\- and $t$-factors for some goals; $len\,(\bullet)$
stands for the length of a ground list, $|\bullet|$ — for the value of a Peano
number, represented as ground term.

##  6 Related Work

To our knowledge, our work is the first attempt of comprehensive time
complexity analysis for interleaving search in miniKanren. There is a number
of separate observations on how certain patterns in relational programming
affect performance and a number of “rules of thumb” based on these
observations [4]. Some papers [9, 16, 12] tackle specific problems with
relational programming using quantitative time measuring for evaluation. These
approaches to performance analysis, being sufficient for specific relational
problems, do not provide the general understanding of interleaving search and
its cost.

At the same time complexity analysis was studied extensively in the broader
context of logic programming (primarily, for Prolog). As one important
motivation for complexity analysis is granularity control in parallel
execution, the main focus was set on the automated approaches.

Probably the best known among them is the framework [7] for cost analysis of
logic programs (demonstrated on plain Prolog), implemented in the system
CASLOG. It uses data dependency information to estimate the sizes of the
arguments and the number of solutions for executed atoms. These estimations
are formulated as recursive inequalities (more precisely, as difference
equations for upper bounds), which are then automatically solved with known
methods. The time and space complexity are expressed using these estimations,
the variations of this approach can provide both upper [7] and lower [8]
bounds.

An alternative approach is suggested in [11] for symbolic analysis of logic
programs (demonstrated in Prolog with cuts). It constructs symbolic evaluation
graphs capturing grounding propagation and reduction of recursive calls to
previous ones, in the process of construction some heuristic approximations
are used. These graphs may look similar to the symbolic schemes described in
the Section 4 at first glance, but there is a principal difference: symbolic
graphs capture the whole execution with all invoked calls (using inverse edges
to represent cycles with recursive calls), while our schemes capture only the
execution inside the body of a specific relation (representing the information
about internal calls in terms of denotational semantics). The graphs are then
transformed into term rewriting systems, for which the problem of the
complexity analysis is well-studied (specifically, AProVE tool is used).

While these two approaches can be seen as partial bases for our technique,
they are mainly focused on how the information about the arguments and results
of the evaluated clauses can be derived automatically, since the calculation
of time complexity of SLD-resolution is trivial when this information is
available. In contrast, we are interested in the penalty of non-trivial
scheduling of relational calls under interleaving search, so we delegate
handling the information about calls to the reasoning in terms of a specific
metatheory.

##  7 Discussion and Future Work

The formal framework presented in this paper analyzes the basic aspects of
scheduling cost for interleaving search strategy from the theoretical
viewpoint. As we have shown, it is sufficiently powerful to explain some
surprising asymptotic behaviour for simple standard programs in miniKanren,
but the applicability of this framework in practice for real implementations
of miniKanren requires further investigation. Two key aspects that determine
practical applicability are the admissibility of the imposed requirements and
the correspondence of specific miniKanren implementations to the reference
operational semantics, which should be studied individually for each
application. We see our work as the ground for the future development of
methods for analyzing the cost of interleaving search.

Our approach imposes three requirements on the analyzed programs: disjunctive
normal form, uniqueness of answers, and grounding of relational calls. The
first two are rather non-restrictive: DNF is equivalent to the description of
relation as a set of Horn clauses in Prolog, and the majority of well-known
examples in miniKanren are written in this or very similar form. Repetition of
answers is usually an indication of a mistake in a program [4]. The groundness
condition is more serious: it prohibits program execution from presenting
infinitely many individual ground solutions in one answer using free
variables, which is a useful pattern. At the same time, this requirement is
not unique for our work (the framework for CASLOG system mentioned above
imposes exactly the same condition) and the experience shows that many
important kinds of programs satisfy it (although it is hard to characterize
the class of such programs precisely). Relaxing any of these restrictions will
likely mess up the current relatively compact description of symbolic
execution (for the conditions on relational calls) or the form of the
extracted inequalities (for the DNF condition).

Also, for now, we confine ourselves to the problem of estimating the time of
the full search for a given goal. Estimating the time before the first (or
some specific) answer is believed to be an important and probably more
practical task. Unfortunately, the technique we describe can not be easily
adjusted for this case. The reason for this is that the reasoning about time
(scheduling time in particular) in our terms becomes non-compositional for the
case of interrupted search: if an answer is found in some branch, the search
is cut short in other branches, too. Dealing with such a non-compositionality
is a subject of future research.

## References

  * [1] Albert, L., Casas, R., Fages, F.: Average-case analysis of unification algorithms. Theor. Comput. Sci. 113(1), 3–34 (1993). https://doi.org/10.1016/0304-3975(93)90208-B, https://doi.org/10.1016/0304-3975(93)90208-B
  * [2] Apt, K.R., Pellegrini, A.: Why the occur-check is not a problem. In: Bruynooghe, M., Wirsing, M. (eds.) Programming Language Implementation and Logic Programming, 4th International Symposium, PLILP’92, Leuven, Belgium, August 26-28, 1992, Proceedings. Lecture Notes in Computer Science, vol. 631, pp. 69–86. Springer (1992). https://doi.org/10.1007/3-540-55844-6_128, https://doi.org/10.1007/3-540-55844-6_128
  * [3] Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 445–532. Elsevier and MIT Press (2001). https://doi.org/10.1016/b978-044450813-3/50010-2, https://doi.org/10.1016/b978-044450813-3/50010-2
  * [4] Byrd, W.E.: Relational Programming in Minikanren: Techniques, Applications, and Implementations. Ph.D. thesis, USA (2009)
  * [5] Byrd, W.E., Ballantyne, A., Rosenblatt, G., Might, M.: A unified approach to solving seven programming problems (functional pearl). Proc. ACM Program. Lang. 1(ICFP), 8:1–8:26 (2017). https://doi.org/10.1145/3110252, https://doi.org/10.1145/3110252
  * [6] Byrd, W.E., Holk, E., Friedman, D.P.: miniKanren, live and untagged: quine generation via relational interpreters (programming pearl). In: Danvy, O. (ed.) Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming, Scheme 2012, Copenhagen, Denmark, September 9-15, 2012. pp. 8–29. ACM (2012). https://doi.org/10.1145/2661103.2661105, https://doi.org/10.1145/2661103.2661105
  * [7] Debray, S.K., Lin, N.: Cost analysis of logic programs. ACM Trans. Program. Lang. Syst. 15(5), 826–875 (1993). https://doi.org/10.1145/161468.161472, https://doi.org/10.1145/161468.161472
  * [8] Debray, S.K., López-García, P., Hermenegildo, M.V., Lin, N.: Lower bound cost estimation for logic programs. In: Maluszynski, J. (ed.) Logic Programming, Proceedings of the 1997 International Symposium, Port Jefferson, Long Island, NY, USA, October 13-16, 1997. pp. 291–305. MIT Press (1997)
  * [9] Donahue, E.: Guarded Fresh Goals: Dependency-Directed Introduction of Fresh Logic Variables. In: third miniKanren and Relational Programming Workshop (2021)
  * [10] Friedman, D.P., Byrd, W.E., Kiselyov, O.: The reasoned schemer. MIT Press (2005)
  * [11] Giesl, J., Ströder, T., Schneider-Kamp, P., Emmes, F., Fuhs, C.: Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs. In: Schreye, D.D., Janssens, G., King, A. (eds.) Principles and Practice of Declarative Programming, PPDP’12, Leuven, Belgium \- September 19 - 21, 2012. pp. 1–12. ACM (2012). https://doi.org/10.1145/2370776.2370778, https://doi.org/10.1145/2370776.2370778
  * [12] Jin, E., Rosenblatt, G., Might, M., Zhang, L.: Universal Quantification and Implication in miniKanren. In: third miniKanren and Relational Programming Workshop (2021)
  * [13] Kiselyov, O., Shan, C., Friedman, D.P., Sabry, A.: Backtracking, interleaving, and terminating monad transformers: (functional pearl). In: Danvy, O., Pierce, B.C. (eds.) Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005. pp. 192–203. ACM (2005). https://doi.org/10.1145/1086365.1086390, https://doi.org/10.1145/1086365.1086390
  * [14] Kosarev, D., Lozov, P., Boulytchev, D.: Relational synthesis for pattern matching. In: d. S. Oliveira, B.C. (ed.) Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12470, pp. 293–310. Springer (2020). https://doi.org/10.1007/978-3-030-64437-6_15, https://doi.org/10.1007/978-3-030-64437-6_15
  * [15] Rozplokhas, D., Vyatkin, A., Boulytchev, D.: Certified semantics for relational programming. In: d. S. Oliveira, B.C. (ed.) Programming Languages and Systems \- 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12470, pp. 167–185. Springer (2020). https://doi.org/10.1007/978-3-030-64437-6_9, https://doi.org/10.1007/978-3-030-64437-6_9
  * [16] Sandre, L., Zaidi, M., Zhang, L.: Relational Floating-Point Arithmetic. In: third miniKanren and Relational Programming Workshop (2021)

##  Appendix 0.A Proofs

###### Lemma 0.A.1

Let $C_{f}$ and $C_{g}$ be real positive constants. If

$h\,(x)=f\,(x)+C_{f}+\Theta\,(g\,(x)+C_{g})$

and value $g\,(x)$ is positive for arbitrary $x$ then

$h\,(x)=f\,(x)+\Theta\,(g\,(x))$

###### Proof

  1. 1.

For some real postive $C_{1}$: $h\,(x)\geq
f\,(x)+C_{f}+C_{1}\cdot(g\,(x)+C_{g})$, thus $h\,(x)\geq f\,(x)+C_{1}\cdot
g\,(x)$

  2. 2.

For some real postive $C_{2}$: $h\,(x)\leq
f\,(x)+C_{f}+C_{2}\cdot(g\,(x)+C_{g})$, thus $h\,(x)\geq
f\,(x)+(C_{f}+C_{2}+C_{2}\cdot C_{g})\cdot g\,(x)$ ∎

###### Lemma 0.A.2

If

$h_{1}\,(x)=f_{1}\,(x)+\Theta\,(g_{1}\,(x))$

and

$h_{2}\,(x)=f_{2}\,(x)+\Theta\,(g_{2}\,(x))$

then

$(h_{1}\,(x)+h_{2}\,(x))=(f_{1}\,(x)+f_{2}\,(x))+\Theta\,(g_{1}\,(x)+g_{2}\,(x))$

###### Proof

Both lower- and upper-bound constants are the sums of the two corresponding
constants for the given approximations. ∎

###### Lemma 0.A.3

Let $g_{1}\,(x)\geq g_{2}\,(x)>0$ for all $x$. If

$h\,(x)=f\,(x)+\Theta\,(g_{1}\,(x)+g_{2}\,(x))$

then

$h\,(x)=f\,(x)+\Theta\,(g_{1}\,(x))$

###### Proof

  1. 1.

For some real postive $C_{1}$:

$h\,(x)\geq f\,(x)+C_{1}\cdot(g_{1}\,(x)+g_{2}\,(x))\geq f\,(x)+C_{1}\cdot
g_{1}\,(x)$

  2. 2.

For some real postive $C_{2}$:

$h\,(x)\leq f\,(x)+C_{2}\cdot(g_{1}\,(x)+g_{2}\,(x))\leq f\,(x)+2C_{2}\cdot
g_{1}\,(x)$

∎

###### Lemma 0.A.4

If

$\langle g,\,e\rangle\xrightarrow{l}s^{\prime}$

then

$\begin{array}[]{rcl}d\,(\langle g,\,e\rangle)&=&d\,(s^{\prime})+1\\\
t\,(\langle g,\,e\rangle)&=&t\,(s^{\prime})+1\end{array}$

###### Proof

Immediately from the definitions of the estimated values. ∎

###### Lemma LABEL:lem:sum_measure_equations

###### Proof

Induction on the sum of values $d\,(s_{1})+d\,(s_{2})$. Both equations easily
hold for both the rules [DisjStop] and [DisjStep] if we apply the inductive
hypothesis for the next state. ∎

###### Lemma LABEL:lem:times_measure_equations

###### Proof

Induction on the value $d\,(s\times g)$. Both equations easily hold for all
the rules [ConjStop], [ConjStopAns], [ConjStep], [ConjStepAns] if we apply the
inductive hypothesis for the next state. ∎

###### Lemma LABEL:lem:otimes_t_approximation

###### Proof

After unfolding the defintions and throwing out the identical parts we have
the following statement:

$\begin{array}[]{l}d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}\min\,\\{2\cdot
d\,(\langle g,\,a_{i}\rangle)-1,2\cdot d\,(s^{\prime}_{i}\otimes g)\\}=\\\
=\Theta\,(d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)-\smashoperator[]{\max^{\bullet}_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle))\\\ \end{array}$

If $\mathcal{T}r^{ans}(s)$ is empty, the statement is trivial.

If $\mathcal{T}r^{ans}(s)$ is not empty, $\displaystyle{\max^{\bullet}}$ turns
into a simple $\max$. We establish lower and upper bounds separately.

  1. 1.

Lower bound. Let’s show that

$\begin{array}[]{l}d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}\min\,\\{2\cdot
d\,(\langle g,\,a_{i}\rangle)-1,2\cdot d\,(s^{\prime}_{i}\otimes g)\\}\geq\\\
\geq
d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)-\smashoperator[]{\max_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)\\\ \end{array}$

First, we can decrease both arguments of $\min$:

$\begin{array}[]{l}d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}\min\,\\{2\cdot
d\,(\langle g,\,a_{i}\rangle)-1,2\cdot d\,(s^{\prime}_{i}\otimes g)\\}\geq\\\
\geq
d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}\min\,\\{d\,(\langle
g,\,a_{i}\rangle),d\,(s^{\prime}_{i}\otimes g)\\}\\\ \end{array}$

Let’s consider two cases.

    1. 1.1

The minimum in this expression is always reached on the first argument. Then

$\begin{array}[]{l}d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}\min\,\\{d\,(\langle
g,\,a_{i}\rangle),d\,(s^{\prime}_{i}\otimes g)\\}=\\\
=d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)\geq\\\ \geq
d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)-\smashoperator[]{\max_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)\\\ \end{array}$

    2. 1.2

$a_{m}$ is the first answer, such that the minimum for $a_{m}$ is reached on
the second argument. Then the answers up to $a_{m}$ are sufficient to prove
the bound.

$\begin{array}[]{l}d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}\min\,\\{d\,(\langle
g,\,a_{i}\rangle),d\,(s^{\prime}_{i}\otimes g)\\}\geq\\\ \geq
d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\\{a_{1},\dots,a_{m}\\}}^{}}\min\,\\{d\,(\langle
g,\,a_{i}\rangle),d\,(s^{\prime}_{i}\otimes g)\\}=\\\
=d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\\{a_{1},\dots,a_{m-1}\\}}^{}}d\,(\langle
g,\,a_{i}\rangle)+d\,(s^{\prime}_{m}\otimes g)=\\\
=d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\\{a_{1},\dots,a_{m-1}\\}}^{}}d\,(\langle
g,\,a_{i}\rangle)+d\,(s^{\prime}_{m})+\smashoperator[lr]{\sum_{a_{i}\in(\mathcal{T}r^{ans}(s)\setminus\\{a_{1},\dots,a_{m}\\})}^{}}d\,(\langle
g,\,a_{i}\rangle)\geq\\\ \geq
d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)-d\,(\langle g,\,a_{m}\rangle)\geq\\\ \geq
d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)-\smashoperator[]{\max_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)\\\ \end{array}$

  2. 2.

Upper bound. Let’s show that

$\begin{array}[]{l}d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}\min\,\\{2\cdot
d\,(\langle g,\,a_{i}\rangle)-1,2\cdot d\,(s^{\prime}_{i}\otimes g)\\}\leq\\\
\leq
4\cdot(d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle)-\smashoperator[]{\max_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}d\,(\langle
g,\,a_{i}\rangle))\\\ \end{array}$

For the upper bound we replace every $\min$ with any of its arguments (the
result can only increase). Let
$a_{m}=\underset{\makebox[0.0pt]{\mbox{\tiny{$a_{i}\in\mathcal{T}r^{ans}(s)$}}}}{argmax}\;\;d\,(\langle
g,\,a_{i}\rangle)$. Then for the upper bound let’s go with the second argument
of $\min$ for $a_{m}$ and with the first argument for all others.

$\begin{array}[]{l}d\,(s)+\smashoperator[lr]{\sum_{a_{i}\in\mathcal{T}r^{ans}(s)}^{}}\min\,\\{2\cdot
d\,(\langle g,\,a_{i}\rangle)-1,2\cdot d\,(s^{\prime}_{i}\otimes g)\\}\leq\\\
\leq d\,(s)+2\cdot d\,(s^{\prime}_{m}\otimes
g)+\smashoperator[lr]{\sum_{a_{i}\in(\mathcal{T}r^{ans}(s)\setminus\\{a_{m}\\})}^{}}(2\cdot
d\,(\langle g,\,a_{i}\rangle))\leq\\\ \leq d\,(s)+2\cdot
d\,(s^{\prime}_{m})+2\cdot\smashoperator[lr]{\sum_{a_{i}\in(\begin{array}[]{l}\mathcal{T}r^{ans}(s)\setminus\\\
\\{a_{1},\dots,a_{m}\\})\end{array}}^{}}d\,(\langle
g,\,a_{i}\rangle)+2\cdot\smashoperator[lr]{\sum_{a_{i}\in(\mathcal{T}r^{ans}(s)\setminus\\{a_{m}\\})}^{}}d\,(\langle
g,\,a_{i}\rangle)\leq\\\ \leq d\,(s)+2\cdot
d\,(s)+2\cdot\smashoperator[lr]{\sum_{a_{i}\in(\mathcal{T}r^{ans}(s)\setminus\\{a_{m}\\})}^{}}d\,(\langle
g,\,a_{i}\rangle)+2\cdot\smashoperator[lr]{\sum_{a_{i}\in(\mathcal{T}r^{ans}(s)\setminus\\{a_{m}\\})}^{}}d\,(\langle
g,\,a_{i}\rangle)\leq\\\ \leq 4\cdot
d\,(s)+4\cdot\smashoperator[lr]{\sum_{a_{i}\in(\mathcal{T}r^{ans}(s)\setminus\\{a_{m}\\})}^{}}d\,(\langle
g,\,a_{i}\rangle)\\\ \end{array}$

∎

###### Lemma 0.A.8

Let $s=((s_{0}\otimes g_{1})\dots\otimes g_{k})$ and let $A_{i}$ be a set of
all answers that are passed to $g_{i}$, i.e.

$\begin{array}[]{rcl}A_{1}&=&\mathcal{T}r^{ans}(s_{0})\\\
A_{i+1}&=&\bigcup\limits_{a\in A_{i}}\mathcal{T}r^{ans}(\langle
g_{i},\,a\rangle)\end{array}$

Then

$\begin{array}[]{rcrl}d\,(s)&=&&d\,(s_{0})+\sum\limits_{1\leq i\leq
k}\displaystyle\sum\limits_{a\in A_{i}}d\,(\langle g_{i},\,a\rangle)\\\ \\\
t\,(s)&=&&t\,(s_{0})+\sum\limits_{1\leq i\leq k}\displaystyle\sum\limits_{a\in
A_{i}}t\,(\langle g_{i},\,a\rangle)+\\\
&&+\Theta\,(&d\,(s_{0})+\sum\limits_{1\leq i\leq
k}\displaystyle\sum\limits_{a\in A_{i}}d\,(\langle
g_{i},\,a\rangle)-\max^{\bullet}\limits_{a\in A_{k}}d\,(\langle
g_{k},\,a\rangle))\\\ \end{array}$

###### Proof

First we show that for all $i$, $A_{i+1}=\mathcal{T}r^{ans}(((s_{0}\otimes
g_{1})\dots\otimes g_{i}))$ (it’s a simple induction on $i$ and then on the
trace).

Then we can prove the statement by induction on $k$. We unfold $d\,(s\otimes
g_{k+1})$ and $t\,(s\otimes g_{k+1})$ using equations in Lem.
LABEL:lem:times_measure_equations. Then we rewrite $d\,(s)$ and $t\,(s)$ in
these equations with inductive hypothesis. For $d\,(s\otimes g_{k+1})$ we get
exactly the equation we need. For $t\,(s\otimes g_{k+1})$ we have a sum of the
following parts (first two from the unfolding of $t\,(s)$, last two from the
rest of the equation for $t\,(s\otimes g_{k+1})$):

  1. 1.

$t\,(s_{0})+\displaystyle{\sum\limits_{1\leq i\leq
k}}\displaystyle\sum\limits_{a\in A_{i}}t\,(\langle g_{i},\,a\rangle)$

  2. 2.

$\Theta\,(d\,(s_{0})+\displaystyle{\sum\limits_{1\leq i\leq
k}}\displaystyle\sum\limits_{a\in A_{i}}d\,(\langle
g_{i},\,a\rangle)-\max^{\bullet}\limits_{a\in A_{k}}d\,(\langle
g_{k},\,a\rangle))$

  3. 3.

$\displaystyle\sum\limits_{a\in A_{k+1}}t\,(\langle g_{k+1},\,a\rangle)$

  4. 4.

$\Theta\,(d\,(s_{0})+\displaystyle{\sum\limits_{1\leq i\leq
k}}\displaystyle\sum\limits_{a\in A_{i}}d\,(\langle
g_{i},\,a\rangle)+\displaystyle\sum\limits_{a\in A_{k}}d\,(\langle
g_{k+1},\,a\rangle)-\max^{\bullet}\limits_{a\in A_{k+1}}d\,(\langle
g_{k},\,a\rangle))$

We can see that the second part is subsumed by the last part (by Lem. 0.A.3).
The rest gives exactly the equation we need. ∎

Here is the general definition of well-formedness of states from [15].

###### Definition 4

Well-formedness condition for extended states:

  * •

$\diamond$ is well-formed;

  * •

$\left<{g,\sigma,n}\right>$ is well-formed iff
$\mathcal{FV}\,({g})\cup\mathcal{D}om\,(\sigma)\cup\mathcal{VR}an\,(\sigma)\subseteq\\{\alpha_{1},\dots,\alpha_{n}\\}$;

  * •

$s_{1}\oplus s_{2}$ is well-formed iff $s_{1}$ and $s_{2}$ are well-formed;

  * •

$s\otimes g$ is well-formed iff $s$ is well-formed and for all leaf triplets
$\left<{\\_,\\_,n}\right>$ in $s$ it is true that
$\mathcal{FV}\,({g})\subseteq\\{\alpha_{1},\dots,\alpha_{n}\\}$.

We will need Lem. LABEL:lem:measures_changing_env in the following generalized
form.

###### Lemma 0.A.9

Let
$\pi\colon\\{\alpha_{1},\dots,\alpha_{N}\\}\to\\{\alpha_{1},\dots,\alpha_{N^{\prime}}\\}$
be an injective function on variables and let $R_{\pi}$ be the following
inductively defined relation on states:

$\begin{array}[]{lcl}\Diamond R_{\pi}\Diamond&&\\\ \langle
g,\,(\sigma,\,n)\rangle R_{\pi}\langle
g^{\prime},\,(\sigma^{\prime},\,n^{\prime})\rangle&\textit{iff}&g\sigma\pi=g^{\prime}\sigma^{\prime}\\\
(s_{1}\oplus s_{2})R_{\pi}(s^{\prime}_{1}\oplus
s^{\prime}_{2})&\textit{iff}&s_{1}R_{\pi}s^{\prime}_{1}\land
s_{2}R_{\pi}s^{\prime}_{2}\\\ (s\otimes g)R_{\pi}(s^{\prime}\otimes
g^{\prime})&\textit{iff}&sR_{\pi}s^{\prime}\land\\\ \lx@intercol\textit{\quad
for all substates $\langle g_{i},\,(\sigma_{i},\,n_{i})\rangle$ in
$s$}\hfil\lx@intercol\\\ \lx@intercol\textit{\quad and corresponding substates
$\langle g^{\prime}_{i},\,(\sigma^{\prime}_{i},\,n^{\prime}_{i})\rangle$ in
$s^{\prime}$,}\hfil\lx@intercol\\\ \lx@intercol\quad
g\sigma_{i}\pi=g^{\prime}\sigma^{\prime}_{i}\hfil\lx@intercol\\\ \end{array}$

Then for any two well-formed states $s$ and $s^{\prime}$, such that all