\documentclass{beamer}

\usepackage{listings}
\usepackage[utf8x]{inputenc}
\usepackage{tikz}
\usetikzlibrary{shapes.misc,decorations.pathmorphing,backgrounds,fit,chains,positioning}

\usepackage{stmaryrd} % \llbracket, \rrbracket
\usepackage{pxfonts}

\usetheme{Boadilla}
\usefonttheme{serif}
\setbeamertemplate{navigation symbols}{}

\usepackage{fourier}

\title{Constraint Grammars}
\author[Thierry Martinez]{Thierry Martinez \\ ~ \\ \emph{Acknowledgments to Rémy
    Haemmerlé\\for the original impulse to this work.}}
\date[2008/07/21]{21 July 2008}
\institute[INRIA]{Contraintes Project--Team, INRIA Paris--Rocquencourt, France}

% Variable-size delimiter pairs
\newcommand{\br}[1]{\left(#1\right)}
\newcommand{\sbr}[1]{\left[#1\right]}
\newcommand{\bbr}[1]{\left\llbracket#1\right\rrbracket}
\newcommand{\cbr}[1]{\left\{#1\right\}}
\newcommand{\vbr}[1]{\left\lvert#1\right\rvert}

\DeclareMathOperator{\definedas}{\stackrel{.}{=}}

\newcommand{\ctxcl}[1]{\mathfrak C[#1]}

\newcommand{\infconj}{~~}
\newcommand{\infrule}[2]{~\begin{array}{c}~#1~\\\hline~#2~\end{array}~}
\newcommand{\powerset}[1]{\mathfrak P(#1)}

\newcommand{\N}{\mathbb N}

\newcommand{\card}[1]{\vbr{#1}}

\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\fv}{fv}
\DeclareMathOperator{\dom}{dom}

\newcommand{\hypergraph}{\mathcal H}

\newcommand{\augmh}{\mathcal H^+}

\newtheorem{proposition}{Proposition}

\begin{document}
\begin{frame}
\titlepage
\end{frame}
\begin{frame}
\frametitle{Outline}
\tableofcontents
\end{frame}
\section{Introduction.}
\begin{frame}
\frametitle{Constraint Sets.}

\begin{description}
\item[Observational confluence] ~~~

\texttt{nil(L) $\backslash$ positive\_list(L) $\Longleftrightarrow$ true.}

\texttt{list(L, H, T) $\backslash$ positive\_list(L)
  $\Longleftrightarrow$}
\\\texttt{~~~~~~~ H > 0, positive\_list(T).}

\begin{itemize}
\item Confluent for queries modelling a list\\ (first arguments of \texttt{list}
tokens are pair-wise distincts).
\item
Non-confluent for queries modelling a tree\\ (with two \texttt{list}
tokens sharing a common first argument).
\end{itemize}
\item[Characterizing (L)CC Stores]
\item[Describing Global Constraints]
Given a set of constraints $S$:
\begin{itemize}
\item either there exists a satisfied constraint in $S$:
  \[\text{$\textsc{regular}(x_1, \dots, x_n, L)$ with $S = \cbr{x_1 = u_1
    \wedge \dots \wedge x_n = u_n}_{u \in L}$}\]
\item or all the constraints of $S$ are satisfied:
  \[\text{$\textsc{all-different}(x_1, \dots, x_n)$ with $S = \cbr{x_i \neq x_j}_{i \neq j}$}\]
\end{itemize}
\end{description}

\end{frame}
\section{Context-Free Constraint Grammars. Definition \&
  Applications.}

\begin{frame}
  \frametitle{Linear Constraint Systems.}

  \color{black}

  Let $V$ be a set of variables.

  \begin{itemize}
  \item If $C$ is a set of formulae over the set of variables $V$, let
    $\ctxcl{C}$ be the closure of $C$ by conjunction ($\otimes$) and
    variable hiding ($\exists$).
  \item If ${\Vdash}$ is a binary relation over $C$, let
    $\widehat{\Vdash}$ be the closure of $\Vdash$ by the rules of linear
    logic.
  \end{itemize}

  \begin{definition}
    A (linear) \textbf{constraint system} is a pair $(C, \vdash)$ where:
    \begin{itemize}
    \item $C$ is a set of formulae closed by conjunction ($\otimes$)
      and variable hiding ($\exists$);
    \item ${\vdash} \subseteq C^2$ is a relation closed by the rules of linear
      logic.
    \end{itemize}
  \end{definition}
\end{frame}

\begin{frame}
  \frametitle{Examples of Constraint Systems}

  \color{black}
Let $\Sigma$ be a signature.  Let $t(\Sigma) \definedas \cbr{f(v_1,
    \dots, v_n) \vert \text{$f/n \in \Sigma$}}$.
\begin{description}

  \item[linear-token system]~\\
  The \textbf{linear-token system} over $\Sigma$ is the constraint system
  $\textsc{tok}(\Sigma) \definedas (\ctxcl{t(\Sigma)}, \widehat{\emptyset})$.

\item[linear-token system with equality]~\\
  The \textbf{linear-token system with equality} over $\Sigma$ is the
  constraint system $\textsc{tok}_=(\Sigma) \definedas (\ctxcl{t(\Sigma) \cup \cbr{!(x = y \vert x, y
      \in V)}}, \widehat{\Vdash})$, where $\Vdash$ is the smallest
  relation with the axioms of the equality theory:

  $\Vdash !(x = x)$; $!(x = y)
  \Vdash !(y = x)$; $!(x = y) \otimes !(y = z) \Vdash !(x = z)$;

  $f(x_0, \dots, x_n) \otimes !(x_0 = y_0) \otimes \dots \otimes !(x_n
  = y_n) \Vdash f(y_0, \dots, y_n)$

\end{description}
\end{frame}

\begin{frame}
\frametitle{Context-Free Constraint Grammars (CFCG).}

  \color{black}

\begin{definition}
  A \textbf{context-free constraint grammar} (CFCG) is a tuple $(V, C,
  \vdash, \Sigma, P)$ where:
  \begin{itemize}
  \item $V$ is a set of variables and $(C, \vdash)$ is a constraint-system over $V$;
  \item $\Sigma$ is the signature of non-terminal symbols:\\
    $N \definedas \cbr{f(y_1, \dots, y_n) \vert \text{$f/n \in \Sigma$
        and $y_1, \dots, y_n \in V$ pair-wise distincts}}$
  \item $P \subseteq N \times \overline{C}$ is the set of
    productions, with $\overline{C} \definedas \ctxcl{C \cup N}$.

    Every production $(f(y_1, \dots, y_n), u) \in P$ is such that
    $\fv(u) \subseteq \cbr{y_1, \dots, y_n}$.

    A production is denoted:
    $f(y_1, \dots, y_n) \Coloneqq u$.
  \end{itemize}  
\end{definition}

\color{black}

\vspace{0.5cm}

\textbf{Example:}
\begin{align*}
h(X, Y)& \Coloneqq \text{edge}(X, Y)\\
h(X, Y)& \Coloneqq \exists Z . \text{edge}(X, Z) \otimes h(Z, Y)
\end{align*}

\end{frame}

\begin{frame}
  \frametitle{Derivations for CFCGs.}

  \color{black}

    Let $(V, C, \vdash, \Sigma, P)$ be a context-free constraint grammar.
    Let $\overline{C} \definedas \ctxcl{C \cup N}$.

  \begin{definition}
    Let ${\rightarrow} \subseteq \overline{C}^2$ be the smallest
    relation satisfying the following rules:
    \[
    \infrule{f(y_1, \dots, y_n) \Coloneqq u}{(f(y_1, \dots,
      y_n))\sigma \rightarrow (u)\sigma}
    \infrule{u \rightarrow v}{\exists x . u \rightarrow \exists x v}
    \infrule{u \rightarrow v}
    {u \otimes w \rightarrow v \otimes w}
    \infrule{u \rightarrow v}
    {w \otimes u \rightarrow w \otimes v}
    \]

    A derivation is a sequence $(c_i)_i$ with elements in
    $\overline{C}$ such that $c_0 \rightarrow c_1 \rightarrow \dots$.
  \end{definition}

\color{black}

\vspace{0.2cm}

\textbf{Example:}

\vspace{-0.5cm}

\begin{align*}
h(X, Y)& \Coloneqq \text{edge}(X, Y)\\
h(X, Y)& \Coloneqq \exists Z . \text{edge}(X, Z) \otimes h(Z, Y)
\end{align*}

\vspace{-0.5cm}
\begin{align*}
h(A, B) &\rightarrow \exists X_1 . \text{edge}(A, X_1) \otimes h(X_1, B)
 \\&\rightarrow \exists X_1 X_2 . \text{edge}(A, X_1) \otimes \text{edge}(X_1, X_2)
 \otimes h(X_2, B) \\&\rightarrow \exists X_1 X_2 . \text{edge}(A, X_1) \otimes
 \text{edge}(X_1, X_2) \otimes \text{edge}(X_2, B)
\end{align*}
\end{frame}

\begin{frame}
  \frametitle{Languages accepted by CFCGs.}

  \color{black}

    Let $G \definedas (V, C, \vdash, \Sigma, P)$ be a context-free
    constraint grammar.  Let $\overline{C} \definedas \ctxcl{C \cup
      N}$.

  \begin{definition}
    The \textbf{constraint language} accepted by a schema $c_0 \in
    \overline{C}$ and the grammar $G$ is:
    \[L_G(c_0) = \cbr{c \in C \vert (\exists n)(\exists (c_i)_{0 \leq i \leq n})
      (c_0 \rightarrow \dots \rightarrow c_n \wedge c_n \dashv \vdash
    c)}\]
  \end{definition}

  \color{black}

\vspace{0.2cm}

\textbf{Example:}

\vspace{-0.5cm}

\begin{align*}
h(X, Y)& \Coloneqq \text{edge}(X, Y)\\
h(X, Y)& \Coloneqq \exists Z . \text{edge}(X, Z) \otimes h(Z, Y)
\end{align*}
\vspace{-0.3cm}
\[L_G(h(A, B)) = \cbr{\text{hamiltonian paths from $A$ to $B$}}\]
  
\end{frame}

\begin{frame}
  \frametitle{Link with Hyperedge Replacement Graph Grammars.}

  \begin{block}{Claim}
    Over linear token systems, context-free constraint grammars have
    the same expressive power than hyperedge replacement graph grammars.
  \end{block}

  \color{black}

  H. Ehrig, M. Nagl, and G. Rozenberg, editors. \emph{Graph Grammars and Their Application 
    to Computer Science}, Lect. Notes Comp. Sci. 153. Springer, 1983. 

  \begin{theorem}[K.-J. Lange and E. Welzl 87]
    Hyperedge replacement graph language membership problem is
    NP-complete.
  \end{theorem}
\end{frame}

\begin{frame}
  \frametitle{Hypergraphs.}

  \color{black}

    A \textbf{labelled set} $\dot E$ is a tuple $(E, E^{\Sigma},
    E^{\lambda})$, with $E^{\Sigma}$ alphabet and $E^{\lambda}
    : E \rightarrow E^{\Sigma}$.

  \begin{definition}
    A \textbf{hypergraph} is a tuple $(V, \dot E, S, \rightarrow)$,
    where:
    \begin{itemize}
    \item $V$ is the set of vertices; $\dot E$ is the labelled set of hyperedges;
    \item $S$ is the alphabet of selectors;
    \item ${\rightarrow} \subseteq E \times S \times V$ is the incidence
      relation.  $(e, s, v) \in {\rightarrow}$ is denoted
      $e \stackrel{s}{\rightarrow} v$.

      $\rightarrow$ is functional: $(\forall e ~ s ~ v_1 ~ v_2) e
      \stackrel{s}{\rightarrow} v_1 \wedge e \stackrel{s}{\rightarrow}
      v_2 \Rightarrow v_1 = v_2$
    \end{itemize}

    Vertices are represented as fat dots, hyperedges as boxes.
  \end{definition}

  \color{black}

  Let $\hypergraph(V, E, S)$ the set of hypergraphs over $V, E, S$.
\vspace{-0.2cm}
\begin{center}
  \begin{tikzpicture}[
    node/.style={
      circle,
      fill=black
    },
    edge/.style={
      rectangle,
      draw=black
    }
    ]
    \matrix[ampersand replacement=\&,row sep=7mm,column sep=7mm]{
                     \& \node (na) [node] {}; \& \node (eb) [edge] {b}; \& \node (ne) [node] {}; \\
\node (nb) [node] {}; \& \node (ea) [edge] {a}; \& \node(nd) [node] {};\\
                     \& \node (nc) [node] {};\\
    };
    \path (na) edge node[auto]{1} (eb);
    \path (na) edge node[auto]{1} (ea);
    \path (eb) edge node[auto]{2} (ne);
    \path (eb) edge node[auto]{2} (nd);
    \path (nb) edge node[auto]{0} (ea);
    \path (ea) edge node[auto]{2} (nd);
    \path (ea) edge node[auto]{3} (nc);
  \end{tikzpicture}
\end{center}
\end{frame}

\begin{frame}
  \frametitle{Embedding of Hypergraphs into Constraints.}

  \color{black}

  Let $H = (V, \dot E, S, \rightarrow)$ be a hypergraph.
  \begin{itemize}
  \item For all $e \in E$, let $\dom(e) \definedas \cbr{s \in S \vert (\exists
    v \in V)(e \stackrel{s}{\rightarrow} v)}$.

  \item Let $n(e) \definedas \card{\dom(e)}$ and $r_e : \cbr{1, \dots, n(e)
  \hookrightarrow \dom(e)}$.

  \item Let $\Sigma \definedas \cbr{f/n \in E^{\Sigma} \times \N \vert
    (\exists e \in E)(\text{$f = E^\lambda(e)$ and $n = n(e)$})}$.
  \end{itemize}

  \begin{definition}
    The \textbf{constraint-embedding} of the hypergraph $h$ is the
    following constraint of $\textsc{tok}(\Sigma)$:
    \[\bbr{h} \definedas (\exists v_1 \dots v_n) \br{\bigotimes_{e \in
        E \wedge n = n(e) \wedge y_i = r_e(i)}
    [E^{\lambda}(e)](y_1, \dots, y_n)}\]
  \end{definition}

  \begin{proposition}
    For every closed constraint $c \in \textsc{tok}(\Sigma)$, there
    exists a hypergraph $h$ such that \[\bbr{h} \dashv\vdash c\]
  \end{proposition}

\end{frame}

\begin{frame}
  \frametitle{Hypergraph Isomorphism.}

  \begin{definition}
  Two hypergraphs $h_0 \definedas (V, (E, E^{\Sigma}, E^{\lambda}_0), S, \rightarrow_0)$
  and $h_1 \definedas (V, (E, E^{\Sigma}, E^{\lambda}_1), S, \rightarrow_1)$ are
  \textbf{isomorphic}, denoted $h_0 \simeq h_1$, when there exist
  $\sigma_V : V \hookrightarrow V$ and $\sigma_E : E \hookrightarrow
  E$ such that:
  \begin{itemize}
  \item $(\forall e \in E)(E^{\lambda}_0(e) = E^{\lambda}_1(\sigma_E(e)))$;
  \item $(\forall e \in E)(\forall s \in S)(\forall v \in V)(e
    \stackrel{s}{\rightarrow_0} v \Longleftrightarrow (\sigma_E(e)
    \stackrel{s}{\rightarrow_1} \sigma_V(v))$.
  \end{itemize}
  \end{definition}

  \begin{proposition}
    \[h_0 \simeq h1 \Longleftrightarrow \bbr{h_0} \dashv\vdash \bbr{h_1}\]
  \end{proposition}
\end{frame}

\begin{frame}
  \frametitle{Hyperedge Replacement Graph Grammars (HRGs).}

  \color{black} Let $N, V, E, E^{\Sigma}, S$ be defined
  accordingly to the following definition.

  We denote $\augmh(N, V, E, E^{\Sigma}, S)$ the set of
  \textbf{augmented hypergraphs}, that is hypergraphs whose edges are
  labelled with $\widehat{E}^{\Sigma}$ and vertices are in
  $\widehat{V}$.

  \begin{definition}
    A \textbf{h-edge replacement graph grammar} is a tuple $(N,
    V, E, E^{\Sigma}, S, P)$, with:
    \begin{itemize}
    \item $N$ is the alphabet of non-terminals, such that $E^{\Sigma} \cap N =
      \emptyset$; $\widehat{E}^{\Sigma} \definedas E^{\Sigma} \uplus N$;
    \item $V$ is the set of vertices;
    \item $E$ is the set of hyperedges and $E^{\Sigma}$ the set of
      ground labels;
    \item $S$ is the alphabet of selectors, such that $V \cap S =
      \emptyset$; $\widehat{V} \definedas V \uplus S$;
    \item $P \subseteq N \times \powerset{S} \times
      \augmh(N, V, E, E^{\Sigma}, S)$ is the set of productions.
    \end{itemize}
  \end{definition}

\vspace{-0.2cm}
\color{black}

\begin{center}
  \begin{tikzpicture}[
    node/.style={
      circle,
      fill=black
    },
    edge/.style={
      rectangle,
      draw=black
    }
    ]
    \matrix[ampersand replacement=\&,row sep=4mm,column sep=4mm]{
 \node (nx) [node] {}; \& \& \node (nx1) [node,label=left:0] {}; \& \& \& \& \node (nx2) [node] {}; \& \& \node (nx3) [node,label=left:0] {}; \& \node (ee) [edge] {e}; \& \node (na) [node] {}; \\
 \node (eh) [edge,fill=yellow] {H}; \& \node {$\Coloneqq$}; \& \node (eh1) [edge] {e}; \& \& \node{;}; \& \&\node (eh2) [edge,fill=yellow] {H}; \& \node {$\Coloneqq$}; \& \& \& \node (eh3) [edge,fill=yellow] {H};\\
 \node (ny) [node] {}; \& \& \node (ny1) [node,label=left:1] {}; \& \& \& \& \node (ny2) [node] {}; \& \& \& \& \node (ny3) [node,label=left:1] {};\\
    };
    \path (nx) edge node[auto]{0} (eh);
    \path (eh) edge node[auto]{1} (ny);
    \path (nx1) edge node[auto]{0} (eh1);
    \path (eh1) edge node[auto]{1} (ny1);
    \path (nx2) edge node[auto]{0} (eh2);
    \path (eh2) edge node[auto]{1} (ny2);
    \path (nx3) edge node[auto]{0} (ee);
    \path (ee) edge node[auto]{1} (na);
    \path (na) edge node[auto]{0} (eh3);
    \path (eh3) edge node[auto]{1} (ny3);
  \end{tikzpicture}
\end{center}
\end{frame}

\begin{frame}
  \frametitle{Derivations for HRGs.}

  \color{black}

    Let $(N, V, E, E^{\Sigma}, S, P)$ be a hyperedge replacement
    graph grammar.


  \begin{definition}
    Let ${\rightarrow} \subseteq \augmh(N, V, E, E^{\Sigma},
    S)^2$ be the relation such that: $(V_0, \dot{E_0}, S,
    {\rightarrow_0}) \rightarrow (V_1, \dot{E_1}, S,
    {\rightarrow_1})$ iff there exist:
    \begin{itemize}
    \item a hyperedge $e \in E_0$; a production $(n, S_p, (V_p,
      \dot{E_p}, S, {\rightarrow_p})) \in P$;
    \item
       $\sigma^E_{0 \rightarrow 1} : E_0 \setminus \cbr{e}
        \hookrightarrow E_1$,
       $\sigma^V_{0 \rightarrow 1} : V_0 \hookrightarrow V_1$,
       $\sigma^E_{p \rightarrow 1} : E_p \hookrightarrow E_1$,
       $\sigma^V_{p \rightarrow 1} : V_p \setminus S \hookrightarrow V_1$
    \end{itemize}
    such that:
    \begin{itemize}
    \item $E^{\lambda}_0(e) = n$; $\im(\sigma^E_{0 \rightarrow 1}) \uplus \im(\sigma^E_{p
        \rightarrow 1}) = E_1$ and $\im(\sigma^V_{0 \rightarrow 1}) \uplus
      \im(\sigma^V_{p \rightarrow 1}) = V_1$;
    \item $(\forall e_0 \in E_0 \setminus \cbr{e})(\forall e_p \in
      E_p)(\forall s ~ s' \in S)(\forall v_0 \in V_0)(\forall v_p \in
      V_p \setminus S)$
      \begin{columns}
        \column{4cm}
        \begin{align*}
          E^{\lambda}_0(e_0) & = E^{\lambda}_1(\sigma^E_{0 \rightarrow
            1}(e_0))\\
          E^{\lambda}_p(e_p) &= E^{\lambda}_1(\sigma^E_{p \rightarrow
            1}(e_p))
        \end{align*}
        \column{5cm}
        \begin{align*}
          e_0 \stackrel{s}{\rightarrow_0} v_0 & \Longleftrightarrow
          \sigma^E_{0 \rightarrow 1}(e_0) \stackrel{s}{\rightarrow_1}
          \sigma^V_{0 \rightarrow 1}(v_0)\\
          e_p \stackrel{s}{\rightarrow_p} v_p & \Longleftrightarrow
          \sigma^E_{p \rightarrow 1}(e_p) \stackrel{s}{\rightarrow_1}
          \sigma^V_{p \rightarrow 1}(v_p)\\
          e \stackrel{s}{\rightarrow_0} v_0 \wedge e_p
          \stackrel{s'}{\rightarrow_p} s & \Longleftrightarrow
          \sigma^E_{p \rightarrow 1}(e_p) \stackrel{s'}{\rightarrow_1}
          \sigma^V_{0 \rightarrow 1}(v_0)
        \end{align*}
      \end{columns}
    \end{itemize}
  \end{definition}
\end{frame}

\begin{frame}
  \frametitle{Embedding of HRGs into CFCGs.}

  \color{black}

  Let $G \definedas (N, V, E, E^{\Sigma}, S, P)$ be a hyperedge replacement
  graph grammar.

  \begin{enumerate}
  \item $\bbr{\bullet}$ can be extended to an embedding of augmented
    hypergraphs into scheme of $\overline{C}$, with $N \definedas
    \cbr{f(y_1, \dots y_n) \vert (\exists h)((f, \cbr{y_1, \dots,
        y_n}, h) \in P)}$;
  \item therefore $\bbr{\bullet}$ can be extended to an embedding of
    HRG productions into context-free constraint productions;
  \item therefore $\bbr{\bullet}$ can be extended to an embedding of
    HRG grammars into context-free constraint grammars.
  \end{enumerate}

  \begin{definition}
    The \textbf{hypergraph language} accepted by an augmented hypergraph $h_0 \in
    \augmh(N, V, E, E^{\Sigma}, S)$ and the grammar $G$ is:
    \[L_G(h_0) = \cbr{h \in \hypergraph(V, E, S) \vert (\exists n)(\exists (h_i)_{0 \leq i \leq n})
      (h_0 \rightarrow \dots \rightarrow h_n \wedge h \simeq
        h_n)}\]
  \end{definition}

  \begin{proposition}
    For all $h_0 \in \augmh(N, V, E, E^{\Sigma}, S)$, we have
    $\bbr{L_G(h)} = L_{\bbr{G}}(\bbr{h})$.
  \end{proposition}
\end{frame}

\begin{frame}
  \frametitle{With Equality Theory.}

\color{black}
  \textbf{Lemma}:
    for all constraint $c \in \textsc{tok}_=(\Sigma)$, there exists a
    constraint $c' \in \textsc{tok}(\Sigma) \subseteq
    \textsc{tok}_=(\Sigma)$ such that $c \dashv \vdash c'$.

  \begin{proposition}
    For every closed constraint $c \in \textsc{tok}_=(\Sigma)$, there
    exists a hypergraph $h$ such that \[\bbr{h} \dashv\vdash c\]
  \end{proposition}

\color{black}
  \textbf{Lemma}:
    For a schema $c \in \overline{\textsc{tok}_=(\Sigma)}$ and a
    grammar $G$ over $\textsc{tok}_=(\Sigma)$, there exists $c' \in
    \overline{\textsc{tok}(\Sigma)}$ and a $G'$ over
    $\textsc{tok}(\Sigma)$ such that:
    \[L_G(c) = \cbr{h \in \textsc{tok}_=(\Sigma) \vert \exists h' \in
      L_{G'}(c'), h \dashv \vdash h'}\]

  \begin{proposition}
    Over $\textsc{tok}_=(\Sigma)$, context-free constraint language
    membership problem is NP-complete.
  \end{proposition}
\end{frame}

\begin{frame}
  \frametitle{Applications to Global Constraints.}
  \color{black}

  Let $A$ be an alphabet.  Every $u = u_1 \cdots u_n \in A^*$ can be represented as a
  string-hypergraph:

\begin{center}
  \begin{tikzpicture}[
    node/.style={
      circle,
      fill=black
    },
    edge/.style={
      rectangle,
      draw=black
    }
    ]
    \matrix[ampersand replacement=\&,row sep=7mm,column sep=7mm]{
                    \node (n0) [node] {}; \& \node (e1) [edge] {$u_1$}; \& \node (n1) {$\cdots$}; \& \node (e2) [edge] {$u_n$}; \& \node (n2) [node] {}; \\
    };
    \path (n0) edge node[auto]{0} (e1);
    \path (e1) edge node[auto]{1} (n1);
    \path (n1) edge node[auto]{0} (e2);
    \path (e2) edge node[auto]{1} (n2);
  \end{tikzpicture}
\end{center}


  \begin{proposition}[Habel and Kreowski 87]
    Every context-free string language $G$ can be recognized by a
    hyperedge replacement graph grammar $\bbr{G}$.
  \end{proposition}

  \color{black}
  \textbf{Corollary}: Every context-free string language $G$ can be recognized by a
    context-free constraint grammar $\bbr{G}$.

  \begin{proposition}
    \[\textsc{context-free}(x_1, \dots, x_n, G) \definedas (\exists) \bbr{G}(x_1, \dots, x_n)\]
  \end{proposition}
\end{frame}

\begin{frame}
  \frametitle{Limitations.}
  \color{black}

  \begin{definition}
\begin{columns}
\column{7cm}
    A \textbf{jungle} is a hypergraph $(V, \dot E, \cbr{\text{in$_k$}, \text{out}}, \rightarrow)$
    such that:
    \begin{itemize}
    \item $(\forall v \in V)\br{\card{\cbr{e \in E \vert e
          \stackrel{\text{out}}{\rightarrow} v}} \leq 1}$;
    \item $\rightarrow$ is acyclic.
    \end{itemize}
\column{3cm}
\vspace{-1cm}
\begin{center}
  \begin{tikzpicture}[
    node/.style={
      circle,
      fill=black
    },
    edge/.style={
      rectangle,
      draw=black
    }
    ]
    \matrix[ampersand replacement=\&,row sep=2mm,column sep=7mm]{
      \& \node (ef) [edge] {f};\\
      \& \& \node (n2) [node] {};\\
      \node (n1) [node] {}; \& \& \node (eg) [edge] {g}; \\
      \& \& \node (n3) [node] {};\\
      \node (ea) [edge] {a}; \& \& \node (eb) [edge] {b}; \\
    };
    \path (ef) edge node[auto]{\tiny in$_0$} (n1);
    \path (ef) edge node[auto]{\tiny in$_1$} (n2);
    \path (n1) edge node[auto]{\tiny out} (ea);
    \path (n2) edge node[auto]{\tiny out} (eg);
    \path (eg) edge node[auto]{\tiny in$_0$} (n1);
    \path (eg) edge node[auto]{\tiny in$_1$} (n3);
    \path (n3) edge node[auto]{\tiny out} (eb);
  \end{tikzpicture}\\
  \vspace{-0.6cm}
  f(a,g(a,b))
\end{center}
\end{columns}
  \end{definition}
\vspace{-0.2cm}
  \color{black}
  F. Raiser and T. Frühwirth, \emph{Towards Term Rewriting Systems in
    Constraint Handling Rules -- Coming to terms with jungles},
  Proceedings of the Fifth Workshop on Constraint Handling Rules,
  2008.

  ``\textbf{Corollary 2:} CHR folding is terminating and confluent.''
  
  \emph{Only true if the query is a jungle!}

  \begin{proposition}
    $\cbr{h \in \hypergraph(V, E, S) \vert \text{$h$ is a jungle}}$ is
    not a hyperedge replacement graph language.
  \end{proposition}

\end{frame}

\section{Domain-Sensitive Constraint Grammars. Definitions \&
  Applications.}
\begin{frame}
  \frametitle{Domain-Sensitive Constraint Grammars. (1/2)}

  \color{black}

  A \textbf{two-sorted signature} $\Sigma$ is a subset of $F \times \N \times
  \N$, where $F$ is a countable symbol set.  Items $(f,n,m) \in
  \Sigma$ are denoted $f/(n,m)$.

  Let $V$ and $W$ be two set of variables and $L$ a set of labels.

  The \textbf{set constraint system} is the smallest \emph{classical}
  constraint system $(S, \vdash_S)$ such that:
  {
    \[
    \infrule{w \in W}{w = \emptyset \in S}~~
    \infrule{v \in V \infconj w \in W}{w = \cbr{v} \in S}~~
    \infrule{v \in V \infconj w \in W}{(v \in w) \in S}~~
    \infrule{w \in W \infconj l \in L}{w = \fv{l} \in S}
    \]
    \[
    \infrule{w_1 \in W \infconj w_2 \in W \infconj w_3 \in W}{w_1 = w_2 \textit{ op } w_3 \in
      S}\text{$\textit{op} \in \cbr{{\cap}, {\cup}, {\setminus}}$}~~
    \]
    with $w = \cbr{v} \vdash_S v \in w$ ~~ $w = \emptyset \vdash_S v
    \notin w$\\and $v \in w_1 \textit{ op$_1$ } v \in w_2 \vdash_S v \in
    w_1 \textit{ op$_2$ } w_2$ with $(\textit{op$_1$},
    \textit{op$_2$}) \in \cbr{({\wedge}, {\cap}); ({\vee}, {\cup});
      ({\wedge ¬}, {\cap})}$\dots }
\end{frame}

\begin{frame}
  \frametitle{Domain-Sensitive Constraint Grammars. (2/2)}

  \color{black}

  \begin{definition}
  A \textbf{domain-sensitive constraint grammar} (DSCG) is a tuple
  $(V, W, L, C,
  \vdash, \Sigma, P)$ where:
  \begin{itemize}
  \item $V, W$ are sets of variables, $L$ a set of labels;
  \item $(C, \vdash)$ is a constraint-system over $V$;
  \item $\Sigma$ is the two-sorted signature of non-terminal symbols:\\
    {\small $N \definedas \cbr{l:f(y_1, \dots, y_n, Y_1, \dots, Y_m)
        \vert \text{$l \in L$, $f/(n,m) \in \Sigma$
        and $\begin{array}{c}y_1, \dots, y_n \in V\\Y_1, \dots, Y_m \in W\end{array}$ p.-w. dist.}}$}
  \item $P \subseteq N \times \overline{C} \times S$ is the set of
    productions, with $\overline{C} \definedas \ctxcl{C \cup N}$.

    A production is denoted:
    $f(y_1, \dots, y_n, Y_1, \dots, Y_m) \Coloneqq u \vert g$.
  \end{itemize}      
  \end{definition}
\end{frame}


\begin{frame}
  \frametitle{Applications of DSCGs.}

  \color{black}

  \begin{description}
    \item[Jungles]

  Let $\Sigma$ be a signature.  For all $f/n \in \Sigma$:
\end{description}
  \[
  j(r) \Coloneqq \text{eq}(r, f(x_1, \dots,
  x_n)) \otimes l_1:j(x_1) \otimes \dots \otimes l_n:j(x_n)
  \vert r \notin \fv(l_1) \cup \cdots \cup \fv(l_n)
  \]

  \begin{description}
\vspace{1cm}
\item[all-different]
  \[a(S) \Coloneqq x_1 \neq x_2 \vert x_1 \in S \wedge x_2 \in S
  \setminus \cbr{x_1}\]

  \[\textsc{all-different}(x_1, \dots x_n) \definedas (\forall) a(\cbr{x_1,
    \dots, x_n})\]
\end{description}
\end{frame}

\section{Conclusions \& Perspectives.}
\begin{frame}
\frametitle{Conclusions \& Perspectives.}
\begin{description}
\item[Objective]~~~~~~~~~~~~~~~~~~
  \begin{itemize}
    \item Describing set of constraints;
    \item for observational confluence;
    \item for defining global constraints.
  \end{itemize}
\item[Contributions]~~~~~~~~~~~~~~
  \begin{itemize}
  \item Definition of constraint grammar;
  \item as expressive as hyperedge-replacement graph grammar;
  \item much more easy to define;
  \item more general.
  \end{itemize}
\item[Future work]~~~~~~~~~~~~~~~
  \begin{itemize}
  \item Decidability and complexity analysis for other constraint
    systems.
  \end{itemize}
\end{description}
\end{frame}
\end{document}