text:
\section{Introduction}

For logic program analysis or formal semantics, the issue of
renaming variables and generally handling substitutions is inevitable.
Yet the image of substitutions in logic programming research is a
somewhat tainted one, at least since it has been pointed out by H.-P. Ko
\cite[p.\,148]{shep:94} that the original claim of strong completeness
of SLD-resolution needs to be amended,
due to a counter-example using the fact that \(\left(\mytop{x}{f(y,z)}\right)\)
is not more general than \(\left(\mytop{x}{f(a,a)}\right)\).
The example may look counter-intuitive, but it complies with the
definition of substitution generality.
Also, by composing substitutions, properties like equivalence, idempotency
or restriction are not preserved.
Lastly, due to group structure of renamings, permuting any number of variables
amounts to "doing nothing", as in \(\left(\mytop{x}{y} \mytop{y}{x}\right) \eqsub \idsubst\),
and such equivalences are also felt to be counter-intuitive.
Hence the prevalent sentiments that substitutions are "a quite hard matter
to deal with" (\cite{catuscia:90}) or "very tricky" (\cite{shep:94}).
As a remedy, in the context of aggregating most general unifiers in a
logic programming computation some helpful new concepts and operators were proposed,
like \emph{parallel composition} instead of traditional composition (\cite{catuscia:90})
and \emph{resultant} instead of answer substitution (\cite{lloyd:shepherdson:91}).
Still, for almost anyone embarking on a journey of logic program
analysis or formal semantics, sooner or later the need for renaming variables
and generally handling substitutions in a new context arises.

In case of \yt, the need arose while trying to prove adequacy of
an operational semantics for pure Prolog, \mymodelold \cite{KulasM:towcb},
and the context was one of \emph{extensibility}:
Given is a pair of queries that are alphabetic variants of each other.
As their respective \mymodelold derivations proceed to develop,
new variables may crop up, due to standardization-apart
(here called \emph{local variables}, \autoref{sec:local}),
but the status of being variant should hold.
This setup is known from the classical \emph{variant lemma} (\cite{lloyd}).
Additionally, the corresponding variables need to be \emph{collected},
obtaining at each step the temporary variance between the derivations.
As an example, assume the first query is \(p(z,u,x)\) and the second \(p(y,z,x)\).
There is only one relevant renaming,
\(\rho=\left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{u}\right)\).
Now assume in the next step the first derivation acquires the variable \(y\),
and the second \(w\).
The relevant renaming this time would be
\(\rho'=\left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{w} \mytop{w}{u}\right)\).
Clearly, \(\rho'\) is not an extension of \(\rho\),
which makes it seem unsafe to proceed: are some properties of the
previous step now in danger?
So the question is, how to "safely" extend a variable mapping.
For this purpose, in \autoref{sec:trenam} we introduce a slight
generalization of renaming, called \emph{\trenam{}}.
It is a mathematical underpinning of the intuitive practice of
renaming terms by just considering the necessary bindings, and not
worrying whether the result is a permutation.
In the above example,
renaming \(p(z,u,x)\) to \(p(y,z,x)\) means mapping
\(z\mapsto y,\, u\mapsto z\) and \( x\mapsto x\).
Intuitively, only \(z\mapsto y,\, u\mapsto z\) are considered necessary bindings,
giving the "renaming" \(\left(\mytop{z}{y} \mytop{u}{z}\right)\).
For \trenam, \(x\mapsto x\) is necessary as well.
It is based on \emph{relaxed core representation}, which is nothing else than
allowing some \(x\mapsto x\) pairs alongside "real" bindings, as placeholders.

\Trenam{}s relate to and are inspired by previous work as follows.
In \cite{plotkin:phd}, the concept of \emph{translation} is defined,
upon which alphabetic variance and standardization apart are built;
this is the same as \trenam but for relaxed core (page \pageref{page-transl}).
A \emph{safe} \trenam is more general than \emph{renaming for a term}
from \cite{lloyd}, and it maximizes \(W\) in the notion of
\emph{W-renaming} from \cite{eder:85} (page \pageref{page-w-ren}).
Also, it generalizes \emph{substitution renaming}
from \cite{amato:05} (\autoref{sec:substvar}).

In \autoref{sec:appl}, \trenam{}s are used to express and prove
a propagation claim for implemented Horn clause logic,
by means of local variable extension (\autoref{lem:propag}).
As a corollary, a variant lemma is obtained (\autoref{lem:var}).
Underway, we touch on the discrepancy between
the rather abundant theory of logic programming and a scarcity of
mathematical claims for implemented logic programming systems.  While
there are some formal proofs of properties like nominal unification
\cite{urban-unif}, for logic programming systems or their compilation
such are still few and far between, a notable exception being \cite{pusch-wam}.
New concepts like \trenam may be of help.

\section{Substitution}

First we need a bit of notation.
Assume two disjoint sets:
a countably infinite set \myemphsym{\VarSet} of \myemph{variable}s
and a set \myemphsym{\bfsl{Fun}} of \myemph{shape}s.
If \(W \subseteq \VarSet\), any mapping \(F\) with \(F(W)\subseteq\VarSet\) shall be called
\myemph{variable-pure on} \(W\).
A mapping variable-pure on the whole set of variables \VarSet shall be
simply called \myemph{variable-pure}.
If \(\VarSet\setminus W\) is finite, \(W\) is said to be \myemph{co-finite}.
A mapping \(F\) is \myemph{injective on} \(W\),
if whenever \(F(x)=F(y)\) for \(x,y \in W\) also holds \(x=y\).
Each
\(\myemphsym{\fsig[n]{f}} \in \bfsl{Fun}\) consists of
a \myemph{functor} \(f\) and an associated number of arguments \(n\),
called \myemph{arity}.
Functors of arity \(0\) are called \myemph{constant}s.  Starting from
\VarSet and \bfsl{Fun}, data objects or \myemph{term}s%
\footnote{In Prolog, everything is a term, and so shall \emph{term} be here
the topmost syntactic concept.} are built:
Any variable $x \in \VarSet$ is a {term}.
If \(t_1,...,t_n\) are terms and \(\fsig[n]{f} \in \bfsl{Fun}\),
then \(f(t_1,...,t_n)\) is a {term} with \myemph{shape} \fsig[n]{f}
and \myemph{constructor} \(f\).  In case of \(\fsig[0]{f}\), the
term shall be written without parentheses.
If a term \(s\) occurs within a term \(t\), we write \myemphsym{\(s \in t\)}.
The \myemph{ordered pair} of terms \(h\) and \(t\) is written
as \myemphsym{\([h|t]\)},
where \(h\) is called the \emph{head} and \(t\) the \emph{tail} of the
pair.  A special case is a \myemph{non-empty list},
distinguished by its tail being a special term
\(\myemphsym{[]}\) called the \myemph{empty list}, or a non-empty list
itself.  A \myemph{list of \(n\) elements} is the term
\([t_1|[t_2|[...[t_n|[]]]]]\), conveniently written as \myemphsym{\([t_1,...,t_n]\)}.
Let \myemphsym{\varsof{t}} be the set of variables in the term $t$.
If the terms \(s\) and \(t\) share a variable, that shall be written
\myemphsym{\(s \nonvardis t\)}.
Otherwise, we say \(s,t\) are \myemph{variable-disjoint}, written as
\myemphsym{\(s \vardis t\)}.

A recurrent theme in this paper shall be "relevance",
meaning "no extraneous variables" relative to some term or terms.
It was used in \cite[p.\.38]{apt:book} in unary sense, i.e.\@{} no extraneous
variables relative to (one) term.  This usage shall be reflected in the
text as follows: A renaming \(\rho\) embedding a \trenam \(\alpha\) is a
\myemph{relevant} embedding, if \(\varsof{\rho} \subseteq
\varsof{\alpha}\) (\autoref{alg:embed}).  Additionally, relevance in a
binary sense, concerning two terms, shall also be needed:
\label{page-cumul}
A mapping \(F\) is \myemph{\cumulative for \(t_1\) to \(t_2\)},
if \( \realDom(F)\subseteq \varsof{t_1} \) and \(\realRange(F) \subseteq \varsof{t_2}\)
(\autoref{alg:pren}, \autoref{lem:propag}).

\begin{definition}[substitution]
A \myemph{substitution} $\theta$ is a function mapping variables to terms,
which is identity almost everywhere.
In other words, it is a function \(\theta\) with
domain \(\realDom(\theta)=\VarSet\) such that
the set $\myemphsym{\Dom(\theta)} \ensuremath{\defeq}\xspace \{x \in \VarSet \suchthat \theta(x)\neq x\}$
is finite.%
\footnote{\cite{gallier} speaks of \emph{finite support}.
}

The set \(\Dom(\theta)\) shall be called the \myemph{active domain}%
\footnote{%
Traditionally called just \emph{domain}.
This may be confusing, since in the usual mathematical sense
it is always the whole \VarSet that is the domain of any substitution.
}
or \myemph{core} of $\theta$,
and its elements \myemph{active variable}s%
\footnote{The name \emph{active variable} appears in \cite{jacobs:langen:1992}.}
of \(\theta\).
The set \(\myemphsym{\Range(\theta)} \ensuremath{\defeq}\xspace \theta(\Dom(\theta))\)
is the \myemph{active range} of $\theta$.
A variable \(x\) such that $\theta(x) = x$ shall be called
a \myemph{passive} \emph{variable}, or a \emph{fixpoint}, for \(\theta\).
Also, we say that \(\theta\) is \emph{active} on the variables from
\(\Dom(\theta)\), and \emph{passive} on all the other variables.
If $\Dom(\theta) = \{x_1,..., x_k\}$, where $x_1,..., x_k$ are pairwise
distinct variables, and $\theta$ maps each $x_i$ to $t_i$, then $\theta$
shall have the \myemph{core representation} \(\{x_1/t_1, ..., x_k/t_k\}\),
or the perhaps more visual
\(\left(\mytop{x_1}{t_1} \mytop{...}{...} \mytop{x_k}{t_k}\right)\).
Each pair \(x_i,t_i\) is called the \myemph{binding} for $x_i$ in $\theta$,
denoted by \myemphsym{\(x_i/t_i \in \theta\)}.
Often we identify a substitution with its core representation, and thus
regard it as a syntactical object, a term representing a finite set.  So
the set of variables of a substitution is defined as
$\myemphsym{\varsof{\theta}} \ensuremath{\defeq}\xspace \Dom(\theta)\unija\varsof{\Range(\theta)}$.

The notions of restriction and extension of a mapping shall also be
transported to core representation: if \(\theta \subseteq \sigma\), we say
\(\theta\) is a \myemph{restriction} of \(\sigma\),
and
\(\sigma\) is an \myemph{extension} of \(\theta\).
The restriction \myemphsym{$\restrict{\theta}{W}$}
of a substitution $\theta$ on a set of variables $W\subseteq\VarSet$
is defined as follows:
if $x\in W$ then $\restrict{\theta}{W}(x)\ensuremath{\defeq}\xspace \theta(x)$,
otherwise $\restrict{\theta}{W}(x)\ensuremath{\defeq}\xspace x$.
The restriction of $\theta$ upon the variables of $t$ is abbreviated as
$\myemphsym{\restrict{\theta}{t}} \ensuremath{\defeq}\xspace \restrict{\theta}{\varsof{t}}$.

The \myemph{composition} $\myemphsym{\theta\compos\sigma}$
of substitutions $\theta$ and $\sigma$ is defined by
$(\theta\compos\sigma)(x) \ensuremath{\defeq}\xspace \theta(\sigma(x))$.
Composition may be iterated, written as
\(\myemphsym{\sigma^n}\ensuremath{\defeq}\xspace\sigma\compos\sigma^{n-1}\) for \(n\geq 1\),
and \(\myemphsym{\sigma^0}\ensuremath{\defeq}\xspace\idsubst\).
Here \(\myemphsym{\idsubst} \ensuremath{\defeq}\xspace \left(\right)\)
is the identity function on \VarSet.
In case a variable-pure substitution \(\rho\) is bijective, its inverse
shall be denoted as \(\myemphsym{\rho^{-1}}\).
A substitution $\theta$ satisfying the equality $\theta\compos\theta =\theta$
is called \myemph{idempotent}.

Definition of substitution is enhanced from variables to arbitrary terms
in a structure-preserving way by
$\myemphsym{\theta(f(t_1,..., t_n))} \ensuremath{\defeq}\xspace f(\theta(t_1),..., \theta(t_n))$.
If $t$ is a term, then $\theta(t)$ is an \myemph{instance} of $t$ via $\theta$.
\end{definition}

\begin{example}
\(
\left(\mytop{x}{u} \mytop{w}{v} \mytop{u}{x} \mytop{v}{w}\right) \compos \left(\mytop{u}{x} \mytop{v}{w} \mytop{x}{y} \mytop{y}{u} \mytop{z}{v} \mytop{w}{z}\right)
= \left(\mytop{\ko{u}}{\ko{u}} \mytop{\ko{v}}{\ko{v}} \mytop{x}{y} \mytop{y}{x} \mytop{z}{w} \mytop{w}{z} \mytop{\ko{x}}{\ko{u}} \mytop{\ko{w}}{\ko{v}} \mytop{\ko{u}}{\ko{x}} \mytop{\ko{v}}{\ko{w}}\right)
= \left(\mytop{x}{y} \mytop{y}{x} \mytop{z}{w} \mytop{w}{z}\right)
\).
\end{example}

\section{Renaming}

\begin{definition}[renaming]\label{def:ren}
A \myemph{renaming} of variables is a bijective variable-pure substitution.
\end{definition}
\noindent
In \cite{eder:85}, it is synonymously called "permutation".
We shall reserve the word for the general case where movement of
infinitely many variables is possible.
Here we synonymously speak of \myemph{finite permutation}
due to the fact that, being a substitution, any renaming has a finite
core, and \autoref{lem:permut} holds.

Due to structure preserving, if \(s \in t\) then \(\sigma(s) \in \sigma(t)\).
For bijective substitutions (i.e.\@{} renamings),
the converse property holds as well, giving

\begin{lemma}[renaming stability of "{$=$}", "{$\in$}", "{$\vardis$}"]\label{lem:ren:aff}
Let \(\rho\) be a renaming and \(s,t\) be terms.
Then
\(s=t\) ~iff~ \(\rho(s)=\rho(t)\),
and also
\(s\in t\) ~iff~ \(\rho(s) \in \rho(t)\).
As a consequence, \(s\vardis t\) ~iff~ \(\rho(s) \vardis \rho(t)\).
\end{lemma}

\begin{legacy}[\cite{maher}]\label{lem:permut}
A substitution \(\rho\) is a renaming iff \( \rho(\Dom(\rho)) = \Dom(\rho)\).
\end{legacy}

\begin{legacy}[\cite{eder:85}]\label{lem:eder:85}
Every injective variable-pure substitution is a renaming.
\end{legacy}

So composition of renamings is a renaming.  The next property is about
cycle decomposition of a finite permutation.

\begin{lemma}[cycles]\label{lem:cyc}
Let \(\sigma\) be a variable-pure substitution.  It is injective iff
for every \(x\in\VarSet \) there is \( n\in\Nat\) such that \(\sigma^n(x)=x\).
\end{lemma}
\begin{myproof}\reference{lem:cyc}
Assume \(\sigma\) injective, and choose \(x_0\in\VarSet\).
If \(\sigma(x_0)=x_0\), we are done.  Otherwise,
\(\sigma^i(x_0)\not=\sigma^{i-1}(x_0)\) for all \(i\ge 1\), due to
injectivity.  Hence, \(\sigma^{i-1}(x_0) \in \Dom(\sigma)\) for every
\(i\ge 1\).  Because of the finiteness of \(\Dom(\sigma)\), there is \(
m>k\geq 1\) such that \( \sigma^m(x_0)=\sigma^k(x_0) \).  Due to
injectivity, \(\sigma^{m-1}(x_0)=\sigma^{k-1}(x_0)\).  By iteration we
get \(n\ensuremath{\defeq}\xspace m-k\).
For the other direction, assume \(\sigma(x)=\sigma(y)\), and minimal
\(m,n\) such that \(\sigma^n(x)=x,~\sigma^m(y)=y\).  Consider the case
\(m\not=n\), say \(m>n\).
Then \(\sigma^{m-n}(y)=\sigma^{m-n}(x)=\sigma^{m-n}(\sigma^n(x))=
\sigma^{m-n}(\sigma^n(y))= \sigma^{m}(y)=y \), contradicting minimality
of \(m\).
Hence \(m=n\), so \(x=\sigma^{n}(x)=\sigma^{n}(y)=y\).
\end{myproof}

\section{Relaxed core representation}

If there is a substitution \(\sigma\) mapping a term \(s\) on a term
\(t\), then it is mapping each variable in \(s\) on a subterm of \(t\).
It is possible that a variable stays the same,
so if we want our mapping to explicitely cover
\emph{all} variables in \(s\),
as in the promised application (\autoref{sec:appl}), then
necessarily \(x/x\) would have to be tolerated as a "binding".

To cater for such wishes, the core of the substitution \(\sigma\) can be
relaxed to contain some passive variables, raising those above the rest,
as it were.
This simple technique is useful beyond the context of renaming,
so we assume arbitrary substitutions.

\begin{definition}[relaxed core]
If \(\Dom(\sigma) \subseteq \{x_1,...,x_n\}\), where variables
\(x_1,...,x_n\) are pairwise distinct, then \(\{x_1,...,x_n\}\) shall be
called a \myemph{relaxed core}
and
\(\left(\mytop{x_1}{\sigma(x_1)} \mytop{...}{...} \mytop{x_n}{\sigma(x_n)}\right) \)
shall be called a \myemph{relaxed core representation}
for \(\sigma\).
If we fix a relaxed core for \(\sigma\), it shall be denoted
\(\myemphsym{\cplus{\sigma}} \ensuremath{\defeq}\xspace \{x_1,...,x_n\}\).
The associated range \(\sigma(\cplus{\sigma})\) we denote as
\(\myemphsym{\rplus{\sigma}}\).
The set of variables of \(\sigma\) is as expected,
\(\myemphsym{\vplus{\sigma}} \ensuremath{\defeq}\xspace \cplus{\sigma}\unija\varsof{\rplus{\sigma}}\).
To get back to the traditional representation, we denote by
\(\myemphsym{\unrelax{\sigma}}\)
the (non-relaxed) core representation of \(\sigma\).
\end{definition}

For extending, substitutions are treated like sets of active bindings,
so (disjoint) union may be used:

\begin{definition}[sum of substitutions]
If
\(\sigma = \left(\mytop{x_1}{s_1} \mytop{...}{...} \mytop{x_n}{s_n}\right)\)
and
\(\theta = \left(\mytop{y_1}{t_1} \mytop{...}{...} \mytop{y_m}{t_m}\right)\)
are substitutions in relaxed representation such that
\(\{y_1,..., y_m\} \vardis \{x_1,..., x_n\}\),
then
\(\myemphsym{\sigma\sadd\theta} \ensuremath{\defeq}\xspace
  \left(\mytop{x_1}{s_1} \mytop{...}{...} \mytop{x_n}{s_n} \mytop{y_1}{t_1} \mytop{...}{...} \mytop{y_m}{t_m}\right)
\)
is the \myemph{sum} of \(\sigma\) and \(\theta\).
\end{definition}

For \autoref{sec:varlem}, backward compatibility of an extension shall be needed.

\begin{lemma}[backward compatibility]\label{rem:pasiv}
Let \(\sigma,\theta\) be substitutions and \(x\) be a variable. Then
\((\sigma\sadd\theta)(x)=\sigma(x)\)
~iff~ \(\theta(x)=x\).
\end{lemma}

\begin{myproof}\reference{rem:pasiv}

If \(x\not\in \cplus{\theta}\), then \(\theta(x)=x\),
and \((\sigma\sadd\theta)(x)=\sigma(x)\).
If \(x\in \cplus{\theta}\), then \((\sigma\sadd\theta)(x)=\theta(x)\)
and also \(x\not\in \cplus{\sigma}\), hence \(\sigma(x)=x\).
The condition \((\sigma\sadd\theta)(x)=\sigma(x)\)
collapses to \(\theta(x)=x\).
\end{myproof}

Passivity of \(\theta\) on a term \(t\) is guaranteed if \(\sigma\) is
"complete" for \(t\), i.e.\@{} lays claim to all its variables:

\begin{definition}[complete for term]
Let \(\sigma\) be given in relaxed core representation.
We say that \(\sigma\) is
\myemph{complete}
for \(t\) if \(\varsof{t} \subseteq \cplus{\sigma}\).
\end{definition}

In such a case there is no danger that an extension of \(\sigma\) might
map \(t\) differently from \(\sigma\):

\begin{corollary}[backward compatibility]\label{lem:compl:back}
If \(\sigma\) is complete for \(t\), then for any \(\theta\) holds:
\(\sigma\sadd\theta\) is complete for \(t\) and
\((\sigma\sadd\theta)(t) = \sigma(t)\).
\end{corollary}

\section{\Trenam}\label{sec:trenam}

In practice, one would like to change the variables in a term without
bothering to check whether this change is a
permutation of variables, i.e.\@{} a renaming in
the sense of \autoref{def:ren}.
For example, the term \(p(z,u,x)\) can be
changed to
\(p(y,z,x)\)
using
mapping
\(z\mapsto y\), \(u\mapsto z\), \(x\mapsto x\).
Let us call such a mapping \emph{\trenam{}}%
\footnote{%
Finding an appropriate name can be a struggle. Shortlisted were
\emph{pre-renaming} and \emph{proto-renaming}.
}.

Like any substitution, a \trenam \(\alpha\) shall also be represented
finitely, but in relaxed core representation, in order to capture
possible \(x\mapsto x\) pairings.  The set \(\cplus{\alpha}\) is fixed
by the terms to map.  Obviously, injectivity is important for such a
mapping, since \(p(z,u,x)\) cannot be mapped on \(p(y,y,x)\) without
losing a variable.  Hence,

\begin{definition}[\trenam]
A \myemph{\trenam} \(\alpha\) is a variable-pure substitution
injective on a finite set of variables
\({\cplus{\alpha}} \supseteq \Dom(\alpha)\).
\end{definition}

Clearly, any renaming is a \trenam.
For \autoref{lem:var}, we need to extend a given \trenam.

\begin{lemma}[extension of \trenam{}]
Let
\(\alpha = \left(\mytop{x_1}{y_1} \mytop{...}{...} \mytop{x_n}{y_n}\right)\)
and
\(\beta = \left(\mytop{u_1}{v_1} \mytop{...}{...} \mytop{u_m}{v_m}\right)\)
be \trenam{}s such that
\(\{u_1,..., u_m\} \vardis \{x_1,..., x_n\}\)
and
\(\{v_1,..., v_m\} \vardis \{y_1,..., y_n\}\).
Then \(\alpha\sadd\beta =
  \left(\mytop{x_1}{y_1} \mytop{...}{...} \mytop{x_n}{y_n} \mytop{u_1}{v_1} \mytop{...}{...} \mytop{u_m}{v_m}\right)
\)
is also a \trenam, with \(\cplus{\alpha\sadd\beta} = \cplus{\alpha} \dunija \cplus{\beta}\) and
\(\rplus{\alpha\sadd\beta} = \rplus{\alpha} \dunija \rplus{\beta}\).
\end{lemma}

\label{page-transl}
Plotkin's concept of \emph{translation} \cite[p.\,46]{plotkin:phd}
corresponds to \trenam without passive bindings.
There, the \emph{inverse translation} for
\(\tau \ensuremath{\defeq}\xspace  \left(\mytop{z}{y} \mytop{u}{z}\right)\)
would be
\(\tau_{inv} \ensuremath{\defeq}\xspace \left(\mytop{y}{z} \mytop{z}{u}\right)\).
Clearly, \(\tau_{inv} \compos \tau =
\left(\mytop{y}{z} \mytop{z}{u}\right) \compos \left(\mytop{z}{y} \mytop{u}{z}\right)
= \left(\mytop{y}{z}\right)\),
which is not identity substitution.
Although \(\restrict{(\tau_{inv}\compos\tau)}{\{z,u\}} = \idsubst\),
so \(\tau\) is reversible and thus "safe" to use on \(\{z,u\}\),
one might instinctively be wary of the possibility that handling
several translations in the same computation could somehow produce "unsafety".
Presumably for that reason, the concept of translation did not catch on,
and it is meanwhile customary to define alphabetic variance
using renaming rather than translation (\cite{apt:book}).
We revisit Plotkin's concept, enriched with passive bindings
and deemed fit for a new name, \emph{\trenam{}},
and show that its safe application on a term and
safe (even backward-compatible) extension are easily achievable,
thus justifying the intuitive practice.

\subsection{The question of inverse}

So a \trenam is more natural in practice, but a "full" renaming is
better mathematically tractable, due to its being invertible on \(\VarSet\).
The next property shows how to extend a \trenam \(\alpha\) to obtain a renaming,
and a \emph{relevant} one at that, i.e.\@{}
active only on the variables from \(\vplus{\alpha}\).
The claim is essentially given in
\cite{lloyd:shepherdson:91}, \cite{apt:book} and \cite{amato:05}
with emphasis on the core%
\footnote{%
 \cite[p.\,23]{apt:book}:
"Every finite 1-1 mapping \(f\) from \(A\) onto \(B\) can be extended to
 a permutation \(g\) of \(A\unija B\).  Moreover, if \(f\) has no
 fixpoints, then it can be extended to a \(g\) with no fixpoints."
}
of such an extension.
Originally the claim appears in \cite{eder:85},
with emphasis on the extent of coincidence%
\footnote{%
\cite[p.\,35]{eder:85}:
"Let W be a co-finite set of variables (...) and let \(\sigma\) be a
\hyperlink{bkm-w-ren}{W-renaming}. Then there is a permutation \(\pi\) which
coincides with  \(\sigma\) on the set W."
},
which is our concern as well.
We rephrase the claim around the notion of \trenam,
and provide a constructive proof based on \autoref{lem:cyc}.

\begin{theorem}[embedding]\label{lem:ren:w}
If \(\alpha\) is a \trenam, there is a renaming
\(\closure{\alpha}\)
which coincides with \(\alpha\) on
\(\VarSet\setminus(\rplus{\alpha}\setminus\cplus{\alpha})\)
such that \(\varsof{\closure{\alpha}}\subseteq \vplus{\alpha}\).
Additionally, if \(\alpha(x)\not=x\) on \(\cplus{\alpha}\), then
\(\closure{\alpha}(x)\not=x\) on \(\vplus{\alpha}\).
\end{theorem}

\begin{figure}[htbp]\center
\hrulefill\par
\(\myemphsym{\closure{\alpha}(x)} \ensuremath{\defeq}\xspace
\begin{cases}
\alpha(x), & \text{if } x\in \cplus{\alpha} \\
z, & \text{if } x\in \rplus{\alpha}\setminus \cplus{\alpha} \text{ and } \alpha^{m}(z)=x \text{ for maximal } m\leq n \\
x, & \text{outside of }\cplus{\alpha}\unija \rplus{\alpha}
\end{cases}
\)
\par\hrulefill
\caption{Closure, the natural relevant embedding}
\label{alg:embed}
\end{figure}

\begin{myproof}\reference{lem:ren:w}
If \(\alpha\) is a \trenam, then \(\cplus{\alpha}\) and \(\rplus{\alpha}\)
are sets of \(n\) distinct variables each.
The wanted renaming is constructed in \autoref{alg:embed},
with the intention to close the possibly open chain \(x, \alpha(x), \alpha^2(x),...\)
So let us see whether for every \(x\) there is a \(j\) such that
\(\closure{\alpha}^j(x)=x\).  If \(x\in \cplus{\alpha}\), we start as in the proof of
\autoref{lem:cyc}, and consider the sequence \(x,\alpha(x),\alpha^2(x), ...\)
Since \(\cplus{\alpha}\) is finite, either we get two equals (and proceed as there),
or we get \(\alpha^k(x)\not\in \cplus{\alpha}\) and are stuck.
For \(y\ensuremath{\defeq}\xspace \alpha^k(x)\) we know \(\closure{\alpha}(y)=z\) such that
\(\alpha^{m}(z) = y\) with maximal \(m\), so \(m\geq k\).  Therefore,
\(
\alpha^m(\closure{\alpha}(y))=y=\alpha^k(x)
\).
Due to injectivity of \(\alpha\) on \(\cplus{\alpha}\), we get
\(
\alpha^{m-k}(\closure{\alpha}(\alpha^k(x))) = x
\),
and hence \( \closure{\alpha}^{m+1}(x)=x \).

The cases \(x\in \rplus{\alpha}\setminus \cplus{\alpha}\) or \(x\not\in \cplus{\alpha}\unija \rplus{\alpha}\) are easy.
By  \autoref{lem:cyc}, \(\closure{\alpha}\) is injective.
By \autoref{lem:eder:85}, \(\closure{\alpha}\) is a renaming.
The discussion of the case \(\alpha(x)\not= x\) on \(\cplus{\alpha}\) is straightforward.
\end{myproof}

\begin{definition}[closure of a \trenam]
The renaming \(\closure{\alpha}\) constructed in \autoref{alg:embed} shall be called the
\myemph{closure} of \(\alpha\).
\end{definition}
\begin{remark}[relevant embedding is not unique]
Let \(\alpha=\left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{x} \mytop{w_1}{w_2}\right)\),
and let us embed it in a relevant renaming.
The \autoref{alg:embed} gives
\(\closure{\alpha} =
  \left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{x} \mytop{w_1}{w_2} \mytop{x}{u} \mytop{w_2}{w_1}\right)
\).
But \(\rho =
  \left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{x} \mytop{w_1}{w_2} \mytop{x}{w_1} \mytop{w_2}{u}\right)
\)
is also a relevant renaming which is embedding \(\alpha\).
In the usual notation for cycle decomposition, \(\rho = \{(x,w_1,w_2,u,z,y)\}\)
and \(\closure{\alpha} = \{(x,u,z,y), (w_1, w_2) \}\).
\end{remark}

If we reverse the \trenam, the closure algorithm shall be closing the
same open chains but in the opposite direction, hence
\begin{lemma}[reverse \trenam]\label{lem:cl:inv}
Let
\(\alpha\ensuremath{\defeq}\xspace \left(\mytop{x_1}{y_1} \mytop{...}{...} \mytop{x_n}{y_n}\right)\)
and
\(\alpha_{inv}\ensuremath{\defeq}\xspace \left(\mytop{y_1}{x_1} \mytop{...}{...} \mytop{y_n}{x_n}\right)\).
Then
\(\closure{\alpha_{inv}}=\closure{\alpha}^{-1}\).
\end{lemma}

\begin{remark}[closure is not compositional]\label{rem:cl:nocomp}
Take
\(\alpha\ensuremath{\defeq}\xspace \left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{x}\right)\)
and \(\rho\ensuremath{\defeq}\xspace\left(\mytop{x}{y} \mytop{y}{x}\right)\).
Then \(\closure{\alpha}=\left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{x} \mytop{x}{u}\right)\),~
\(\rho\compos\closure{\alpha} = \left(\mytop{z}{x} \mytop{u}{z} \mytop{x}{u}\right)\),~
\(\rho\compos\alpha=\left(\mytop{z}{x} \mytop{u}{z} \mytop{x}{y}\right)\)
and
\(\closure{\rho\compos\alpha}=\left(\mytop{z}{x} \mytop{u}{z} \mytop{x}{y} \mytop{y}{u}\right)\).
\end{remark}

\begin{remark}[closure is not monotone]\label{rem:cl:nomon}
If \(\alpha \supseteq \alpha'\),
then not always
\(\closure{\alpha} \supseteq \closure{\alpha'}\).
To see this, let
\(\alpha=\left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{x}\right)\) and
\(\alpha'=\left(\mytop{z}{y} \mytop{u}{z}\right)\).
Then
\(\closure{\alpha'}=\left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{u}\right)\)
and
\(\closure{\alpha}=\left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{x} \mytop{x}{u}\right)\).
\end{remark}

\subsection{Staying safe}\label{sec:safe}

Let us look more closely into \autoref{rem:cl:nomon}:
\(\alpha(y)=x \text{ and } \alpha(x)=x\), so \(y\) and \(x\) may not
simultaneously occur in the candidate term.  Otherwise, a variable shall
be lost, which we call "aliasing", like in
\(\left(\mytop{y}{x}\right)(p(x,f(y))) = p(x,f(x))\).

\begin{definition}[aliasing]
Let \(\alpha\) be a \trenam.  If \(x\not= y\) but \(\alpha(x)=\alpha(y)\), then \(\alpha\) is
\myemph{aliasing} \(x\) and \(y\).
\end{definition}

So what \autoref{rem:cl:nomon} means is:
if we want to use \(\alpha\) on a larger set than \(\cplus{\alpha}\), then the set
\(\myemphsym{\noninj(\alpha)} \ensuremath{\defeq}\xspace \rplus{\alpha}\setminus\cplus{\alpha}\)
should be avoided, because aliasing may happen.
But, luckily, its complement is safe:

\begin{lemma}[larger set]\label{lem:larger}
A \trenam \(\alpha\) is injective on the co-finite set
\(\VarSet\setminus\noninj(\alpha)\).
The set is maximal containing \(\cplus{\alpha}\).
\end{lemma}

\begin{myproof}\reference{lem:larger}

Let \(x,y \in \VarSet\setminus\noninj(\alpha)\).  Is it possible that
\(\alpha(x)=\alpha(y)\)?  Possible cases: If \(x,y \in \cplus{\alpha}\),
then by definition of \trenam \(\alpha(x)\not=\alpha(y)\).
If \(x,y \not\in \cplus{\alpha}\), then \(\alpha(x)=x\not= y=\alpha(y)\).
It remains to consider the mixed case \(x\in\cplus{\alpha}, \,y\not\in \cplus{\alpha}\).
We have \(\alpha(x) \in \rplus{\alpha}\) and
\(\alpha(y)=y\).  So is \(\alpha(x)=y\) possible?  If yes, then \(y \in \rplus{\alpha}\), but since \(y\not\in \cplus{\alpha}\), that would mean
\(y \in \noninj(\alpha)\).  Contradiction.

The set cannot be made larger: if \(y \in \noninj(\alpha)\), then there is
\(x \in \cplus{\alpha}\) with \(x\not=y\) and \(\alpha(x)=y=\alpha(y)\).
\end{myproof}

\begin{definition}[injectivity domain]
Since \(\myemphsym{\indom(\alpha)} \ensuremath{\defeq}\xspace \VarSet\setminus\noninj(\alpha)\)
is the largest co-finite set containing \(\cplus{\alpha}\)
on which \(\alpha\) is injective, it shall be called
the \myemph{injectivity domain} of \(\alpha\).
\end{definition}

The injectivity domain of a \trenam is clearly the only safe place for it to be mapping terms from.

\begin{definition}[safety of \trenam]

A \trenam{} \(\alpha\) is \myemph{safe}%
\footnote{%
Safe \trenam is more general than
\emph{renaming for a term} in
\cite[p.\,22]{lloyd}, since we do not require
\(\Dom(\alpha) \subseteq \varsof{t}\).
}
for a term $t$ if \(\varsof{t}\subseteq \indom(\alpha)\).
\end{definition}

Clearly, \(\indom(\alpha) = \cplus{\alpha} \unija (\VarSet\setminus\rplus{\alpha})\),
so \(\alpha\) is safe for its relaxed core. Hence,

\begin{corollary}[complete and safe]\label{lem:compl:safe}
If a \trenam is complete for a term, it is safe for that term.
\end{corollary}

For a \trenam \(\alpha\) with the quality \(
\rplus{\alpha}=\cplus{\alpha} \), i.e.\@{} a renaming, it is no surprise
that \(\indom(\alpha)=\VarSet\) and hence safety is guaranteed for any term.

A \trenam behaves like a renaming on its injectivity domain, since it
coincides with its closure there.  This follows immediately from \autoref{lem:ren:w}:
\begin{lemma}[injectivity domain]\label{lem:indom}
Let \(x\in \indom(\alpha)\). Then \(\alpha(x) = \closure{\alpha}(x)\).
\end{lemma}

\begin{corollary}[\trenam stability]\label{lem:ren:aff:gen}
A generalization of \autoref{lem:ren:aff} holds:
Let \(s,t\) be terms and \(\alpha\) be a \trenam safe for \(s,t\).
Then \(s=t\) iff
\(\alpha(s)=\alpha(t)\) and also \(s\in t\) iff \(\alpha(s) \in \alpha(t)\).
As a consequence, \(s\vardis t\) iff \(\alpha(s) \vardis \alpha(t)\).
\end{corollary}

Our definition of \trenam was inspired by the following more general notion from \cite{eder:85}.
\label{page-w-ren}
\begin{definition}[W-renaming, \cite{eder:85}]
Let \(W\subseteq V\).  A substitution \(\sigma\) is a \myemph{\hypertarget{bkm-w-ren}{W-renaming}}
if \(\sigma\) is variable-pure on \(W\), and \(\sigma\) is injective on \(W\).
\end{definition}
With this notion, \autoref{lem:larger} can be summarized as:
\(\indom(\alpha)\) is a co-finite set of variables,
and the largest set \(W \supseteq \cplus{\alpha}\) such that \(\alpha\)
is a W-renaming.

What about safety of extension?  If \(\alpha\) is safe for \(t\),
\(\alpha\sadd\beta\) does not have to be, even if \(\beta(t)=t\), as the
following example shows:
\( \alpha\ensuremath{\defeq}\xspace\left(\mytop{v}{w}\right),~ \beta\ensuremath{\defeq}\xspace\left(\mytop{z}{y} \mytop{u}{z} \mytop{y}{x}\right),~ t\ensuremath{\defeq}\xspace p(x) \)
(here no aliasing happened, though).
The next two claims address safety of extension.

\begin{lemma}[monotonicity]\label{lem:cont}
Assume \(\alpha\sadd\beta\) is defined. Then
\begin{enumerate}
\item
\(\indom(\alpha) \unija\, \indom(\beta) = \VarSet\)
\item
\(\indom(\alpha) \presek\, \indom(\beta)  \subseteq \indom(\alpha\sadd\beta)\)
\end{enumerate}
\end{lemma}

\begin{myproof}\reference{lem:cont}
Since
\(
(\VarSet\setminus A)\unija (\VarSet\setminus B) = \VarSet\setminus (A\presek B))
\),
and \(\noninj(\alpha) \vardis \noninj(\beta)\), we get
\(
\indom(\alpha) \unija \indom(\beta) = \VarSet
\).
Further,
\(
(\VarSet\setminus A) \presek (\VarSet\setminus B) = \VarSet\setminus (A\unija B)
\)
and so
\(
\noninj(\alpha\sadd\beta) = (\rplus{\alpha}\dunija\rplus{\beta})
  \setminus (\cplus{\alpha}\dunija\cplus{\beta})
  \subseteq
   (\rplus{\alpha}\setminus\cplus{\alpha}) \unija (\rplus{\beta}\setminus\cplus{\beta})
  = \noninj(\alpha) \unija \noninj(\beta)
\).
\end{myproof}

In \autoref{rem:cl:nomon}, \(\noninj(\alpha') = \{y\}\),
\(\noninj(\left(\mytop{y}{x}\right)) = \{x\}\),
and \(\noninj(\alpha) = \{x\}\),
hence
\(\indom(\alpha') = \VarSet\setminus\{y\}\),
\(\indom(\left(\mytop{y}{x}\right)) = \VarSet\setminus\{x\}\)
and
\(\indom(\alpha) = \VarSet\setminus\{x\}\).

By the last claim, staying within \(\indom(\alpha)\) and
\(\indom(\beta)\) ensures staying within \(\indom(\alpha\sadd\beta)\).
By assuming a bit more about \(\alpha\) than just safety, we may
ignore the nature of extension \(\beta\), and still ensure safety and
even backward compatibility of \(\alpha\sadd\beta\).
This shall be used in \autoref{sec:appl}.

\begin{theorem}[safety of extension]\label{lem:exx}
Assume \(\alpha\sadd\beta\) is defined.
\begin{enumerate}
\item
If \(\alpha\) is safe for \(t\) \,and\, \(\beta\) is safe for \(t\),
then \(\alpha\sadd\beta\) is safe for \(t\).

\item \label{lemx:eq}
If \(\alpha\) is complete for \(t\), then
\(\alpha\sadd\beta\) is complete (hence safe) for \(t\), and
\((\alpha\sadd\beta)(t) = \alpha(t)\).
\end{enumerate}
\end{theorem}
\noindent
The first part follows from \autoref{lem:cont} and the second
from \autoref{lem:compl:back} and \autoref{lem:compl:safe}.

\subsection{Variant of term and substitution}

The traditional notion of term variance, which is term renaming, shall
be generalized to \trenam.  As a special case, substitution variance is
defined, inspired by substitution renaming from \cite{amato:05}.
For this, substitution shall once again be regarded as a special case of
term.  The term is of course the relaxed core representation.  This
concept shall come in handy for proving properties of renamed
derivations (\autoref{sec:varlem}).

\subsubsection{Term variant}

\begin{definition}[term variant]
If \(\alpha\) is a \trenam safe for \(t\), then $\alpha(t)$ is a
\myemph{variant} of \(t\),  written
\myemphsym{\(\alpha(t) \variant t\)}.
The particular variance and the direction of its application may be
explicated by
\myemphsym{\(s \variant[\alpha] t\)} iff \(s=\alpha(t)\).
\end{definition}

If \(s\variant t\), then there is a unique \(\alpha\) mapping \(s\) to
\(t\) in a complete and \cumulative%
\footnote{%
"\Cumulative{}" in the binary sense (page \pageref{page-cumul}).
In case of \trenam, we naturally use \cplus{} as \realDom and \(\rplus{}\) as \realRange.
}
manner, i.e.\@{} mapping each variable pair and nothing else, as computed
by \autoref{alg:pren}.  The algorithm makes do with only one set for
equations and bindings, thanks to different types.
Termination can be seen from the tuple
\((\mathit{lfun}_{=}(E), \mathit{card}_{=}(E))\) decreasing in
lexicographic order with each rule application,
where \(\mathit{lfun}_{=}(E)\) is the number of function symbols in
equations in \(E\), and \(\mathit{card}_{=}(E)\) is the number of equations in \(E\).

\begin{figure}[htbp]
\hrulefill\par%
Start from the set \(E \ensuremath{\defeq}\xspace \{s=t\}\) and transform according to the
following rules.  The transformation is bound to stop.  If the stop was
not due to failure, then the final set \(E\) is
{the \trenam of \(s\) to \(t\)}, \myemphsym{\(\pren(s,t)\)}.
\begin{description}
\item[elimination]
\(
E \dunija \{x=y\}  \goto E, \text{ if } x/y \in E
\)
\item[failure: alias]
\(
E \dunija \{x=y\} \goto \text{failure, if }(x/z\in E,\, z\not=y)\text{ or } (z/y\in E,\, z\not=x)
\)
\item[binding]
\(
E \dunija \{x=y\} \goto E\unija\{x/y\}, \text{ if }(x/\any\not\in E)\text{ and } (\any/y\not\in E)
\)
\item[failure: instance]
\(
E \dunija \{x=t\}  \goto \text{failure, if } t\not\in \VarSet
\);~
\(
E \dunija \{t=x\}  \goto \text{failure, if } t\not\in \VarSet
\)
\item[decomposition]
\(
E \dunija \{f(s_1,...,s_n)=f(t_1,...,t_n)\} \goto E\unija\{s_1=t_1,..., s_n=t_n\}
\)
\item[failure: clash]
\(
E \dunija \{f(s_1,...,s_n)=g(t_1,...,t_m)\} \goto \text{failure, if }f\not=g\text{ or }m\not=n
\)
\end{description}
\unskip
\hrulefill
\caption{Computing the \trenam of $s$ to $t$}
\label{alg:pren}
\end{figure}

\begin{notation}[epsoid]
The \trenam constructed in \autoref{alg:pren} shall be simply called
\myemph{the \trenam} of \emph{\(s\) to \(t\)},
and denoted \myemphsym{\(\pren(s,t)\)}.
It is complete for \(s\) and \cumulative for \(s\) to \(t\).

In case \(s=t\), we obtain for \(\pren(s,t)\) essentially the identity
substitution.  However, regarded as \trenam{}s, \(\pren(t,t)\) and
\idsubst are not the same.  A \trenam \(\alpha\) with relaxed core \(W\)
mapping each variable on itself (in other words, \(\cplus{\alpha} = W\)
and \(\unrelax{\alpha}=\idsubst\)) shall be called the \myemph{$W$-epsoid}
and denoted \(\myemphsym{\id{W}}\).
For a term \(t\), we abbreviate
\(\myemphsym{\id{t}} \ensuremath{\defeq}\xspace \id{\varsof{t}}\).
\end{notation}
Regarding composition, an epsoid behaves just like \idsubst.
Its use is for providing completeness, and hence extensibility,
by means of placeholder bindings \(x/x\).

\subsubsection{Special case: substitution variant}\label{sec:substvar}
Even substitutions themselves can be renamed.  To rename a
substitution, one regards it as a syntactical object, a set of
bindings, and renames those bindings.
If \(\rho\) is a renaming and \(\sigma\) is a substitution,
\cite{amato:05} defines substitution renaming by
\(
\rho(\sigma) \ensuremath{\defeq}\xspace \{ \rho(x)/\rho(\sigma(x)) ~|~ x \in \Dom(\sigma) \}
\).
It is easy to see that \(\rho(\sigma)\) is a substitution in core
representation.  For this only two properties of \(\rho\) were needed:
variable-purity on \(\varsof{\sigma}\) and injectivity on
\(\varsof{\sigma}\).  These requirements are clearly fulfilled by
\trenam{}s safe on \(\sigma\) as well.  Hence,

\begin{definition}[substitution variant]\label{def:proto}
Let \(\sigma\) be a substitution and let \(\alpha\) be a
\trenam safe for \(\sigma\),  i.e.\@{}
\(\varsof{\sigma}\subseteq \indom(\alpha)\).
Then a
\myemph{variant} \emph{of $\sigma$ by $\alpha$} is
\begin{equation}\label{eq:rho:sigma}
\myemphsym{\alpha(\sigma)} \ensuremath{\defeq}\xspace \{ \alpha(x)/\alpha(\sigma(x)) ~|~ x \in \Dom(\sigma) \}
\end{equation}
\end{definition}
We may write
\myemphsym{\(\theta \variant[\alpha] \sigma\)}
if \(\theta = \alpha(\sigma)\), as with any other terms.  As can be
expected, the concept of variance by \trenam is well-defined, owing to
safety.  Otherwise, the result of \trenam would not even have to be a
substitution again, as in the case of
\(\alpha=\left(\mytop{y}{x}\right)\) and \(\sigma=\left(\mytop{x}{a} \mytop{y}{b}\right)\).

\begin{lemma}[well-defined]\label{lem:welldef}
Substitution variant is well-defined, i.e.\@{} \eqref{eq:rho:sigma}
is a core representation of a substitution, and \(\alpha\) does not introduce aliasing.
\end{lemma}

\begin{myproof}\reference{lem:welldef}

Let \(\Dom(\sigma)=\{x_1,...,x_n\}\).
Due to injectivity of \(\alpha\) on \(\varsof{\sigma}\), if
\(\alpha(x_i)=\alpha(x_j)\), then \(x_i=x_j\), so \(i=j\).
To finish the proof that \eqref{eq:rho:sigma} a core representation, observe
\( x \in \Dom(\sigma) \) iff \( x \not= \sigma(x) \) iff
\( \alpha(x) \not= \alpha(\sigma(x)) \), due to injectivity again.
Re aliasing, by \autoref{lem:ren:aff:gen}, if
\(\alpha(\sigma(x_i)) \nonvardis \alpha(\sigma(x_j))\),
then \(\sigma(x_i) \nonvardis \sigma(x_j)\),
meaning that \(\alpha\) does not introduce aliasing.
\end{myproof}

From \autoref{def:proto} and \autoref{lem:indom} follows
\begin{lemma}
Let \(\sigma\) be a substitution, \(\alpha, \beta\) be \trenam{}s and
\(\alpha(\sigma)\) and \((\alpha\compos\beta)(\sigma)\) be defined.
Then
\begin{enumerate}
\item
\( (\alpha\compos\beta)(\sigma) = \alpha(\beta(\sigma)) \)

\item
\( \alpha(\sigma) = \closure{\alpha}(\sigma) \)
\end{enumerate}
\end{lemma}

For the case of "full" renaming, there is a way to dissolve the new expression:%
\footnote{%
an immediate consequence being \(\rho(\sigma)\neq\rho\compos\sigma\)
}
\begin{legacy}[\cite{amato:05}]\label{lem:amato}
For any renaming \(\rho\) and substitution \(\sigma\)
\[
\rho(\sigma) = \rho\compos\sigma\compos\rho^{-1}
\]
\end{legacy}
Would such a claim hold for the weakened case, \trenam{}s?

\begin{theorem}[substitution variant]\label{lem:proto}
Let \(\sigma\) be a substitution and \(\alpha\) be a \trenam safe for
\(\sigma\). Then
\begin{enumerate}
\item
\(\alpha(\sigma)\compos\alpha = \alpha\compos\sigma\)
\item
\(\alpha(\sigma)=\closure{\alpha}\compos\sigma\compos\closure{\alpha}^{-1}\)
\end{enumerate}
\end{theorem}

\begin{myproof}\reference{lem:proto}

First part:
According to \autoref{def:proto}, for every \(x\in\VarSet\) holds
\( (\alpha(\sigma)\compos\alpha)(x) = \alpha(\sigma(x)) \).
Since any substitution is structure-preserving, the claim holds for any term \(t\) as well.
Second part: From the first part we know
\(\closure{\alpha}(\sigma)\compos\closure{\alpha}=\closure{\alpha}\compos\sigma\),
hence
\(\closure{\alpha}(\sigma)=\closure{\alpha}\compos\sigma\compos\closure{\alpha}^{-1}\).
By \autoref{lem:indom}, \( \alpha(\sigma) = \closure{\alpha}(\sigma) \).
\end{myproof}

It is known that idempotence and equivalence of substitutions are not
compatible with composition \cite{eder:85}.  Luckily, the concept of
variance, with constant \trenam, does not share this handicap:

\begin{theorem}[compositionality]\label{lem:proto:compos}
Let \(\sigma,\theta\) be substitutions and \(\alpha\) be their safe \trenam. Then
\begin{align*}
\alpha(\sigma\compos\theta) &= \alpha(\sigma)\compos\alpha(\theta)
\end{align*}
\end{theorem}

\begin{myproof}\reference{lem:proto:compos}

Since \(\varsof{\sigma\compos\theta} \subseteq \varsof{\sigma}\unija \varsof{\theta}\),
clearly \(\varsof{\sigma\compos\theta} \subseteq  \indom(\alpha)\).
By \autoref{lem:proto},
\(
\alpha(\sigma) \compos \alpha(\theta)
= \closure{\alpha}\compos\sigma\compos\closure{\alpha}^{-1}\compos\closure{\alpha}\compos\theta\compos\closure{\alpha}^{-1}
= \closure{\alpha}\compos\sigma\compos\theta\compos\closure{\alpha}^{-1}
= \alpha(\sigma\compos\theta)
\).
\end{myproof}

\section{Application}\label{sec:appl}
Implementing logic programming means that the {freedom} of Horn clause logic
(\myemphsym{HCL}) must be restrained:
\begin{itemize}
\item
most general unifier (\myemph{mgu}) is provided by a fixed algorithm,

\item
standardization-apart is provided by a fixed algorithm.
\end{itemize}
Every implementation of HCL is parametrized by the two algorithms.
Here we shall consider only the unification algorithm, so by
\myemphsym{\hclparam}
an implementation of HCL using unification algorithm \ualg is denoted.
From the literature (\emph{variant lemma}) we know that such a restriction is not
compromising soundness and completeness of SLD-resolution. Yet, there may
be lots of "lowlier" claims which more or less implicitly rely on
freedom of mgus and standardization-apart.  For example, with both
choices fixed we may not any more just rename an SLD-derivation
wholesale (the resolvents, the mgus, the input clauses), as was possible
in Horn clause logic, based on \autoref{lem:ren:aff}.  This is because
the two algorithms do not have to be renaming-compatible.  In fact, the
second one cannot be, which makes claims like \autoref{lem:propag} necessary.

Let us cast a look at the first restriction.  For any two unifiable
terms \(s,t\) holds that the set of their mgus, written as
\(\myemphsym{\mgus(s,t)}\), is infinite.
On the other hand, in practice any unification algorithm \ualg produces,
for the given two unifiable terms, just one deterministic value as their mgu.
We shall denote this particular mgu of \(s\) and \(t\) as
\(\myemphsym{\ualg(s, t)}\),
the \myemph{algorithmic mgu} of \(s\) and \(t\) obtained by \ualg.

The abundancy of mgus is not only good, it also stands in the way of proofs.
The simplest unification problem \(p(x)=p(y)\)
has among others two equally attractive candidate mgus,
\((\mytop{x}{y})\) and \((\mytop{y}{x})\).
Assume our unification algorithm decided upon \((\mytop{x}{y})\).
Assume further that we rename the protagonists and obtain \(p(x)=p(z)\).
What mgu shall be chosen this time?  To ensure some dependability in
this issue, we shall require of any unification algorithm the following
simple requirement, postulated as an axiom:

\begin{axiom}[renaming compatibility]\label{ax:mgu}
Let \ualg be a unification algorithm.
For any renaming \(\rho\) and any equation \(E\), it has to hold
\(
\ualg(\rho(E)) = \rho(\ualg(E)).
\)
\end{axiom}
Since classical unification algorithms like Robinson's and
Martelli-Montanari's do not depend upon the actual names of variables
(as observed in \cite{amato:05}),
this requirement is in practice always satisfied.

\begin{remark}[renaming compatibility of \mgus]\label{rem:mgu}
For every \(\rho\) and \(E\) holds
\(
\mgus(\rho(E)) = \rho(\mgus(E)).
\)
This is due to \autoref{lem:proto} and \autoref{lem:ren:aff}.
Assume \(\sigma\in\mgus(s,t)\), then
\(
\rho(\sigma)(\rho(s))= \rho(\sigma(s))= \rho(\sigma(t)) = \rho(\sigma)(\rho(t))
\).
Further, if \(\theta\) is a unifier of \(\rho(s),\rho(t)\),
then \(\theta\compos\rho\) is a unifier of \(s,t\),
hence there is a renaming \(\delta\) with \(\theta\compos\rho = \delta\compos\sigma\), giving
\(\theta
=\delta\compos\sigma\compos\rho^{-1}
=\delta\compos\rho^{-1}\compos\rho\compos\sigma\compos\rho^{-1} = (\delta\compos\rho^{-1})\compos\rho(\sigma)\),
meaning \(\rho(\sigma)\in \mgus(\rho(E))\).
For the other direction, observe
\(\theta
= \rho\compos\rho^{-1}\compos\delta\compos\sigma\compos\rho^{-1}
= \rho(\rho^{-1}\compos\delta\compos\sigma)
\).
\end{remark}

\subsection{Handling local variables in \protect\hclparam}\label{sec:local}

With \ualg complying to \autoref{ax:mgu} and yielding relevant mgus, that is to say
with practically any \ualg,%
\footnote{Classical unification algorithms not only satisfy \autoref{ax:mgu} but also
yield idempotent mgus. Idempotent mgus are always relevant (\cite{apt:book}).
}
\label{foot-relevance}
a propagation result for SLD-derivations can be proved, which leads to a
constructive and incremental version of the variant lemma.

Regarding SLD-derivations, for the most part we shall assume traditional
concepts as given in \cite{lloyd} and \cite{apt:book}, but with some changes and
additions listed below.
An input clause \(\ensuremath{\mathcal{K}}\xspace_i\) obtained from a program clause \(\klausi\)
by replacing the variables in order of appearance with \(t_1,...,t_n\)
may be denoted as \(\ensuremath{\mathcal{K}}\xspace_i=\myemphsym{\klausi[t_1,...,t_n]}\).
Assume now an SLD-derivation \compd for \(G\) of the form
\(
G \resol{\ensuremath{\mathcal{K}}\xspace_1\mathord{:}\sigma_1} G_1
\resol{\ensuremath{\mathcal{K}}\xspace_2\mathord{:}\sigma_2}
...
\resol{\ensuremath{\mathcal{K}}\xspace_n\mathord{:}\sigma_n}
G_n
\).

\begin{itemize}
\item

$\ensuremath{\mathcal{K}}\xspace_i$ is here the \emph{actually used} variant of a program clause
(i.e.\@, the current \emph{input clause}) and not the program clause itself.

\item
The substitution \(\sigma_n\compos...\compos\sigma_1\) shall be called
the \myemph{partial answer} for \(G\) at step \(n\) of the derivation.
A final partial answer, whenever \(G_n=\emptycl\), shall be called a
\myemph{\casq} for \(G\).

\end{itemize}
Relation to earlier concepts of answer: In a derivation, the \myemph{resultant}
of level \(n\) is defined in \cite{lloyd:shepherdson:91} as
\(
\sigma_n\compos...\compos\sigma_1(G) \ensuremath{\leftarrow}\xspace  G_n
\).
So partial answer is at heart of resultant.
An \emph{answer substitution}
for \(G\) is defined in \cite{apt:vanemden:82} exactly as \casq;
later (\cite{lloyd}, \cite{apt:book})
it is made relevant by restricting to variables of \(G\),
hence \(\restrict{(\sigma_n\compos...\compos\sigma_1)}{G}\) whenever \(G_n=\emptycl\),
and called \myemph{computed answer substitution (\cas)}.

Showing the actually used variants of program clauses (instead of
program clauses themselves) enables a simple definition of derivation variables:
the annotations
\(\ensuremath{\mathcal{K}}\xspace_i\mathord{:}\sigma_i\)
are regarded as part of the derivation, so
\(
\myemph{\varsof{\compd}}  \ensuremath{\defeq}\xspace
(\varsof{G} \unija ... \unija \varsof{G_n})
\unija
(\varsof{\sigma_1} \unija ... \unija \varsof{\sigma_n})
\unija
(\varsof{\ensuremath{\mathcal{K}}\xspace_1} \unija ... \unija \varsof{\ensuremath{\mathcal{K}}\xspace_n})
\).

Now to the propagation result. Assume the program
"\meta{son(S) \ensuremath{\leftarrow}\xspace male(S),\, child(S,P).}",
and let us enquire about \meta{son} in two derivations.
If we know that one query, say \meta{son(X)}, is a variant of the
other, \meta{son(A)}, does the same connection hold between the
resolvents as well?

As can be seen from \autoref{tab:resolve} and \autoref{fig:propag},
in a resolution some new variables may crop up, originating from standardization-apart.
Let us call them \myemph{local variable}s,  as opposed to \emph{query variable}s.
Likely causes are
a pattern in a clause head (\fsig[1]{nat} in \autoref{tab:resolve})
or surplus variables in a clause body (\fsig[1]{son} in \autoref{fig:propag}).
But even without those,
local variables can appear (\fsig[1]{p} in \autoref{tab:resolve}),
except with a restriction to \emph{normal SLD-derivation} (\cite{bol:92}),
preventing "needless renaming of variables".
Were it not for local variables, the resolvents in both derivations
would clearly be variants, with the same \trenam as for the original queries.
Yet, even though the variables new in one derivation do not have to be new in the other,
the \trenam can (under reasonable conditions) be extended to accomodate them.
The claim is proved in a constructive manner.

\begin{table}[htbp]\center
\begin{tabular}{@{}l@{\hspace{2\tabcolsep}}l@{\hspace{2\tabcolsep}}l@{}}
\begin{cell}
\rm query
\\\midrule
   \meta{nat(X)}
\\
  \meta{nat(A)}
\\
 \meta{p(X)}
\\
 \meta{p(A)}
\end{cell}
&
\begin{cell}
\rm  input clause
\\\midrule
\meta{nat(s(A)) \ensuremath{\leftarrow}\xspace nat(A).}
\\
\meta{nat(s(B)) \ensuremath{\leftarrow}\xspace nat(B).}
\\
\meta{p(A) \ensuremath{\leftarrow}\xspace q(A).}
\\
\meta{p(B) \ensuremath{\leftarrow}\xspace q(B).}
\end{cell}
&
\begin{cell}
\rm resolvent
\\\midrule
\meta{nat(A)}
\\
\meta{nat(B)}
\\
\meta{q(X)} or \meta{q(A)}
\\
\meta{q(A)} or \meta{q(B)}
\end{cell}
\end{tabular}
\caption{Resolution may produce local variables}
\label{tab:resolve}
\end{table}

\begin{lemma}[propagation of variance]\label{lem:propag}
Assume a unification algorithm \ualg satisfying \autoref{ax:mgu}.
Assume an SLD-derivation \(\compd\) ending with \(G\) and an
SLD-derivation \(\compd'\) ending with \(G'\) such that
\(\alpha(G)=G'\) for some \trenam \(\alpha\)
which is complete for \(G\) and \cumulative for
\(\compd\) to \(\compd'\).

Further assume that
 \(G \resol{\ensuremath{\mathcal{K}}\xspace\mathord{:}\sigma} H\)
and
 \(G' \resol{\ensuremath{\mathcal{K}}\xspace'\mathord{:}\sigma'} H'\)
such that in \(G\) and \(G'\) atoms in the same positions were selected
and \(\ensuremath{\mathcal{K}}\xspace, \ensuremath{\mathcal{K}}\xspace'\) are variants.
Lastly assume that \(\sigma\) is a relevant mgu.
Then for \(\lambda \ensuremath{\defeq}\xspace \pren(\ensuremath{\mathcal{K}}\xspace, \ensuremath{\mathcal{K}}\xspace')\) holds
\begin{enumerate}

\item\label{lem:propag:complete}
\(\alpha\sadd\lambda\) is complete for \(H\)
and \(\sigma\)

\item\label{lem:propag:cumulative}
\(\alpha\sadd\lambda\)
is \cumulative for
\(\compd \resol{\ensuremath{\mathcal{K}}\xspace\mathord{:}\sigma} H\) to
\(\compd' \resol{\ensuremath{\mathcal{K}}\xspace'\mathord{:}\sigma'} H'\)

\item\label{lem:propag:increm}
\(H' = (\alpha\sadd\lambda)(H)\)
and
\(\sigma' = (\alpha\sadd\lambda)(\sigma)\)

\end{enumerate}
\end{lemma}
\begin{figure}[htbp]\center
\begin{math}
\begin{CD}
G @>\resol{}>>  H\\
@V\alpha V\alpha\,\sadd\,\lambda V
@VV\alpha\,\sadd\,\lambda V\\
G'  @>>\resol{}>  H'
\end{CD}
\end{math}
\hspace*{2cm}
\begin{math}
\begin{CD}
\meta{son(X)} @>\resol{}>> \meta{male(X),\, child(X,B)} \\
@VV\alpha=\left(\mytop{X}{A} \mytop{B}{X}\right)V
@VV\alpha\,\sadd\,\text{?} V\\
\meta{son(A)}  @>>\resol{}>  \meta{male(A),\, child(A,C)}
\end{CD}
\end{math}
\caption{Propagation of variance ...is not always possible}
\label{fig:propag}
\end{figure}

The claim can be summarized in \autoref{fig:propag}, together with the r\^{o}le of \cumulativeness requirement.
From \autoref{lem:propag} and \autoref{tab:resolve}
follows that resolution is not \trenam-stable (or even renaming-stable);
extending the \trenam with local variables may be necessary.

\begin{myproof}\reference{lem:propag}

First let us establish that \(\alpha\sadd\lambda\) is defined.
Due to
\emph{\cumulativeness of \(\alpha\) for \(\compd,\compd'\)},
\begin{equation}\label{lemp:cumul0}
{\cplus{\alpha}} \subseteq \varsof{\compd} \text{~and~}  {\rplus{\alpha}} \subseteq \varsof{\compd'}
\end{equation}
Due to \emph{standardization-apart},
\(\ensuremath{\mathcal{K}}\xspace \vardis {\compd}\)  and \(\ensuremath{\mathcal{K}}\xspace' \vardis {\compd'}\), hence
\begin{align}
&{\cplus{\lambda}} \vardis {\compd}  \text{~and~} {\rplus{\lambda}} \vardis {\compd'} \label{lemp:stap}
\end{align}
Thus
\( {\cplus{\alpha}} \vardis {\cplus{\lambda}} \) and \( {\rplus{\alpha}} \vardis {\rplus{\lambda}} \),
so \(\alpha\sadd\lambda\) is defined.
Also,
\eqref{lemp:stap} proves that \(\lambda\) is passive on old variables, i.e.\@{}
\(\lambda(\compd)=\compd\).
Let \(G \ensuremath{\defeq}\xspace (M,A,N)\) and \(H \ensuremath{\defeq}\xspace \sigma(M,B,N)\),
where \(M,B,N\) may be conjunctions.
Then \( G' = (M',A',N')=(\alpha(M),\alpha(A),\alpha(N)) \).
Let \(\ensuremath{\mathcal{K}}\xspace\from A_1 \ensuremath{\leftarrow}\xspace B_1\) and
\(\ensuremath{\mathcal{K}}\xspace'\from A_2 \ensuremath{\leftarrow}\xspace B_2\). Then
\(\sigma = \ualg(A, A_1)\), \(B = \sigma(B_1)\)
and \(\sigma' = \ualg(A', A_2)\), \(B' = \sigma'(B_2)\).
Also,
\begin{align}
& \alpha \text{ is complete for }M,A,N\text{: } \varsof{(M,A,N)} \subseteq \cplus{\alpha}, \text{ by \emph{completeness} of \(\alpha\) for \(G\)} \label{lemp:ac}
\\
& \lambda \text{ is complete for }A_1,B_1\text{: } \varsof{\ensuremath{\mathcal{K}}\xspace} = \varsof{(A_1, B_1)} = \cplus{\lambda}, \text{ by definition of \(\lambda\)} \label{lemp:lc}
\end{align}
Due to \emph{relevance} of \(\sigma\), we have
\(\varsof{\sigma} \subseteq \varsof{A}\unija\varsof{A_1}\),
which together with \eqref{lemp:ac} and \eqref{lemp:lc} gives
\begin{align}
& \alpha\sadd\lambda \text{ is complete for }\sigma\text{: } \varsof{\sigma} \subseteq
\cplus{\alpha\sadd\lambda}
\label{lemp:cs}
\end{align}
Having thus fielded all the assumptions, we obtain
\begin{align}
& \alpha\sadd\lambda \text{ is safe for }M,A,N,A_1, B_1,\sigma\text{: } \text{ by \eqref{lemp:ac}, \eqref{lemp:lc}, \eqref{lemp:cs} and \autoref{lem:exx}\eqref{lemx:eq}}  \label{lemp:safe}
\end{align}
\noindent
{\em Proof of \ref{lem:propag:complete}.:}
Completeness of \(\alpha\sadd\lambda\) for \(\sigma\) is proved above.
Completeness of \(\alpha\sadd\lambda\) for \(H\) follows from
\(
\varsof{H} \subseteq \varsof{G} \unija \varsof{\ensuremath{\mathcal{K}}\xspace}
   \subseteq \cplus{\alpha} \unija \cplus{\lambda}
   = \cplus{\alpha\sadd\lambda}
\),
by \eqref{lemp:ac} and \eqref{lemp:lc}.

\medskip
\noindent
{\em Proof of \ref{lem:propag:cumulative}.:}
By definition, \(\cplus{\lambda} = \varsof{\ensuremath{\mathcal{K}}\xspace}\)
and \(\rplus{\lambda} = \varsof{\ensuremath{\mathcal{K}}\xspace'}\).
Hence, and due to \cumulativeness of \(\alpha\),
\(
\cplus{\alpha\sadd\lambda} = \cplus{\alpha} \dunija \cplus{\lambda}
\subseteq \varsof{\compd} \unija \varsof{\ensuremath{\mathcal{K}}\xspace}
\subseteq \varsof{\compd \resol{\ensuremath{\mathcal{K}}\xspace\mathord{:}\sigma} H}.
\)
Similarly,
\(\rplus{\alpha\sadd\lambda} \subseteq \varsof{\compd' \resol{\ensuremath{\mathcal{K}}\xspace'\mathord{:}\sigma'} H'}\),
therefore
\(\alpha\sadd\lambda\) is \cumulative for
\(\compd \resol{\ensuremath{\mathcal{K}}\xspace\mathord{:}\sigma} H\)
to
\(\compd' \resol{\ensuremath{\mathcal{K}}\xspace'\mathord{:}\sigma'} H'\).

\medskip
\noindent
{\em Proof of \ref{lem:propag:increm}.:}
\begin{align*}
\lefteqn{\sigma' = \ualg(A',A_2)  = \ualg(\alpha(A), \lambda(A_1))
=\ualg((\alpha\sadd\lambda)(A), (\alpha\sadd\lambda)(A_1)), \text{ by \eqref{lemp:ac}, \eqref{lemp:lc} and \autoref{lem:compl:back}}  }
\\&
  = \ualg((\closure{\alpha\sadd\lambda})(A), (\closure{\alpha\sadd\lambda})(A_1))
= \closure{(\alpha\sadd\lambda)}(\sigma) = {(\alpha\sadd\lambda)}(\sigma) , \text{ by \eqref{lemp:safe}, \autoref{lem:indom} and \autoref{ax:mgu}}
\displaybreak[0]\\[.4em]
\lefteqn{B' = \sigma'(B_2) = (\alpha\sadd\lambda)(\sigma)(\lambda(B_1))
=(\alpha\sadd\lambda)(\sigma)((\alpha\sadd\lambda)(B_1)), \text{ by \eqref{lemp:lc} and \autoref{lem:compl:back}}  }
\\&
=(\alpha\sadd\lambda)(\sigma(B_1))=(\alpha\sadd\lambda)(B), \text{ by \autoref{lem:proto}}
\displaybreak[0]\\[.4em]
\lefteqn{H' = \sigma'(\alpha(M), B', \alpha(N))
= (\alpha\sadd\lambda)(\sigma)(\alpha(M), (\alpha\sadd\lambda)(B), \alpha(N)), \text{ by preceding line}   }
\\&
= (\alpha\sadd\lambda)(\sigma)((\alpha\sadd\lambda)(M), (\alpha\sadd\lambda)(B), (\alpha\sadd\lambda)(N)), \text{ by \eqref{lemp:ac} and \autoref{lem:compl:back}}
\\&
= (\alpha\sadd\lambda)(\sigma(M,B,N))
= (\alpha\sadd\lambda)(H), \text{ by \autoref{lem:proto}}
\end{align*}
\end{myproof}

\subsection{Variant lemma for \protect\hclparam}\label{sec:varlem}

\begin{definition}[similarity]
SLD-derivations of the same length
\begin{equation}\label{eq:def:simil}
\begin{split}
G \resol{\ensuremath{\mathcal{K}}\xspace_1\mathord{:}\sigma_1} G_1 \resol{\ensuremath{\mathcal{K}}\xspace_2\mathord{:}\sigma_2}  ... \resol{\ensuremath{\mathcal{K}}\xspace_{n}\mathord{:}\sigma_{n}} G_{n}
\\
G' \resol{\ensuremath{\mathcal{K}}\xspace'_1\mathord{:}\sigma'_1} G'_1 \resol{\ensuremath{\mathcal{K}}\xspace'_2\mathord{:}\sigma'_2}  ... \resol{\ensuremath{\mathcal{K}}\xspace'_{n}\mathord{:}\sigma'_{n}} G'_{n}
\end{split}
\end{equation}
are
\myemph{similar}
if \(G\) and \(G'\) are variants and additionally at each step \(i\)
holds: atoms in the same position are selected, and the input clauses
\(\ensuremath{\mathcal{K}}\xspace_i\) and \(\ensuremath{\mathcal{K}}\xspace'_i\) are variants.
\end{definition}

That the name "similarity" is justified, follows from the claim known as
\emph{variant lemma} (\cite{lloyd}, \cite{lloyd:shepherdson:91}, \cite{apt:book}),
here in the formulation from \cite{doets:93}:
\emph{Finite derivations which are similar and start from variant queries have variant resultants}.
For logic programming systems obeying \autoref{ax:mgu} and
relevance of mgu, a more precise claim can be proved.  The added
assumptions (the axiom and relevance) are practically void (see footnote
on page \pageref{foot-relevance}), yet the added conclusion has
substance: first, renaming a query now costs a degree of freedom -- if we
treat the two variants of the program clause at each step as independent,
then the two mgus are not independent.
Second, the precise variance is now known.

\begin{theorem}[variant claim for \hclparam]\label{lem:var}
Assume a unification algorithm \ualg satisfying \autoref{ax:mgu}
and yielding relevant mgus. Then:
\begin{itemize}
\item
finite SLD-derivations which are similar and start from variant queries
have variant partial answers

\item
the variance depends only on the starting queries and input clauses.
\end{itemize}
In particular, assume our similar derivations to be as in
\eqref{eq:def:simil}.  Then for every \(i=1,...,n\) holds
\(
G_i' = \beta_i(G_i),~
\sigma_i' = \beta_i(\sigma_i)
\text{~and~} \sigma_i'\compos...\compos\sigma_1' = \beta_i(\sigma_i\compos...\compos\sigma_1)
\),
where
\(\beta_i \ensuremath{\defeq}\xspace \alpha\sadd\lambda_1\sadd...\sadd\lambda_i\),~
\(\alpha \ensuremath{\defeq}\xspace \pren(G, G')\)~
and
\(\lambda_i \ensuremath{\defeq}\xspace \pren(\ensuremath{\mathcal{K}}\xspace_i, \ensuremath{\mathcal{K}}\xspace_i')\).
\end{theorem}

\begin{myproof}\reference{lem:var}
By assumption, \(G\) and \(G'\) are variants, so
\begin{equation}\label{lemv:1}
\alpha \ensuremath{\defeq}\xspace \pren(G, G')
\end{equation}
exists.
Clearly, \(\alpha\) is complete for \(G\).
By construction, \(\alpha\) is also
\cumulative for \(\compd_0 \ensuremath{\defeq}\xspace G\) ~to~ \(\compd_0' \ensuremath{\defeq}\xspace G'\).
We may iterate \autoref{lem:propag}, obtaining for every \(i=1,...,n\)
\begin{align}
\sigma_i' &= (\alpha\sadd\lambda_1\sadd...\sadd\lambda_i)(\sigma_i) \label{lemv:2}
\\
G_i' &= (\alpha\sadd\lambda_1\sadd...\sadd\lambda_i)(G_i) \label{lemv:3}
\end{align}
where \(\lambda_i \ensuremath{\defeq}\xspace \pren(\ensuremath{\mathcal{K}}\xspace_i, \ensuremath{\mathcal{K}}\xspace_i')\).
Due to completeness of \(\alpha\) for \(G\) and \autoref{lem:compl:back},
\begin{align} \label{lemv:4a}
\alpha(G) &= (\alpha\sadd\lambda_1\sadd...\sadd\lambda_i)(G)
\end{align}
So
\(
\sigma_i'\compos \sigma_{i-1}'\compos...\compos\sigma_1' =
  (\alpha\sadd\lambda_1\sadd...\sadd\lambda_i)(\sigma_i)
  \compos
  (\alpha\sadd\lambda_1\sadd...\sadd\lambda_{i-1})(\sigma_{i-1})
  \compos
...
  \compos
  (\alpha\sadd\lambda_1)(\sigma_1)
\).
We would like to extract \(\sigma_i\compos
\sigma_{i-1}\compos...\compos\sigma_1\) on the right, to have a connection between partial answers.

Assume
\(k<i\). Since \(\varsof{\sigma_k} \subseteq \varsof{G} \unija \varsof{\ensuremath{\mathcal{K}}\xspace_1}\unija...\unija \varsof{\ensuremath{\mathcal{K}}\xspace_k}
\subseteq \cplus{\alpha}\unija\cplus{\lambda_1}\unija...\unija\cplus{\lambda_k}
= \cplus{\alpha\sadd\lambda_1\sadd...\sadd\lambda_k}
\),
by \autoref{lem:exx}\eqref{lemx:eq}
\(
(\alpha\sadd\lambda_1\sadd...\sadd\lambda_k\sadd...\sadd\lambda_i)(\sigma_k) =
(\alpha\sadd\lambda_1\sadd...\sadd\lambda_k)(\sigma_k)
\).
Hence,
\begin{equation}
\begin{split}\label{lemv:4}
  (\alpha\sadd\lambda_1\sadd...\sadd\lambda_{i-1})(\sigma_{i-1}) &= (\alpha\sadd\lambda_1\sadd...\sadd\lambda_i)(\sigma_{i-1})
\\
...
\\
  (\alpha\sadd\lambda_1)(\sigma_1) &= (\alpha\sadd\lambda_1\sadd...\sadd\lambda_i)(\sigma_1)
\end{split}
\end{equation}
Let us abbreviate
\(
\beta_i \ensuremath{\defeq}\xspace \alpha\sadd\lambda_1\sadd...\sadd\lambda_i
\).
Then from \eqref{lemv:2} and \eqref{lemv:4} by
\autoref{lem:proto:compos}
\begin{equation}\label{lemv:5}
\sigma_i'\compos \sigma_{i-1}'\compos...\compos\sigma_1' =
  \beta_i(\sigma_i) \compos \beta_i(\sigma_{i-1})\compos...\compos \beta_i(\sigma_1)
= \beta_i(\sigma_i\compos\sigma_{i-1}\compos...\compos\sigma_1)
\end{equation}
which is the promised connection between partial answers.

Clearly, variance of partial answers means variance of \casq{}s,
\cas{}es and resultants as well.
For the cases when \(G_n = \emptycl\), we obtain, by \eqref{lemv:5},
the expected relationship between the respective \casq{}s:
\(\sigma_n'\compos...\compos\sigma_1' = \beta_n(\sigma_n\compos...\compos\sigma_1)
\).
\Cas{} differs from \casq{} by the added restriction on the query variables.
Due to renaming-compatibility of restriction, \eqref{lemv:5} and
\(\beta_n(G) = \alpha(G) = G'\), we obtain
\(
\restrict{\sigma_n'\compos...\compos\sigma_1'}{G'} = \beta_n(\restrict{\sigma_n\compos...\compos\sigma_1}{G})
\),
i.e.\@{} the same relationship.
Finally, knowing that the {resultant} of step \(i\) is
\({R_i} \ensuremath{\defeq}\xspace \sigma_i\compos...\compos\sigma_1(G) \ensuremath{\leftarrow}\xspace G_i\),
we obtain
\begin{align*}
\lefteqn{R_i' =
  \sigma_i'\compos...\compos\sigma_1'(G') \ensuremath{\leftarrow}\xspace G_i'
  = \beta_i(\sigma_i\compos...\compos\sigma_1)(\alpha(G)) \ensuremath{\leftarrow}\xspace \beta_i(G_i), \text{ by \eqref{lemv:5}, \eqref{lemv:1} and \eqref{lemv:3}}  }
\\&
= \beta_i(\sigma_i\compos...\compos\sigma_1)(\beta_i(G)) \ensuremath{\leftarrow}\xspace \beta_i(G_i)
= \beta_i((\sigma_i\compos...\compos\sigma_1)(G)) \ensuremath{\leftarrow}\xspace \beta_i(G_i), \text{ by \eqref{lemv:4a} and \autoref{lem:proto}}
\\&
= \beta_i(R_i)
\end{align*}
So partial answers of step \(i\) (and in consequence \cas{}es and resultants)
are variant via \(\beta_i\).
\end{myproof}

\begin{example}[similarity]
Let the logic program be
\begin{alignat*}{2}
&son(X) \ensuremath{\leftarrow}\xspace male(X),\, child(X,A). && \quad\color{\Commentcolor}\%\, \klausi_1
\\
&male(c).~ male(d).~ child(d,a).    && \quad\color{\Commentcolor}\%\, \klausi_2,~ \klausi_3, ~\klausi_4
\end{alignat*}
An interpreter for LD-resolution may produce the following two derivations:
\begin{align*}
&
\meta{son(A)} \resol{\ensuremath{\mathcal{K}}\xspace_1\mathord{:}\sigma_1} \meta{male(A),\, child(A,C)} \resol{\ensuremath{\mathcal{K}}\xspace_2\mathord{:}\sigma_2} \meta{child(d,C)}
\\&
\meta{son(B)} \resol{\ensuremath{\mathcal{K}}\xspace'_1\mathord{:}\sigma'_1} \meta{male(B),\, child(B,D)} \resol{\ensuremath{\mathcal{K}}\xspace'_2\mathord{:}\sigma'_2} \meta{child(d,D)}
\end{align*}
They are obviously similar, with
\(\ensuremath{\mathcal{K}}\xspace_1 = \klausi_1[\specu,C]\),~
\(\ensuremath{\mathcal{K}}\xspace'_1 = \klausi_1[\specv,D]\),~
\(\ensuremath{\mathcal{K}}\xspace_2 = \ensuremath{\mathcal{K}}\xspace'_2 = \klausi_3\).
The variables \(\specu,\specv\) stand for actually used variables, which are not
discernible from the form of derivations.
From the queries, input clauses and resolvents we can further deduce
which relevant mgus were used:
\(\sigma_1 = \left(\mytop{\specu}{A}\right)\),~
\(\sigma'_1 = \left(\mytop{\specv}{B}\right)\),~
\(\sigma_2 = \left(\mytop{A}{d}\right)\) and \(\sigma'_2 = \left(\mytop{B}{d}\right)\).
The mappings are
\(\alpha=\left(\mytop{A}{B}\right)\),~
\(\lambda_1=\left(\mytop{\specu}{\specv} \mytop{C}{D}\right)\) and \(\lambda_2=\idsubst\).
Clearly, they fulfill
\((\alpha\sadd\lambda_1)(\meta{male(A),\, child(A,C)}) = \meta{male(B),\, child(B,D)}\)
and
\((\alpha\sadd\lambda_1)(\left(\mytop{B}{A}\right))= \left(\mytop{C}{B}\right)\),
as well as
\((\alpha\sadd\lambda_1\sadd\lambda_2)(\meta{child(d,C)})=\meta{child(d,D)}\),
and so forth.
\end{example}

\section{Outlook}

Concepts relating to variable renaming have been reviewed and built upon,
with the aim of providing for practical needs of program analysis and
formal semantics in logic programming.
By \emph{relaxing the core representation} and forgoing permutation
requirement for renaming, the concept of \emph{\trenam{}} is obtained.
It is a mathematical underpinning of the intuitive practice of
renaming terms by just considering the necessary bindings,
where now \(x/x\) may be necessary.
In other words, a \trenam is a variable-pure substitution with
mutually distinct variables in range, possibly including some passive bindings.

\Trenam{}s enable incremental claims like variance propagation
in implemented Horn clause logic (\autoref{lem:propag}, \autoref{lem:var}).
There, \trenam{}s made it possible to keep track of new (\emph{local}) variables.

redpajama_set_name: RedPajamaArXiv


If you've been on the internet for a while, you know memes.
They're essentially joke setups available to everyone.
Every once in a while, a meme format takes off. Millions of people start using the format.
People use them over and over for likes and comments.
Eventually, the best ideas get exhausted and the format evolves.
Somebody adds more absurdity to it or changes elements in the meme.
Then THAT format gets exhausted.
This happens a few more times until the meme is "dead" and doesn't really get used anymore.
Why the hell am I telling you this?!
Broadly speaking, this is how markets behave—whether it be memes or products.
There are tons of "me too" products—just like there are "me too" memes, which are more or less all the same.
But what really wins money, followers and popularity are the ones which first tweak something and WIN.
Can you change your market?
Can you tweak something and set yourself apart from all the standard BS happening?
Obviously, this might lead to some failure. You're always taking risks.
But the payoff can be gigantic and can set you apart forever.
Plus, you won't be mediocre. But if you were, you probably wouldn't be reading this anyway.


text:
Weirdest Laws In Florida
Everett Atlas/Shutterstock
By Alice Minium/Jan. 6, 2022 1:13 pm EST
You've probably heard of "Florida Man," the archetypal figure whose bizarre antics have earned the state its online infamy as the capital of all things weird. While Florida Man is subject to legal fines and penalties for much of his lawless conduct (see his entry on Know Your Meme), even your ordinary Florida resident could be found breaking some of these laws you probably didn't know existed.
Nearly every state has dozens of antiquated laws still on the books (via Vox), and Florida is no exception. All of these laws are still in existence, and you can technically be prosecuted (although this rarely occurs). Each of them might have their own unique origin story, and it's possible, if not probable, that we have the misbehaving Florida Men of decades past to thank for their existence. Here are some of the weirdest laws in Florida you've probably never heard of, which are particularly shocking for a state that's not too big on laws to begin with.
Banned: adultery
Orlando/Getty Images
According to NPR, 28% of women and 41% of men say they've "thought about" cheating on their spouse. Whoever wrote Florida Statute 798.02 was ready to slap adulterers with consequences. According to the law, "living in open adultery" is a class two misdemeanor, rendering it punitively equivalent to driving with a suspended license or committing petty theft, both class two misdemeanors under Florida law. Class two misdemeanors can technically be punishable by up a $500 fine, six months' probation, and up to 60 days in jail (via Florida State Legislature's statute on "General Penalties").
A similar 1868 law banning unwed cohabitation was overturned in 2016 by then-governor Rick Scott (via Orlando Sentinel), but the law against adultery remains on Florida's books. According to Pew Research Center data reported by CNBC in 2016, approximately 18 million unmarried adults in the United States cohabitate. This marked a 27% jump over a nine-year span, so it makes sense this law would be overturned, lest we criminalize half the state's residents.
Exact statistics on adultery are not so readily available, but a 1990s study by the National Opinion Research Center (cited by U.S. News & World Report) found that 15% to 18% may have violated this law — although perhaps not openly.
Banned: releasing 10 or more balloons
Keystone/Getty Images
According to Florida Statute 379.23, releasing 10 or more balloons is prohibited by law. There are exceptions, however, if the balloons are biodegradable, they are part of a scientific or meteorological project, they're hot air balloons, or they will be released indoors. Additionally, you may petition the court for permission to release more than 10 balloons on a special occasion. The penalty for violating this law is a noncriminal infraction with a $250 fine.
This law was passed in 2012 and is included in the legislative chapter on fish and wildlife conservation. The reasoning for this ban is actually pretty wholesome: "release into the atmosphere of large numbers of balloons inflated with lighter-than-air gases poses a danger and nuisance to the environment, particularly to wildlife and marine animals."
For a coastal state, this law makes sense. The Ocean Conservation Society reports over 100,000 marine mammals die each year from plastic debris, and balloon fragments pose a particular risk for sea turtles due to their food-like appearance, often resulting in stomach blockages from swallowing, and even starvation.
Banned: 'Being a Peeping Tom'
Linda_K/Shutterstock
Although most states and localities ban "public indecency" or "spying," the language varies and is often odd. Satellite Beach, Florida, specifically bans "being a peeping tom" in its legislation. The Satellite Beach Code of Ordinances Sec. 38-3 (Code 1976, §§ 14-30, 14-31), titled "Peeping toms," says: "Any person who enters on or about the property of another and spies or looks through the windows, transoms or doors is hereby defined as a peeping tom. No person shall be a peeping tom."
The euphemism "peeping tom" originates from a centuries-old myth. In the myth, all citizens agreed not to look at Lady Godiva as she rode naked around the town of Coventry. One man, however, did not keep this promise: his name was Tom, and he peeped (via Phrases.co.uk). "Peeping Tom" became a term for a voyeur who invades the privacy of others for lewd purposes without the consent of the person they observe.
Banned: eating cottage cheese after 6 p.m. on a Sunday
Nitr/Shutterstock
Often referred to as "blue laws," hundreds of laws still exist across the United States banning certain activities from taking place on Sundays (via World Population Review). Sunday, in Christian tradition, was considered to be a day of rest, and this religious decree was often taken so seriously in the past that there were civil legal codes enforcing it. Many of these laws pertain to alcohol sale and consumption, but they can pertain to anything, including cottage cheese.
In Tampa Bay, Florida, for example, residents are absolutely prohibited from eating cottage cheese after 6 p.m. on Sundays, as the Florida Independent and South Florida Sun-Sentinel report. Florida has an entire subsection of "cottage food law" (via Florida Department of Agriculture and Consumer Services) regulating the preparation and sale of at-home foods, but it's unclear if the regulations on cottage cheese consumption are related or if they are some kind of restriction on the Sabbath-day labor implied.
Banned: musicians 'mingling' with fans
Print Collector/Getty Images
The Miami County Code of Ordinances contains a specific section pertaining exclusively to "dance halls and ballrooms." In addition to varying requirements on licensing, permits, alcoholic beverage limitations, and operating hours, legislators took the time to outline specific provisions for proper conduct between "entertainers" and members of crowds. Specifically, the law instructs that there shall be no mingling between "dance instructors" or "entertainers" and attendees or dance participants.
The text of (Code 1967, § 4-46; Code 1980, § 5-81) Sec. 5-45, titled "Dancehalls and Ballrooms: Employees mingling with customers," reads: "It shall be unlawful for employees or entertainers in dancehalls or ballrooms to mingle or fraternize with the customers or patrons of such establishments, except when actually providing dance instruction to such customers or patrons."
The law references another city code prohibiting nightclubs from permitting their entertainers to "contact or associate with" nightclub patrons or guests. This is undeniably bad news for all Miami groupies who were hoping to catch the eye of a cute guitarist.

redpajama_set_name: RedPajamaCommonCrawl


Today Native Instruments unveiled a new version of Traktor DJ, named Traktor DJ 2. The new version is quite different from the original version that only worked on IOS devices since it can work on both Windows and Mac as well.
At least for now, Traktor DJ 2 will only work with the Traktor Kontrol S2 MK3 and IOS devices.
Will TRAKTOR DJ 2 replace TRAKTOR PRO 3?
TRAKTOR DJ 2 is based on an entirely new codebase that will set TRAKTOR up for the future. TRAKTOR PRO 3 remains the most advanced incarnation of TRAKTOR. It's used by professionals worldwide on a daily basis and will continue to be our flagship DJ software for years to come.
TRAKTOR DJ 2 and TRAKTOR PRO 3 will therefore be developed and updated in tandem in the coming years, until we and our professional users consider the new platform to be mature enough to make the switch.
Traktor DJ 2 also integrates with SoundCloud GO, which gives you access to the entire SoundCloud library of sounds and tracks.
There is no word about compatibility with other DJ controllers besides the Traktor Kontrol Z1 and the Traktor Kontrol S2 MK3, but it's reasonable to expect that it will work with other controllers as well, especially as its feature set is expanded.
Native Instruments Releases Traktor Pro 3.1!
Black Friday DJ Gear And DJ Software Deals!


For those following each week, Apologies for the absence of a write up last week but unfortunately I had to skip the session due to a bad case of hay-fever and an ear infection….! But back this week and firing on all cylinders.
As mentioned in previous weeks, I was keen to try out some back flips and this was the main focus last night.
After warming up with some basic moves I switched trampolines and headed over to one with a harness above it. For the first few tries I was going to be hooked up to a harness while Mark (one of the coaches), controlled my decent. Quiet handy I thought as I didn't really want to land face first on the trampoline.
The instructions were, to first jump and then feel as though the belly button is pointing toward the celling, tucking the body and keeping it all together rather than separating the head. What I mean by this is trying to keep the body in alignment, (well that's the way I was trying to picture the whole thing), rather than a curved line where your head is preceding the flip. Of course the head would look into the new direction but not an over exaggerated curve of the spin.
Now when I first imagined myself doing a flips, I actually thought that I would jump and then throw my head back, followed by body and feet, but no. To stop any 'drifting' while in the air and to maintain a controlled ascent / decent, it is key to first jump and then rotate at the apex of the flip.
Obviously there are other movements going on here, like tucked leg, using the arms and spotting the landing.
Throughout the session I was comfortably getting around 8/10 attempts but the problem area lie in spotting the landing earlier enough. Sometimes I would get it, and other times not, usually spotting too late to be honest. The feedback I was getting was that I needed to tuck more and complete the rotation earlier, which would then allow me more time to spot the landing and, if needed, open up to slow the rotation down.
I got a few like this which felt super nice and keen to get back on it next week.
Now going back to the head preceding the body, it's a really interesting point with the whole, jump first then rotate. I think this relates to where a lot of people go wrong when trying out their first back flip on a snowboard.
When you see people doing back flips, say on the beach or in a park, they rarely start and land in the same spot. Most of the time drifting backwards or forwards slightly.
The other major different is of course while on a snowboard we are standing side on, where as when doing it on a trampoline we facing forward. (on a snowboard this type of spin may be called a barrel role or something similar).
However, these movements can be related as we are still going upside down. So, if drift backwards or forwards while doing a back flip on a snowboard over a jump, there is the possibility of: A: catching the lip on take off, B: drifting back and not making the landing.
Have a look at the following video below and let me know if you think the above statement is of value, (although it is questionable whether or not this guy was actually going for a back flip or not – either way, do you want to throw your head back).
Now while the above guy threw his head back to early, have a look at the following back flip. Another disadvantage of throwing back to much is that the board becomes light and shoots out from under you.
Looking forward to next week to try out / experiment some more with the back flips and will be talking more about my findings. Still trying to get my head around (no pun intended) the timing and movements.
Thanks Tom, It has been a few weeks since I've been down to trampolining but will put a post up soon concluding the whole thing.


text:
Home » KAI Adds Two to Build Group
KAI Adds Two to Build Group
KAI has added two new employees to its Build Group -- Melissa McGinnis-Russo (left) as senior project manager and and Joe Kabance as estimator/project engineer.
KEYWORDS build group / engineering / kai / new hire / OSHA
KAI has added two new employees to its Build Group -- Melissa McGinnis-Russo as senior project manager and Joe Kabance as estimator/project engineer.
McGinnis-Russo will serve as the MEP coordinator on the BJC HealthCare West County replacement hospital project, a PARIC/KAI joint venture. She comes to KAI with 30 years of AEC industry experience and a diverse engineering background. Most recently she worked for Ascension Health, a large Catholic healthcare system, as director of engineering where she oversaw MEP infrastructure projects for over 130 hospitals. Her experience includes overseeing engineering on large capital projects, GPO agreements, executing contracts and building relationships with vendors, contractors and facility directors across the country. She has a Bachelor of Technology in Mechanical Engineering from Washington University in St. Louis and a Commissioning Certification from the University of Wisconsin-Madison. She holds certifications in the following: ASHE Healthcare, OSHA 30-Hour and Carrier and Trane Load Calculation Programs. McGinnis-Russo is a member of the American Society of Heating, Refrigeration and Air-Conditioning Engineers; American Society of Healthcare Engineering and Design-Build Institute of America.
Kabance served as an intern at KAI while completing his Bachelor of Science in Engineering/Construction Management at Southern Illinois University - Edwardsville, where he achieved the highest score in the school's history on the AIC Level 1 exam. Graduating in December, Kabance accepted a position at KAI as an estimator/project engineer. He also has an Associates Degree in Business Management from St. Louis Community College and has earned an OSHA 10-Hour certification. He is also certified as an Associate Constructor with the American Institute of Constructors.
KAI Texas Adds 9 Employees to Architecture Dep.
KAI Design & Build Expands Marketing Dept. with New Hires and Promotions
KAI Design & Build Hires Three New Employees
KAI Design & Build Hires Michael Hein as Chief Integration Officer


DDN (Data Delivery Network) is a new generation of data distribution network based on blockchain technology , an upgraded version of CDN (Content Delivery Network).
DDN (Data Delivery Network) is a new generation of data distribution network based on blockchain technology , an upgraded version of CDN (Content Delivery Network). Its core is MatrixChain, a bottom-level system of blockchains created by the Ebookchain team over the past two years, focusing on data deposit, data distribution, copyright protection and knowledge realization. Its classic applications include Ebooker, Starchain, Art Traceability system, Sample library management system.Through the means of DDN pledge rapidly expand to the film and television, works of art, health care, insurance, Internet of Things and other industries, formed a huge economic ecology based on the underlying blockchain. Next, DDN will also be online at major domestic and international exchanges, promote a depth development of the Value Internet .
Would like to know the latest Data Delivery Network price? Here is it as well as other useful data about this kind of cryptocurrency. At NEIRONIX, we collect and provide any valuable content on it such as 1 DDN to USD so that you could make a favorable investment and have a positive result. We invite you to the world of Data Delivery Network value, by giving a real comprehension of its prospect and worthiness!
Due to NEIRONIX, you will be aware of all the latest news. Firstly, everybody can get acquainted with Data Delivery Network price today – these data are renewed with a high speed as we appreciate your wish to have up-to-date information at hand. Secondly, you are able to look through the following important aspects: market cap shows the collective value of all sold coins, low/high value demonstrates the minimal and maximal value of 1 coin among other stock exchanges, and volume is the total value of transactions on stock in a day. Thus, you won't have a question: 'How much is a Data Delivery Network worth?' All data are thoroughly analyzed and presented for your convenience!
If you keen on Data Delivery Network price chart, we offer it – just choose the period you need (from 1 day to maximum) and get a full analysis of its falls and growth during the appropriate period. To add to it, NEIRONIX disposes of topical news about Data Delivery Network current rate and its possible changes, current Data Delivery Network value with future forecasts and growth perspectives. Thanks to us, you will be notified about the latest tendencies in the chosen cryptocurrency market!


At The British Deer Society, we believe in being open about how we use your information.
A 'cookie' is a small text file that is placed on a user's computer hard drive by a website. There are several types of cookie and the most common are often referred to as 'session' cookies. These are used to keep track of information needed by a user as they travel from page to page within a website. These cookies have a short lifetime and expire within a few minutes of the user leaving the site.
Other types of cookies can be used to track internet activity after the user has left a website. These are either sponsored by organisations external to the website being visited (known as 'third party' cookies) or can originate from the website organisation itself ('first party' cookies). These usually have a long lifetime with several months being quite common. They are 'harvested' and 'refreshed' whenever the user visits a page where the same or a similar cookie is being used.
The British Deer Society uses benign, short lived 'session' cookies and 'first party' cookies to tell whether a website user has logged-in, where to find details that can be used to pre-fill parts of on-line forms and to personalise the user's visit to the website. They are also used to track anonymously which areas of the site are popular and which are not used; this allows us to target carefully our website resources.


text:
KCGE/CGE - Cambridge Dorchester Airport
Cambridge, United States
Cambridge–Dorchester Regional Airport (IATA: CGE, ICAO: KCGE, FAA LID: CGE) is a county-owned, public-use airport located three nautical miles (6 km) southeast of the central business district of Cambridge, in Dorchester County, Maryland, United States. Amber L. Hulsey, A.B.D, ASC is the Airport Director. == Facilities and aircraft == Cambridge–Dorchester Regional Airport covers an area of 555 acres (225 ha) at an elevation of 20 feet (6 m) above mean sea level.
(Airport Infos by Wikipedia)
Open current view/airport in an external service:
OurAirports.com
Random Airports
This app shows satellite views of random airports. Its aim is to introduce you to the variety of airport structures embedded into the landscape.
Click on the satellite image or on the button in the control panel to advance to another randomly selected airport.
Click on the button in the control panel to start auto play mode (every 30 seconds a random airport is loaded); Click on the button to stop the auto play mode.
Click on the button in the control panel to search for a specific airport by ICAO code, IATA code, airport name, or location name.
Click on the button in the control panel to show additional information about the current airport and to open the current view in a variety of external services (e.g. Google Maps).
Click on the button in the control panel to toggle fullscreen mode.
Unlike other mapping websites, it is not possible to change the view by panning it around with the mouse or to change the zoom factor.
Technologies and Data Sources
This app is based on the Google Maps API, which on the one hand provides a powerful programming interface for web-based mapping applications, and on the other hand opens access to high quality satellite imagery for places all over the world.
The backend is realized in Python with the help of the excellent Flask micro framework.
The locations of airports have been imported from the public domain data provided by the aviation enthusiasts at OurAirports.com. The app displays randomly selected airports of the categories 'large_airport','medium_airport' and 'small_airport' for which runway coordinates are available.
Furthermore, the user interface incorporates icons from Font Awesome and fonts from Google Fonts.
This is brought to you by me, Florian Pigorsch. Feel free to contact me via mail. The source code of this app can be found at Github.
Random Airports has been featured on several websites including
the AvGeek Weekly Newsletter on 2015/01/16,
the Maps Mania blog on 2015/01/03
Here's a list of 10 random airports:
SLVM/VLM - Teniente Coronel Rafael Pabón Airport
KZPH/ZPH - Zephyrhills Municipal Airport
DAOI/CFK - Ech Cheliff Airport
KMCI/MCI - Kansas City International Airport
ROKJ/UEO - Kumejima Airport
OEPI - Pump Station 9 Airport
WIOS/SQG - Sintang(Susilo) Airport
KETH - Wheaton Municipal Airport
CYFE/YFE - Forestville Airport
K97M - Ekalaka Airport
Click on the satellite image or on to advance to another randomly selected airport.
Click on start 'auto play' mode (every 30 seconds a random airport is loaded).
Click on to search for a specific airport.
Click on to show infos about the current airport.
Click on to toggle fullscreen mode.
You can search for ICAO-codes (4-letter airport codes, e.g. 'KSFO'), IATA-codes (3-letter airport codes, e.g. 'SFO'), airport and location names (e.g. 'San Francisco').
Search queries containing multiple words and/or non-alphanumeric characters may be problematic - try to keep your query simple (e.g. prefer 'Helsinki' to 'Helsinki Airport')!
Here's a list of 10 randomly selected airports: