 
\documentclass[landscape]{seminar}

%\usepackage{alltt,graphicx,latexsym,color}
\usepackage{alltt,graphicx,fixseminar,latexsym,color}

\definecolor{GreenYellow}{cmyk}{0.15,0,0.69,0}
\definecolor{Yellow}{cmyk}{0,0,1.,0}
\definecolor{Goldenrod}{cmyk}{0,0.10,0.84,0}
\definecolor{Dandelion}{cmyk}{0,0.29,0.84,0}
\definecolor{Apricot}{cmyk}{0,0.32,0.52,0}
\definecolor{Peach}{cmyk}{0,0.50,0.70,0}
\definecolor{Melon}{cmyk}{0,0.46,0.50,0}
\definecolor{YellowOrange}{cmyk}{0,0.42,1.,0}
\definecolor{Orange}{cmyk}{0,0.61,0.87,0}
\definecolor{BurntOrange}{cmyk}{0,0.51,1.,0}
\definecolor{Bittersweet}{cmyk}{0,0.75,1.,0.24}
\definecolor{RedOrange}{cmyk}{0,0.77,0.87,0}
\definecolor{Mahogany}{cmyk}{0,0.85,0.87,0.35}
\definecolor{Maroon}{cmyk}{0,0.87,0.68,0.32}
\definecolor{BrickRed}{cmyk}{0,0.89,0.94,0.28}
\definecolor{Red}{cmyk}{0,1.,1.,0.3}
\definecolor{OrangeRed}{cmyk}{0,1.,0.50,0}
\definecolor{RubineRed}{cmyk}{0,1.,0.13,0}
\definecolor{WildStrawberry}{cmyk}{0,0.96,0.39,0}
\definecolor{Salmon}{cmyk}{0,0.53,0.38,0}
\definecolor{CarnationPink}{cmyk}{0,0.63,0,0}
\definecolor{Magenta}{cmyk}{0,1.,0,0}
\definecolor{VioletRed}{cmyk}{0,0.81,0,0}
\definecolor{Rhodamine}{cmyk}{0,0.82,0,0}
\definecolor{Mulberry}{cmyk}{0.34,0.90,0,0.02}
\definecolor{RedViolet}{cmyk}{0.07,0.90,0,0.34}
\definecolor{Fuchsia}{cmyk}{0.6,1,0,0.2}
\definecolor{Lavender}{cmyk}{0,0.48,0,0}
\definecolor{Thistle}{cmyk}{0.12,0.59,0,0}
\definecolor{Orchid}{cmyk}{0.32,0.64,0,0}
\definecolor{DarkOrchid}{cmyk}{0.40,0.80,0.20,0}
\definecolor{Purple}{cmyk}{0.45,0.86,0,0}
\definecolor{Plum}{cmyk}{0.50,1.,0,0}
\definecolor{Violet}{cmyk}{0.79,0.88,0,0}
\definecolor{RoyalPurple}{cmyk}{0.75,0.90,0,0}
\definecolor{BlueViolet}{cmyk}{0.86,0.91,0,0.04}
\definecolor{Periwinkle}{cmyk}{0.57,0.55,0,0}
\definecolor{CadetBlue}{cmyk}{0.62,0.57,0.23,0}
\definecolor{CornflowerBlue}{cmyk}{0.65,0.13,0,0}
\definecolor{MidnightBlue}{cmyk}{0.98,0.13,0,0.43}
\definecolor{NavyBlue}{cmyk}{0.94,0.54,0,0}
\definecolor{RoyalBlue}{cmyk}{1.,0.50,0,0}
\definecolor{Blue}{cmyk}{1.,1.,0,0.3}
\definecolor{Cerulean}{cmyk}{0.94,0.11,0,0}
\definecolor{Cyan}{cmyk}{1.,0,0,0}
\definecolor{ProcessBlue}{cmyk}{0.96,0,0,0}
\definecolor{SkyBlue}{cmyk}{0.62,0,0.12,0}
\definecolor{Turquoise}{cmyk}{0.85,0,0.20,0}
\definecolor{TealBlue}{cmyk}{0.86,0,0.34,0.02}
\definecolor{Aquamarine}{cmyk}{0.82,0,0.30,0}
\definecolor{BlueGreen}{cmyk}{0.85,0,0.33,0}
\definecolor{Emerald}{cmyk}{1.,0,0.50,0}
\definecolor{JungleGreen}{cmyk}{0.99,0,0.52,0}
\definecolor{SeaGreen}{cmyk}{0.69,0,0.50,0}
\definecolor{Green}{cmyk}{1.,0,1.,0}
\definecolor{ForestGreen}{cmyk}{0.91,0,0.88,0.12}
\definecolor{PineGreen}{cmyk}{0.92,0,0.59,0.25}
\definecolor{LimeGreen}{cmyk}{0.50,0,1.,0}
\definecolor{YellowGreen}{cmyk}{0.44,0,0.74,0}
\definecolor{SpringGreen}{cmyk}{0.26,0,0.76,0}
\definecolor{OliveGreen}{cmyk}{0.64,0,0.95,0.40}
\definecolor{RawSienna}{cmyk}{0,0.72,1.,0.45}
\definecolor{Sepia}{cmyk}{0,0.83,1.,0.70}
\definecolor{Brown}{cmyk}{0,0.81,1.,0.60}
\definecolor{Tan}{cmyk}{0.14,0.42,0.56,0}
\definecolor{Gray}{cmyk}{0,0,0,0.50}
\definecolor{Black}{cmyk}{0,0,0,1.}
\definecolor{White}{cmyk}{0,0,0,0}

\newenvironment{Maude}[1]
{\begin{center}\scriptsize\vspace{0.25ex}\begin{minipage}{#1}\begin{alltt}}
{\end{alltt}\end{minipage}\end{center}}

\newenvironment{Slide}[1]
{
\begin{slide}
\sf
\begin{center}
\textcolor{cyan}{\Large\em #1}
\end{center}
}
{
\end{slide}
}

\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}
\newcommand{\EM}[1]{\textcolor{red}{\em #1}}
\newcommand{\mo}{\in}
\newcommand{\fn}{\rightarrow}
\newcommand{\goesto}{\leftarrow}
\newcommand{\upto}{, \ldots ,}
\newcommand{\sort}{{\it sort}}
\newcommand{\osu}{{\it osu}}
\newcommand{\mgu}{{\it mgu}}
\newcommand{\Nat}{{\it Nat}}
\newcommand{\NzNat}{{\it NzNat}}
\newcommand{\lc}{\lceil}
\newcommand{\rc}{\rceil}

\begin{document}

\begin{Slide}{\huge Unification in Maude}
\begin{center}
\vspace{0.5in}
Steven Eker\\
\vspace{0.5in}
Protocol eXchange Seminar
\end{center}
\end{Slide}


\begin{Slide}{Unification}
\begin{itemize}
\item Unification is essentially solving equations in an abstract setting.
\item Given a signature $\Sigma$, variables $X$ and terms $t_1, t_2\mo
T(\Sigma)$ we want to find substitutions $\sigma : X \fn T(W)$, where
$W$ is some fresh set of variables such that
\[
t_1\sigma = t_2\sigma
\]
\item A unifier $\sigma_1$ is \EM{more general} that a unifier $\sigma_2$
if there is a substitution $\upsilon$ such that $\sigma_1\upsilon =
\sigma_2$. $\sigma_2$ is an \EM{instance} of $\sigma_1$.

\item For most applications we want a \EM{complete set} $C$ of unifiers -
every unifer of $t_1 =_? t_2$ would be an instance of some unifer in
$C$.

\item Computing a minimal $C$ (no redundant unifiers) would be nice
but can be expensive.
\end{itemize}
\end{Slide}

\begin{Slide}{Unification in Maude}
Unification in Maude is complicated by two factors:
\begin{enumerate}
\item Equational theories: rather than equality between substituted
terms we want equality between their congruence classes:
\[
[t_1\sigma]_{E} = [t_2\sigma]_{E} 
\]
where $E$ is a set of axioms supported by Maude.
\item Membership equational logic: assignments to variables in unifiers
must respect the sorts of the variables. In fact we punt on on MEL
(undecideable in general) and just consider order sort algebra.
\end{enumerate}
Either factor on its own:
\begin{enumerate}
\item Results in non-singleton minimal complete sets of unifiers.
\item Bumps the complexity of the decision problem (is there a unifer?)
from linear time to NP-hard.
\end{enumerate}
\end{Slide}


\begin{Slide}{Order-sorted free theory unification}
Given a two free-theory terms $t_1, t_2$ from a pre-regular
order-sorted signature, deciding where thay are unifable, $t_1=_{?}
t_2$, is NP-complete.

To see that the problem is in NP we note that given a putative unifier
$\sigma$:
\begin{enumerate}
\item $t_1\sigma = t_2\sigma$ can be checked in linear time
substitution.
\item The sort of a term $t$ can be computed in polynomial time by
proceeding bottom up and at each operator occurence, looking at all
the operator declarations that have a sufficiently large coarity and
taking the glb of their arities (unique by preregularity).
\item Thus for each assignment $X\goesto t$ in $\sigma$ we can check in
polynomial time that the sort of $t$ is less or equal to the sort of
$X$.
\end{enumerate}
\end{Slide}


\begin{Slide}{NP-hardness}
The basic idea is to encode satisfiability using the following
signature:

\begin{Maude}{4in}
fmod ENCODE is
  sorts True False Value .
  subsort True False < Value .
  op true : -> True .
  op false : -> False .
  op not : True -> False .
  op not : False -> True .
  op and : True True -> True .
  op and : True False -> False .
  op and : False True -> False .
  op and : False False -> False .
  op or : True True -> True .
  op or : True False -> True .
  op or : False True -> True .
  op or : False False -> False .
endfm
\end{Maude}
\end{Slide}

\begin{Slide}{NP-hardness 2}
Let $F$ be any propositional formula over propositions $p_1\upto p_n$.
Translate $F$ into a term $t$ over the signature \verb"ENCODE":
\begin{itemize}
\item Proposition $p_i$ is replaced by a variable $X_i$ of sort \verb"Value".
\item Each propositional connective is replaced by the corresponding
operator.
\end{itemize}
Let $Y$ be a variable of sort \verb"True". Then
the order sorted unification problem $Y =_? t$ has a solution iff $F$
is satisfiable, since $Y$ and $t$ are unifiable iff there is an
assignment of sorts to $X_1\upto X_n$ such that $t$ has sort
\verb"True" and the sort declarations exactly mirror the semantics of
the propositional connectives.
\end{Slide}


\begin{Slide}{Implementation}
Unsorted unification in the free theory is well understood. For
order-sorted unification we:
\begin{itemize}
\item Find the unique unsorted unifier using a standard algorithm.
\item Search for all ways of giving sorts to free variables in the
unifier such that:
\begin{itemize}
\item Each free variable recieves a sort that is less or equal to its
original sort.
\item The term assigned to each bound variable has a sort less or
equal than the sort of that variable.
\end{itemize}
\item For each such assignment of sorts to free variables, compute an
order-sorted unifier by replacing the free variables in the unsorted
unifier by fresh variables of the appropriate sort.
\end{itemize}
\end{Slide}


\begin{Slide}{Top-down constraint propagation}
Consider an assignment $Y:s\goesto t$ in the unsorted unifier. That gives
us an initial constraint that $\sort(t)\leq s$.
\begin{itemize}
\item Suppose $t = f(t_1\upto t_n)$.
\item A declaration $f : s_{1}\ldots s_{n}\fn s'$ of largest arity such
that $s' < s$ gives us a conjunction of new constraints
$\sort(t_1) \leq s_1 \wedge \cdots \wedge\sort(t_n) \leq s_n$.
\item Multiple such declarations leads to a disjunction of
conjunctions.
\item The non-existence of a declaration for $f$ with coarity $\leq s$
leads to failure.
\end{itemize}
The constraints can be percolated down until ultimately we arrive at a
nesting of conjunctions and disjunctions of constraints on the sorts
the free variables for each assignment on the unsorted unifier.
\end{Slide}


\begin{Slide}{Top-down constraint propagation 2}
\begin{itemize}
\item These expressions can be conjuncted together and the result placed in
DNF where each conjunction is a conjunction of constraints the
free variables.
\item Each free variable already has a constraint on it's
sort given by it original declared sort.
\item Multiple constraints on the
same variable can be resolved by a glb computation, possibly producing
several alternatives - or none at all.
\item Thus each of the conjuncts may give rise to 0 or more
order-sorted unifiers.
\end{itemize}
This approach can introduce redundant unifiers.
\end{Slide}


\begin{Slide}{Top-down constraint propagation 3}
Consider the unification problem
\[
f(A:\NzNat, B:\NzNat) =_? f(X:\Nat + Y:\Nat, Y:\Nat + Z:\Nat)
\]
in the signature
\begin{Maude}{4in}
fmod NAT is
  sorts NzNat Nat .
  subsort NzNat < Nat .
  op _+_ : Nat Nat -> Nat .
  op _+_ : NzNat Nat -> NzNat .
  op _+_ : Nat NzNat -> NzNat .
  op 0 : -> Nat .
  op s : Nat -> NzNat .
  op f : Nat Nat -> Nat .
endfm
\end{Maude}
The unsorted unifier is
\[
  A:\NzNat \goesto X:\Nat + Y:\Nat
\]
\[
  B:\NzNat \goesto Y:\Nat + Z:\Nat
\]
\end{Slide}

\begin{Slide}{Top-down constraint propagation 4}
Resolving $\sort(X:\Nat + Y:\Nat) \leq \NzNat$ we get:
\[
  \sort(X) \leq \NzNat \wedge \sort(Y) \leq \Nat \vee
  \sort(X) \leq \Nat \wedge \sort(Y) \leq \NzNat
\]
Similarly resolving $\sort(Y:\Nat + Z:\Nat) \leq \NzNat$ we get:
\[
  \sort(Y) \leq \NzNat \wedge \sort(Z) \leq \Nat \vee
  \sort(Y) \leq \Nat \wedge \sort(Z) \leq \NzNat
\]
Conjuncting these two constraints together and distributing out we
get 4 conjunctions:
\[
\sort(X) \leq \NzNat \wedge \sort(Y) \leq \Nat \wedge \sort(Y) \leq \NzNat \wedge \sort(Z) \leq \Nat
\]
\[
\sort(X) \leq \NzNat \wedge \sort(Y) \leq \Nat \wedge \sort(Y) \leq \Nat \wedge \sort(Z) \leq \NzNat
\]
\[
\sort(X) \leq \Nat \wedge \sort(Y) \leq \NzNat \wedge \sort(Y) \leq \NzNat \wedge \sort(Z) \leq \Nat
\]
\[
\sort(X) \leq \Nat \wedge \sort(Y) \leq \NzNat \wedge \sort(Y) \leq \Nat \wedge \sort(Z) \leq \NzNat
\]
\end{Slide}

\begin{Slide}{Top-down constraint propagation 5}
Resolving the multiple constraints on $Y$ we get
\[
\sort(X) = \NzNat \wedge \sort(Y) = \NzNat \wedge \sort(Z) = \Nat
\]
\[
\sort(X) = \NzNat \wedge \sort(Y) = \Nat \wedge \sort(Z) = \NzNat
\]
\[
\sort(X) = \Nat \wedge \sort(Y) = \NzNat  \wedge \sort(Z) = \Nat
\]
\[
\sort(X) = \Nat \wedge \sort(Y) = \NzNat \wedge \sort(Z) = \NzNat
\]
However the 1st and 4th alternatives are subsumed by the 3rd
alternative so there are only 2 most general unifiers corresponding to the 2nd and 3rd
alternatives.
\end{Slide}

\begin{Slide}{Bottom-up symbolic sort computation}
\EM{Boolean Decision Diagrams} (BDDs) can be viewed as compressed truth tables.
\begin{itemize}
\item For random Boolean functions they are less compact than
truth tables.
\item Boolean functions of interest usually have a lot of structure ---
BDDs can be much more compact than truth tables --- perhaps even
exponentially so if we lucky.
\item Many useful operations (combination by arbitrary Boolean
connective, composition, univeral and existential elimination of
variables, substitution of variables) can be performed efficiently.
\item Many implementations available as open source libraries.
\end{itemize}
\end{Slide}

\begin{Slide}{Bottom-up symbolic sort computation 2}
\begin{itemize}
\item Represent sorts symbolically using BDDs.
\item If a kind has $n$ user sorts we need to represent $n+1$ values and thus need
$\lc(\log_2(n+1)\rc$ BDD variables to represent a sort from this kind.
\item For each operator we precompute the vector of BDDs that encodes its
sort function --- this can be done reasonably efficiently if (as in
Maude) an ordered decision diagram for computing this sort function has
already be generated.
\item For each sort $s$ we precompute the BDD for the relation ${\it lt}_{s}(s') = s'\leq s$.
\item For each kind $k$, we precompute the BDD for the relation $s > s'$.
\end{itemize}
\end{Slide}


\begin{Slide}{Bottom-up symbolic sort computation 3}
\begin{itemize}
\item We represent the sort of each free variable $X:s$ by a vector of BDD 
variables.
\item For each assignment $Y:s'\goesto t$ in the unsorted unifer we can 
bottom-up symbolically compute the sort of $t$ as a vector of BDDs by
using BDD vector composition.
\item We can then compute a BDD for the constraint that $\sort(t)\leq s'$.
\item For each free variable $X:s$ we can also compute a BDD for the
constraint that $sort(X) \leq s$.
\item Conjuncting together both kinds of constraints we arrive a BDD
encoding a relation $\osu$ on the sorts of the free variables that
exactly corresponds to sort assignments yielding order-sorted unifiers.
\end{itemize}
\end{Slide}


\begin{Slide}{Bottom-up symbolic sort computation 4}
\begin{itemize}
\item Often there will be a huge number of such sort assignments and we are
only interested in those yielding most general unifiers.
\item Want to compute a relation $\mgu$ that encodes these sort
assignments.
\item Let vector of kinds on which $\osu$ is defined be $(K_1\upto K_n)$.
\item The sorts in each kind are partially ordered and thus the pointwise
extension of these orderings gives a partial ordering on
$K_1 \times\cdots\times K_n$.
\item For $v, v' \mo K_1 \times\cdots\times K_n$, if $\osu(v)$ and $v'
\leq v$ then $\osu(v')$.
\item Furthermore if $v\neq v'$ then $v' < v$ by antisymmmetry and $v'$ cannot
yield a most general unifier.
\end{itemize}
\end{Slide}

\begin{Slide}{Bottom-up symbolic sort computation 5}
For $v'\mo K_1 \times\cdots\times K_n$, if $\osu(v')$ but $v'$ does not yield a most
general unifier then the must be some unifier, different from $v'$ that
is more general, given by a sort vector $v$. 

Clearly $v \geq v'$ since the more general unifier must be at least as general as that given be $v'$
on every variable position. And we can't have $v = v'$ since we need a
distinct unifier, so $v > v'$.

Thus to compute the relation $\mgu$ that encodes exactly the most general
unifiers we want to compute
\[
\mgu(v) = \osu(v) \wedge \neg( \exists v'.[v' > v \wedge \osu(v')] )
\]
Computation can be expensive since it doubles the number of BDD variables
in the intermediate expressions.
\end{Slide}


\begin{Slide}{Bottom-up symbolic sort computation 6}
We note that if $v' > v$ and $\osu(v')$ then
\begin{enumerate}
\item for all $v''$ such that $v' > v''$, we have $\osu(v'')$; and
\item there must exist some index $j$ at which the sort in $v'$ is great
than the sort in $v$.
\end{enumerate}
Thus there exists a vector $u$ which is equal to $v$ on all components
except $j$ and greater than $v$ on component $j$, and $\osu(u)$.

Thus to assert $\neg( \exists v'.[v' > v \wedge \osu(v')] )$ we form a
conjunction of assertions, one for each of the possible indices $j$:
\[
{\rm for}~j = 1\upto n .[
  \neg ( \exists s .[s > v_j \wedge \osu(v_1\upto v_{j-1}, s,
  v_{j+1}\upto v_n)])
]
\]
Here we existentially quantify over sorts rather than vectors of sorts
so we use fewer additional BDD variables in the intermediate expressions.
\end{Slide}

\begin{Slide}{Bottom-up symbolic sort computation 7}
Having computed a BDD that encodes $\mgu$ we recover the sort
assignments to free variables that result in most general order-sorted
unifiers.
\begin{itemize}
\item We trace the from the root of the BDD to the true terminal.

\item Each such path corresponds to one or more sort assignments, given by the labels on arcs
taken.

\item Where some BDD variable is not mentioned on a path, both the
true and false values must be used, giving rise to multiple
sort assignments.
\end{itemize}
\end{Slide}


\begin{Slide}{Maude Implementation}
\begin{itemize}
\item The unify command has the syntax:
\[
{\tt unify}~[\la{\it limit}\ra] ~{\tt in} ~\la{\it module}\ra : \la{\it term}\ra =? \la{\it term}\ra .
\]
\item $[\la{\it limit}\ra]$ and ${\tt in} ~\la{\it module}$ parts are optional.
\item Terms may only contain free function symbols.
\item Unifiers are returned as subsitutions where all variables in the
original problem are mappped to terms containing 
fresh variables with base names \#1, \#2, \#3.
\item The command
\[
{\tt cont}~\la{\it limit}\ra .
\]
can be used to look for further unifiers if a limit was
originally given.
\end{itemize}
\end{Slide}

\begin{Slide}{Maude Implementation 2}
\begin{itemize}
\item The unify command is reflected by the descent function:
\begin{Maude}{4in}
  op metaUnify : Module Term Term Nat ~> Substitution?
        [special (...)] .
\end{Maude}
\item As with metaMatch(), the last argument controls which solution is
returned.
\item When there are no further unifiers
\begin{Maude}{4in}
  op noMatch : -> Substitution? [ctor] .
\end{Maude}
is returned.
\end{itemize}
\end{Slide}


\begin{Slide}{Next steps}
\begin{itemize}
\item Non-algebraic data types (Strings, Floats, Qids).
\item Iter theory (in order to support number hierarchy).
\item Commutative and AC theories.
\end{itemize}
In the AC case, sort information can be pushed into the unsorted
unification algorithm by computing bounds on what a given variable can
take and using it to prune the Diophantive basis and choice of subsets
drawn from the basis.
\end{Slide}
\end{document}
