\subsection{Edge Annotation}

\subsection{Edge Transformers}

Ordinary BDDs are commonly optimized with \emph{complement edges}.
These edges indicate that the node they terminate in is to
be complemented; if it represents the function $f$ by itself, then
with the complement edge it represents $\neg f$. This allows
for the sharing of common subexpressions and their complements:
so $x\wedge y$ would be represented by the same subgraph as
$\neg x \vee \neg y$. In order to maintain the property of 
canonicity, it is required
that the low edge always be non-complemented. Details can be found
in \cite{somenzi99}.

Where $D$ is binary and $R$ is the set of natural numbers, 
blah blah blah.

The intuitive idea behind edge transformers is that each edge in
the diagram -- and also the root -- is annotated with a transformation
on the range. This transformation is applied pointwise to the function
represented by the terminal node of the edge. As an example, consider
we have a subdiagram representing the arithmetic function $f(x)=3x$. 
If there is a root labelled with the edge transformer $(+7)$, the
combination of incoming edge and node represents the function $3x+7$.

\begin{definition}
Let $D$ be a variable domain and $R$ the range. A set of edge valuations
is a set of functions $F$, each from $R$ to $R$. A decision-diagram
is edge-valued if each edge is labelled with a function $f \in F$.
For any node $v$, $\edge_{v, d_i}$ is the label of the edge $(v,
\child_v(d_i))$.

\end{definition}

The function $f_u$ represented by a decision-diagram node $u$ is still
the 

$$f_u = case(\labl(u), \edge_{u,d_1}(\child_v(1)), \ldots
		       \edge_{u,d_m}(\child_v(m)))$$
\begin{example}

\end{example}

Even if an edge-valued decision diagram is reduced and ordered, it may
not be canonical.

\subsection{Canonicity}

Even with edge transformations as simple as complement edges, there
must be constraints on their placement in order to guarantee canonicity.
If not, there are already two possible ways to represent the one-variable
identity function $x$ (IMAGE: either: inbound complement, low edge to 0
complement, high edge to 0 id, or, low edge to 0 id, high edge complement,
inbound id)

Canonicity is restored by the constraint that the only the high edge
may be complemented. It can be guaranteed for EVDDs and FEVDDs by
an analogous constraint: requiring the low edge to be the identity.


\begin{eqnarray}
|T| = 1 \mbox{; denote the unique element in $T$ by $t$}\\
\forall d \in D \cdot . \exists ! f \in F . d=f(\valu(t)) \\
id \in F \\
\forall f \in F . \exists f^{-1} \in F \\
\end{eqnarray}

Sketch of canonicity proof:

\begin{proof}
The proof proceeds by induction on the number of variables $k$.
Base case. There is a canonical representation for any constant.
  Needed axioms: (1) One distinguished value 
		 (2) For any value x, exactly one edge transformer takes
			the distinguished value onto x.

Induction case. The function is expressed as a case statement of its
cofactors.
By the induction hypothesis, we know that
for each cofactor $f[x_i/d_j]$, there is a canonical (edge, node) pair
$(e_j, u_j)$
such that $f[x_i/d_j]=e_j(f_u)$. 

Either all the $(e_j, u_j)$ are identical, in which case $(e_1, u_1)$ is
the canonical representation for $f$.

Or, we construct a new node $v$ with 
$\child_v(d_j)=u_j$ and $\edge_{v, d_j} = (e_1^{-1}\cdot e_j)$. We show
that this represents $f$: