the [*computability*]{} of the function [$f^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}$]{}, so that encoders can indeed be used for performing dynamic programming.

\[defi:encod\] An *encoder* is a triple ${{\ensuremath{{\mathcal}{E}_{}}\xspace}}= ({\ensuremath{{\mathcal}{C}^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace},{\ensuremath{L^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace},{\ensuremath{f^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace})$ where

-   is a function in $2^\mathbb{N} \to 2^{\Upsilon^*}$ that maps a finite subset of integers $ I \subseteq \mathbb{N}$ to a set ${\ensuremath{{\mathcal}{C}^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace}(I)$ of strings over some alphabet $\Upsilon$. Each string $R \in {\ensuremath{{\mathcal}{C}^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace}(I)$ is called an *encoding*. The *size* of the encoder is the function $s_{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}} : \mathbb{N} \to \mathbb{N}$ defined as $s_{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}(t)  :=  \max \{|{\ensuremath{{\mathcal}{C}^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace}(I)| : I \subseteq \{1,\ldots,t\}\} $, where $|{\ensuremath{{\mathcal}{C}^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace}(I)|$ denotes the number of encodings in ${\ensuremath{{\mathcal}{C}^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace}(I)$;

-   is a computable language which accepts triples $(G,{\cal S},R)\in \Gamma^* \times \Sigma^* \times \Upsilon^*$, where $G$ is a boundaried graph, ${\cal S}$ is a collection of subgraphs of $G$ and $R \in {\ensuremath{{\mathcal}{C}^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace}(\Lambda(G))$ is an encoding. If $(G,{\cal S},R)\in {\ensuremath{L^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace}$, we say that ${\cal S}$ *satisfies* the encoding $R$ in $G$; and

-   is a computable function in $\Gamma^* \times \Upsilon^* \to \mathbb{N}\cup\{ -\infty\}$ that maps a boundaried graph $G$ and an encoding $R\in {\ensuremath{{\mathcal}{C}^{{{\ensuremath{{\mathcal}{E}_{}}\xspace}}}}\xspace}(\Lambda(G))$ to an integer or to $-\infty$.

As it will become clear with the applications described in the next sections, an encoder is a formalization of the tables 