foundations.tex

%\newcommand{\emptysmodel}[0]{$\textbf{\LARGE{X}}$}
%\usetikzlibrary {positioning}
%\newcommand{\setsets}[1]{\boldsymbol{#1}}
%\newcommand{\App}[1]{\ensuremath{A_{#1}}}
%\newcommand{\A}[2]{\App{#1}#2}
%\newcommand{\fixp}[1]{#1^{\star}}
%\newcommand{\Appfixp}[1]{\ensuremath{\fixp{A_{#1}}}}
%\newcommand{\Afixp}[2]{\Appfixp{#1}#2}
%\newcommand{\Appi}[2]{\ensuremath{A_{#1}^{#2}}}
%\newcommand{\Ai}[3]{\Appi{#1}{#2}#3}

%\newcommand{\myinput}[1]{
%\ifx\inlibrary\undefined
%  \input{#1}
%\else
%  \input{../#1}
%\fi
%}

\newcommand{\xtodo}[0]{
\begin{tikzpicture}[remember picture,overlay]
    \node[draw, very thick, rounded corners, xshift=-1.3cm,yshift=-2cm] at (current page.north east)
    {TO DO};
\end{tikzpicture}
}

%%%\tikzset{% 
%%%    examples/.style={%
%%%%, >={Stealth[round]}
%%%%->
%%%, x=1.5cm
%%%, y=-1.5cm
%%%, smodel/.style={rectangle,minimum size=0.5cm,draw,thin, rounded corners, ellipse}
%%%%, empty/.style={minimum size=7mm}
%%%, arrow/.style={<-,thin}
%%%%, empty_arrow/.style={arrow,dotted,draw=none} % dashed
%%%, rule/.style={align=center}
%%%, rule_dep/.style={align=center, draw}
%%%, rule_arrow/.style={<-}
%%%, rule_arrow_neg/.style={rule_arrow, dashed}
%%%, clingo/.style={font=\small\ttfamily,draw,align=left}
%%%, clingo_rule/.style={font=\small\ttfamily,align=left}
%%%    },
%%%    note/.style={draw,rounded corners, very thick, fill=blue!50!black}
%%%}

%%%\begin{tikzpicture}[remember picture,overlay]
%%%\node[note]
%%%  at (8.57,2.25)           % CHANGE THIS
%%%  {{\begin{varwidth}{90pt}
%%%  ...                      % CHANGE THIS
%%%  \end{varwidth}}
%%%};
%%%%\draw[step=1,help lines] (0,0) grid (10,10);
%%%\end{tikzpicture}


% ----------------------------------------------------------------------
\section{Motivation}
% ----------------------------------------------------------------------

% ----------------------------------------------------------------------
\begin{frame}{Motivation}
\begin{itemize}
  \vfill
  \item<1->\alert<1>{Goals}:
  \begin{itemize}
    \item Teach Answer Set Programming (ASP)
    \item Develop a methodology for ASP
  \end{itemize}
  \bigskip
  \bigskip
  \item<2->There is a \alert<2>{gap} between
  \begin{itemize}
    \item Stable model semantics for \alert<2>{logic} programs
    \item Answer Set \alert<2>{Programming}
  \end{itemize}
  \vfill
\end{itemize}
\end{frame}

% ----------------------------------------------------------------------
\begin{frame}{Both sides}
\begin{itemize}

  \item<1-> \alert<1>{Stable model semantics} for logic programs
  \begin{itemize}
    \item Very general syntax (e.g., negation, disjunction, aggregates)
    \item \alert<1>{Formal semantics} using reduct (or HT-logic)
    \item Translational semantics for some constructs (e.g., choices)
    \item Not constructive, pre-grounding
  \end{itemize}
  Great in theory: general, elegant, concise\ldots 
  \bigskip\bigskip
  \item<2-> \alert<2>{Answer Set Programming} \only<3>{\alert<3>{(often)}}
  \begin{itemize}
    \item Restricted syntax (limited recursion, no disjunction)
    \item \alert<2>{Informal semantics} using examples
    \item Direct interpretation of constructs (e.g., choices and constraints)
    \item Constructive (grounding as needed)
  \end{itemize}
  Great in practice: easy modeling language with effective solvers

\end{itemize}
\end{frame}

% ----------------------------------------------------------------------
\begin{frame}{The gap}
\begin{itemize}
  \item<1-> The explanations about Answer Set Programming are 
        only indirectly linked to the formal semantics:
        \alert<1>{where is the reduct?}
  \bigskip
  \item<2-> How do \alert<2>{the experts} bridge the gap?
  \begin{itemize}
    \item Programming methodology: restricted syntax, and rules in order
    \item Non-recursive negation: simplified using the Splitting Set Theorem
    \item Positive rules: iterate over $\T{P}$ 
    \item Choice rules and constraints: direct interpretation
  \end{itemize}
  \bigskip 
  \item<3-> \alert<3>{This talk:}
  Tutorial + formal semantics for Answer Set Programming
  \begin{itemize}
    \item Those features are made explicit in the semantics
    \item Easy and constructive (grounding as needed) 
    \item Graphical interpretation
  \end{itemize}
\end{itemize}
\end{frame}

% ----------------------------------------------------------------------
\section{Examples}
% ----------------------------------------------------------------------

% ----------------------------------------------------------------------
\begin{frame}{Example}

$
P
=
\left\{
    \only<1>{\{ p \} \leftarrow,}\only<2->{q \leftarrow p,} \
    \only<1>{q \leftarrow p,}\only<2>{\{ p \} \leftarrow,}\only<3->{\phantom{q} \leftarrow \naf{q},} \
    \only<1-2>{\phantom{q} \leftarrow \naf{q}}\only<3->{\{ p \} \leftarrow} 
\right\}
$
\bigskip
\begin{center}
\begin{tikzpicture}
[
  examples
]

% line 0
\uncover<4->{
\alert<4>{
\node[smodel] (node01)  at ( 1, 0) {};
}
}

% line 1

\uncover<5->{
\alert<5>{
\node[smodel] (node11) at ( 0,1) {}
  edge [arrow] (node01);

\node[smodel] (node12) at ( 2,1) {$p$}
  edge [arrow] (node01);
}
}

\only<1-7>{
\alert<5>{
\node[rule] at (3.5,1) {$\{p\} \leftarrow$};
}
}
\node[rule_dep] (rule1) at (5.5,1) {$\{p\} \leftarrow$};
\visible<8>{
\draw (2.75,0.75) node[anchor=south west,align=right] {\texttt{example.lp}} rectangle (4.25,3.25) ;

\node[clingo_rule] at (3.5,1) {\{p\}.};
}
% line 2

\uncover<6->{
\alert<6>{
\node[smodel] (node21) at ( 0,2) {}
  edge [arrow] (node11);

\node[smodel] (node22) at ( 2,2) {$p$ $q$}
  edge [arrow] (node12);
}
}

\only<1-7>{
\alert<6>{
\node[rule] at (3.5,2) {$q \leftarrow p$};
}
}

\node[rule_dep] (rule2) at (5.5,2) {$q \leftarrow p$}
  edge [rule_arrow] (rule1);
\only<8>{
\node[clingo_rule] at (3.5,2) {q :- p.};
}

% line 3

%\node[empty] (node31) at ( 0,3) {\emptysmodel}
%  edge [empty_arrow] (node21);

\uncover<7->{
\alert<7>{
\node[smodel] (node32) at ( 2,3) {$p$ $q$}
  edge [arrow] (node22);
}
}

\only<1-7>{
\alert<7>{
\node[rule] at (3.5,3) {$\phantom{q} \leftarrow \naf{q}$};
}
}
\node[rule_dep] (rule3) at (5.5,3) {$\phantom{q} \leftarrow \naf{q}$}
  edge [rule_arrow_neg] (rule2);
\only<8>{
\node[clingo_rule] at (3.5,3) {:- not q.};
}

%\draw [help lines] (0,0) grid (5,5);
\end{tikzpicture}
\end{center}

\end{frame}

% ----------------------------------------------------------------------
\begin{frame}[label=newexamplelong]{Example}

$
P
=
\left\{
    \{ p \} \leftarrow, \ \
    q \leftarrow p, \ \
    \{ r \} \leftarrow \naf{p}, \ \
    s \leftarrow \naf{q}, \naf{r}, \ \
    \phantom{s} \leftarrow r, \naf{p}
\right\}
$

\bigskip
\begin{center}
\begin{tikzpicture}
[
  examples
  , x=1cm
  , y=-1cm
  , every node/.style={node distance=1cm and 1cm, on grid}
  , rule_dep/.style={align=center, draw}
  , rule_arrow/.style={<-}
  , rule_arrow_neg/.style={rule_arrow, dashed}
]

%
% dependency graph
%
\node[rule_dep] (rule1) at (8.5,1.5) {$\{p\} \leftarrow$};
\node[rule_dep, below left=of rule1, xshift=-1.5mm] (rule21) {$q \leftarrow p$}
  edge [rule_arrow] (rule1);
\node[rule_dep, below right=of rule1, xshift=1.5mm] (rule22) {$\{r\} \leftarrow \naf{p}$}
  edge [rule_arrow_neg] (rule1);
\node[rule_dep, below=of rule21] (rule31) {$s \leftarrow \naf{q}, \naf{r}$}
  edge [rule_arrow_neg] (rule21);
\draw [rule_arrow_neg, shorten <= 0.1mm] (rule31.north east) -- (rule22.south);
\node[rule_dep, below=of rule22] (rule32) {$\phantom{s} \leftarrow r, \naf{p}$}
  edge [rule_arrow] (rule22);
\draw [rule_arrow_neg, ->, rounded corners] (rule1.east) -- ++ (1.85,0) -- ++ (0,2) -- (rule32.east);

%\draw [help lines] (0,0) grid (-5,5);


%
% rule sequence
%
\node[rule] (rule_seq_1) at (4.25,1) {$\{p\} \leftarrow$};
\alt<7->{
\node[rule, below=of rule_seq_1] (rule_seq_2) {$\{r\} \leftarrow \naf{p}$};
\node[rule, below=of rule_seq_2] (rule_seq_3) {$\phantom{s} \leftarrow r, \naf{p}$};
\node[rule, below=of rule_seq_3] (rule_seq_4) {$q \leftarrow p$};
\node[rule, below=of rule_seq_4] (rule_seq_5) {$s \leftarrow \naf{q}, \naf{r}$};
}{
\node[rule, below=of rule_seq_1] (rule_seq_2) {$q \leftarrow p$};
\node[rule, below=of rule_seq_2] (rule_seq_3) {$\{r\} \leftarrow \naf{p}$};
\node[rule, below=of rule_seq_3] (rule_seq_4) {$s \leftarrow \naf{q}, \naf{r}$};
\node[rule, below=of rule_seq_4] (rule_seq_5) {$\phantom{s} \leftarrow r, \naf{p}$};
}
%
% smodels
%

% line 0
\node[smodel] (node01)  at ( 1, 0) {};

% line 1
\uncover<2-6,8->{
\node[smodel, below left=of node01] (node11) {}
  edge [arrow] (node01);
\node[smodel, below right=of node01] (node12) {$p$}
  edge [arrow] (node01);
}

\alt<7->{

% line 2
\uncover<9->{
\node[smodel, below left=of node11, xshift=4mm] (node21) {}
  edge [arrow] (node11);
\node[smodel, below right=of node11, xshift=-4mm] (node22) {$r$}
  edge [arrow] (node11);
\node[smodel, below=of node12] (node23) {$p$}
  edge [arrow] (node12);
}

% line 3
\uncover<10->{
\node[smodel, below=of node21] (node31) {}
  edge [arrow] (node21);
\node[smodel, below=of node23] (node32) {$p$}
  edge [arrow] (node23);
}

% line 4
\uncover<11->{
\node[smodel, below=of node31] (node41) {}
  edge [arrow] (node31);
\node[smodel, below=of node32] (node42) {$p$ $q$}
  edge [arrow] (node32);
}

% line 5
\uncover<12->{
\node[smodel, below=of node41] (node51) {$s$}
  edge [arrow] (node41);
\node[smodel, below=of node42] (node52) {$p$ $q$}
  edge [arrow] (node42);
}

}{
% line 2
\uncover<3->{
\node[smodel, below=of node11] (node21) {}
  edge [arrow] (node11);
\node[smodel, below=of node12] (node22) {$p$ $q$}
  edge [arrow] (node12);
}

% line 3
\uncover<4->{
\node[smodel, below left=of node21, xshift=4mm] (node31) {}
  edge [arrow] (node21);
\node[smodel, below right=of node21, xshift=-4mm] (node32) {$r$}
  edge [arrow] (node21);
\node[smodel, below=of node22] (node33) {$p$ $q$}
  edge [arrow] (node22);
}

% line 4
\uncover<5->{
\node[smodel, below=of node31] (node41) {$s$}
  edge [arrow] (node31);
\node[smodel, below=of node32] (node42) {$r$}
  edge [arrow] (node32);
\node[smodel, below=of node33] (node43) {$p$ $q$}
  edge [arrow] (node33);
}

% line 5
\uncover<6->{
\node[smodel, below=of node41] (node51) {$s$}
  edge [arrow] (node41);
%\node[smodel] (node42) at ( 1,4) {$r$}
%  edge [arrow] (node32);
\node[smodel, below=of node43] (node53) {$p$ $q$}
  edge [arrow] (node43);
}
}

\end{tikzpicture}
\end{center}

\end{frame}

% ----------------------------------------------------------------------
% \input{recursion_hard}
% \input{recursion}

\begin{frame}{Recursion examples\ldots}
\end{frame}

% ----------------------------------------------------------------------
\section{Theory}
% ----------------------------------------------------------------------

% ----------------------------------------------------------------------
\begin{frame}<1-4>[label=programsframe]{\only<1>{Normal logic programs}%
              \only<2->{\alert<2-4>{Extended} logic programs}}%\only<6->{ \alert<6->{with variables}}}
  \label{eqn:rule}
  \begin{itemize}
  \item %<1->
    \alt<6>{
    A \alert{logic program}, $P$, over a set $\mathcal{A}$ of \alert{atoms with variables} 
    is a finite set of \alert{safe} rules, i.e., the variables of every rule $r$ must occur in \pbody{r}
    }{
    A \alert<1>{logic program}, $P$, over a set $\mathcal{A}$ of atoms is a finite \alert<1>{set} of rules
    }
%  \only<6>{\item Every rule $r$ must be \alert{safe}, i.e., each of its variables also occurs in \pbody{r}}
  \item %<1->
    A \only<1>{(normal)}\alert<2-4>{\only<2>{normal}\only<3>{choice}\only<4->{constraint}} \alert<1-4>{rule}, $r$, is of the form
    \[
%      \alt<2>{\tt a_0\texttt{ :- } a_1,\dots,a_m,\texttt{ not }{a_{m+1}},\dots,\texttt{ not }{a_n}.}%
                  {\only<1-2>{a_0}\only<3>{\{a_0\}}\only<4->{\phantom{\{a_0\}}} \leftarrow   a_1,\dots,a_m,          \naf{a_{m+1}},\dots,          \naf{a_n}}
    \]
    where $0\leq m\leq n$ and each $a_i\in{\mathcal{A}}$ is an atom for $\alt<4->{1}{0}\leq i\leq n$
  \item %<3->
    \structure{Notation}
    \begin{align*}
      \head{r}\phantom{^+}    &=\, \only<1-3>{a_0}\only<4->{{\{\}}}
      \\
      \body{r}\phantom{^+}    &=\, \{a_1,\dots,a_m,\naf{a_{m+1}},\dots,\naf{a_n}\}
      \\
      \pbody{r}               &=\, \{a_1,\dots,a_m\}
      \\
      \nbody{r}               &=\, \{a_{m+1},\dots,a_n\}
%     \only<4>{%
%      \\
%      \atom{P}\phantom{^+} &=\, \textstyle\bigcup_{r\in P}\left(\{\head{r}\}\cup\pbody{r}\cup\nbody{r}\right)
%      \\
%      \body{P}\phantom{^+} &=\, \{\body{r}\mid r\in P\}
%      \\
%      \head{P}\phantom{^+} & =\, \{\head{r}\mid r\in P\}}
    \end{align*}%
  \item %<4-> 
  A \alert<1>{literal} is an atom or a negated atom
  \item %<5-> 
  A program $P$ is \alert<1>{positive} if $\nbody{r}=\emptyset$ for all $r\in P$
  \end{itemize}

\only<0>{
\begin{tikzpicture}[remember picture,overlay]
%\node[note]
%  at (5.85,7.2)            % CHANGE THIS
%  {{\begin{varwidth}{100pt}
%  over a set $\mathcal{A}$ of atoms \par \alert{with variables} % CHANGE THIS
%  \end{varwidth}}
%};
\node[note]
  at (2,6)            % CHANGE THIS
  {{\begin{varwidth}{150pt}
  \begin{itemize}
  \item
  A logic program, $P$, over a set $\mathcal{A}$ of atoms \alert{with variables} is a finite set of rules
  \end{itemize}
  \end{varwidth}}
};
%\draw[step=1,help lines] (0,0) grid (10,10);
\end{tikzpicture}

%%%\begin{tikzpicture}[remember picture,overlay]
%%%%\draw[step=1,help lines] (0,0) grid (10,10);
%%%\node % [draw, rounded corners, very thick] 
%%%  at (7.77,6.4) {\alert{with variables}};
%%%\draw[rounded corners, very thick] 
%%%  (6.6,7.2) -- (7.72,7.2) -- (7.72,6.65) -- (9,6.65)
%%%  -- (9,6.1) -- (6.6,6.1) -- cycle;
%%%\end{tikzpicture}
}
\end{frame}


%\renewcommand{\head}[1]{\ensuremath{\mathit{h}(#1)}}
%\renewcommand{\body}[1]{\ensuremath{\mathit{b}(#1)}}

\newcommand{\headphantom}[1]{\ensuremath{\phantom{\mathit{head}(}#1\phantom{)}}}

% ----------------------------------------------------------------------
\begin{frame}<1-8>[label=operatorframe]{Application operator}
  \begin{itemize}
  \item A set of atoms $X$ \alert<1>{satisfies} a set of literals 
        \mbox{\small$\{a_1,\dots,a_m,\naf{a_{m+1}},\dots,\naf{a_n}\}$} if
        \mbox{\small$\{a_1, \dots, a_m\} \subseteq X$} and 
        \mbox{\small$\{a_{m+1},\dots,a_n\} \cap X = \emptyset$}.
  \medskip
  \item<2-> Let $P$ be a set of \alert<2-8>{\only<1-4>{normal}\only<5-6>{choice}\only<7->{constraint}} 
            rules and $\setsets{X}$ a set of sets of atoms,\par     
            the \alert<2-8>{application operator} $\App{P}$ is defined as follows:
  \smallskip 
  \mbox{\small$
      \A{P}{\setsets{X}} = \big\{  
        \only<1-6>{X \cup Y}\only<7->{\alert<5>{\hspace{9.5pt}X \hspace{10pt}}}\mid X \in \setsets{X}, %
        \only<1-6>{Y}\only<7->{\ \alert<7>{\emptyset}} \only<1-4,7->{\alert{=}}\only<5-6>{\alert{\subseteq}} %
        \alt<3>{
        \underbrace{
        \{ \only<1-6>{\head{r}}\only<7->{\hspace{14.5pt} \alert<7-8>{r} \hspace{14pt}} \mid r\in P\text{ and }%
        X \text{ satisfies } \body{r} \}
        }_{\T{P}{X}\text{ if }P\text{ is positive}} 
        }{
        \{ \only<1-6>{\head{r}}\only<7->{\hspace{14.5pt} \alert<7-8>{r} \hspace{14pt}} \mid r\in P\text{ and }%
        X \text{ satisfies } \body{r} \}
        } 
      \big\}
      $}
      \bigskip 

%  \item \structure{Example:}
\only<10->{
   \item For $n \geq 1$, let \alert<10>{$\Ai{P}{n}{\setsets{X}}$} be $\A{P}{\setsets{X}}$ 
         if $n=1$ and $\A{P}{\Ai{P}{n-1}{\setsets{X}}}$ if $n > 1$.\par
         E.g., $\Ai{P}{2}{\setsets{X}}$ is  $\A{P}{\A{P}{\setsets{X}}}$, 
         and $\Ai{P}{3}{\setsets{X}}$ is  $\A{P}{\A{P}{\A{P}{\setsets{X}}}}$.
}\only<11->{
   \pause
   \item Let \alert<11>{$\Afixp{P}{\setsets{X}}$} be $\Ai{P}{n}{\setsets{X}}$ where $n$ is the smallest integer such that 
        $\Ai{P}{n}{\setsets{X}}=\Ai{P}{n+1}{\setsets{X}}$. 
}
  \end{itemize}

\only<13>{
\begin{tikzpicture}[remember picture,overlay]
\node[note]
  at (8.57,2.55)           % CHANGE THIS
  {{\begin{varwidth}{90pt}
    \alert{$r \in \ground{P}$} 
    \setlength{\leftmargini}{1em}
    \begin{itemize}
    \item $\pbody{r} \subseteq X$ 
    %\item The Herbrand universe is obtained from $P$ and $X$
    \end{itemize}
  \end{varwidth}}
};
%\draw[step=1,help lines] (0,0) grid (10,10);
\end{tikzpicture}
}

\input{application_figs}


\end{frame}

% ----------------------------------------------------------------------
\begin{frame}<1-5>[label=nonrecframe]{Non-recursive programs}
  \begin{itemize}
      \item \alert<1>{Dependency graph} of program $P$
      \begin{itemize}
        \alt<7-8>{
        \item rule $r_2$ \alert{depends} on rule $r_1$\\ 
        \alt<7>{
        if $b\in\pbody{r_2}\cup\nbody{r_2}$ \alert{unifies} with $\head{r_1}$
        }{
        if $b\in\pbody{r_2}\cup\nbody{r_2}$ and $\head{r_1}$ have \alert{the same predicate}
        }
        }{
        \item rule $r_2$ depends on rule $r_1$
              if $(\pbody{r_2}\cup\nbody{r_2})\cap\head{r_1}\neq\emptyset$
        }
        \item $G_P=(P,E)$ where $E=\{ (r_1,r_2) \mid r_2 \mbox{ depends on } r_1 \}$
      \end{itemize}
    \pause
    \item Program $P$ is \alert<2>{non-recursive} if $G_P$ is acyclic, i.e., it has no path of length greater than zero
          from some rule $r$ to itself.
    \pause
    \bigskip
    %\item If $P$ is non-recursive then there is some topological ordering
    \item If $P$ is \alert<3>{non-recursive} then there is some \alert<3>{topological ordering}
          $(r_1, \ldots, r_n)$
          of $G_P$. %and
    \pause
    \item For all such orderings the results of
          \alert<4>{$\A{\{r_n\}}{\ldots\A{\{r_1\}}{\{\emptyset\}}}$}
          coincide and are equal to the \alert<4>{stable models} of $P$.
    \pause
    \bigskip
    \item \alert<5>{Methodology:} 
          \begin{enumerate}
            \item Write the rules of non-recursive programs in order.
            \item The stable models are the result of applying the rules in order.
          \end{enumerate}
  \end{itemize}
\end{frame}

% ----------------------------------------------------------------------
%\againframe<6>{newexamplelong}

% ----------------------------------------------------------------------
%\againframe<12>{newexamplelong}

% ----------------------------------------------------------------------
\begin{frame}<0>{Non-recursive programs}
  \begin{itemize}
    \item If $P$ is non-recursive then there is
          some ordering $(p_1, p_2, \ldots)$ of the atoms of $P$ along with
          some topological ordering
          $(r_1, \ldots, r_n)$ of $G_P$ where:
    \begin{itemize}
      \item first occur the facts, 
      \item then the normal rules whose head is $p_1$, 
      \item then the choice rules whose head is $p_1$, 
      \item then the constraint rules that are independent of the rest of the rules,
      \item then the normal rules whose head is $p_2$, 
      \item then the choice rules whose head is $p_2$, 
      \item and so on\ldots
    \end{itemize}
    %for some ordering $(p_1, p_2, \ldots)$ of the atoms of $P$ 
    \item $\A{C_n}{\ldots\A{C_m}{\A{C_{m+1}}{\ldots\A{C_1}{\{\emptyset\}}}}} =
           \A{C_n}{\ldots\A{C_m \cup C_{m+1}}{\ldots\A{C_1}{\{\emptyset\}}}}$ whenever 
            the rules of $C_m$ do not depend on the rules of $C_{m+1}$ and vice versa
    \item Then we can group in separate components
          the normal, choice and constraint rules for every atom, and also the initial facts
  \end{itemize}

%\begin{textblock*}{\textwidth}(.75\textwidth,0.25\textheight)
%    \begin{beamercolorbox}[wd=.5\textwidth,center,sep=0.3cm]{block body example}
%        This is wrong!
%    \end{beamercolorbox}
%\end{textblock*}

%\begin{tikzpicture}[remember picture,overlay]
%\node at (current page.center) {\alert{ground}};
%\node at (3,0.5) {\alert{\Huge{ground}}};
%\draw[step=1,help lines] (0,0) grid (10,10);
%\end{tikzpicture}

\end{frame}

% ----------------------------------------------------------------------
\againframe<9-11>{operatorframe}

% ----------------------------------------------------------------------
%\againframe<6>{examplerecursion}
%\againframe<10>{examplerecursion}
%\againframe<15>{examplerecursion}

% ----------------------------------------------------------------------
\begin{frame}<1-5>[label=easyframe]{Easy programs}
  \begin{itemize}
    \item \alert<1>{Dependency graph} of program $P$
      \begin{itemize}
        %\item rule $r_2$ depends on rule $r_1$
        %      if $(\pbody{r_2}\cup\nbody{r_2})\cap\head{r_1}\neq\emptyset$
        %\item $G_P=(P,E)$ where $E=\{ (r_1,r_2) \mid r_2 \mbox{ depends on } r_1 \}$
        \alt<7-8>{
        \alt<7>{
        \item an edge $(r_1,r_2)$ is \alert{negative} if $b \in \nbody{r_2}$ \alert{unifies} with $\head{r_1}$
        }{
        \item an edge $(r_1,r_2)$ is \alert{negative} if $b \in \nbody{r_2}$ and $\head{r_1}$
        \par have \alert{the same predicate}
        }
        }{
        \item an edge $(r_1,r_2)$ is \alert<1>{negative} if $\nbody{r_2}\cap\head{r_1}\neq\emptyset$
        }
      \end{itemize}
    \pause
    \item Program $P$ is \alert<2>{easy} if the strongly connected components of $G_P$ 
     \begin{itemize}
       \item do not include negative edges, and
       \item do not include rules of different types.
     \end{itemize} 

%\only<3>{
%\begin{tikzpicture}[remember picture,overlay]
%\node[note]
%  at (8.5,0.5)           % CHANGE THIS
%  {{\begin{varwidth}{90pt}
%  Non-recursive programs 
%      are easy
%  \end{varwidth}}
%};
%%\draw[step=1,help lines] (0,0) grid (10,10);
%\end{tikzpicture}
%}

    \bigskip
    \pause
    \item If $P$ is \alert<3>{easy} then there is some \alert<3>{topological ordering}
          $(C_1, \ldots, C_n)$ of the \alert<3>{strongly connected components}
          of $G_P$.
    \pause
    \item For all such orderings the results of
          \alert<4>{$\Afixp{C_n}{\ldots\Afixp{C_1}{\{\emptyset\}}}$}
          coincide and are equal to the \alert<4>{stable models} of $P$.
    \pause
    \bigskip
    \item Note:
          The $C_i$'s are either sets of \alert<5>{recursive rules}, or
          \alert<5>{singleton sets} $\{r\}$ where $r$ is not recursive,
          in which case $\Appfixp{{\{r\}}}=\App{\{r\}}$.
  \end{itemize}

\end{frame}

% ----------------------------------------------------------------------
%\againframe<10>{examplerecursion}

% ----------------------------------------------------------------------
%\againframe<15>{examplerecursion}

% ----------------------------------------------------------------------
\begin{frame}{Easy programs}
  \begin{itemize}
    \bigskip
    \item \alert<1>{Methodology:}
          \begin{enumerate}
            \item Write the rules of easy programs in order.\par
                  The order between the rules of the recursive sets does not matter.
            \item The stable models are the result of applying the rules in order, \par 
                  iterating over the rules of the recursive sets.
          \end{enumerate}
    \bigskip
    \item[$*$]<2-> The components may be \alert<2>{applied together}:
      \begin{itemize}
        \item 
        If the rules of $C_{m}$ \alert<2>{do not depend negatively} on the rules of $C_{m-1}$
        $\Afixp{C_n}{\ldots\Afixp{C_m}{\Afixp{C_{m-1}}{\ldots\Afixp{C_1}{\{\emptyset\}}}}} =
        \Afixp{C_n}{\ldots\Afixp{C_m \cup C_{m-1}}{\ldots\Afixp{C_1}{\{\emptyset\}}}}$.
        \vspace{2pt}
        \item If there are no dependencies between the rules of $C_i$ then
                 {$\Appfixp{{C_i}}=\App{C_i}$}.
        \item Examples: non-recursive normal (or choice) rules with the same head,
              facts at the start, constraints at the end\ldots  
    \end{itemize}
      
%      \begin{itemize}
%        %\item<3-> If \alert<3>{$P$ is positive}, then its stable models are 
%        %          \alert<3>{$\Afixp{P}{\{\emptyset\}}$}.
%        \item<4-> If \alert<4>{$C_i$ is not recursive}, then 
%                  \alert<4>{$\Appfixp{{C_i}}=\App{C_i}$}.
%      \end{itemize}
  \end{itemize}
\end{frame}
    
% ----------------------------------------------------------------------
\begin{frame}{\alert{Extending} easy programs}
  \begin{itemize}
    \vfill
    \item Allow rules of different types in strongly connected components %,\par
    \medskip
    \item Only disallow recursion through negation
    \bigskip
    \bigskip
    \pause
    \item Let $C$ be a strongly connected component of $G_P$
          \alt<3>{
          \[ 
          \Appfixp{C} = \App{constraints(C)}\fixp{\big(
                        \Appfixp{normal(C)}
                        \App{choice(C)}\big)} 
          \]
          }{
          \[ 
          \Appfixp{C} = \fixp{\big(\Appfixp{constraints(C)}
                                   \Appfixp{normal(C)}
                                   \Appfixp{choice(C)}\big)} 
          \]
          }
%          \begin{center}
%          \end{center}
    \vfill
  \end{itemize}
\end{frame}
%
% a.
% {b} :- a.
% c :- b.
% d :- c.
% a :- d.
% returns {a, abc, abcd} if we use A_normal(C) without the star
%

% ----------------------------------------------------------------------
\begin{frame}<0>{Easy programs}
  \begin{itemize}
    \item If $P$ is easy then there is 
          some ordering $(X_1, \ldots, X_n)$ of a partition of the atoms of $P$ along with
          some topological ordering
          $(C_1, \ldots, C_n)$ of the strongly connected components of $G_P$
          where:
    \begin{itemize}
      \item first occur the facts, 
      \item then the non-recursive normal rules whose head is in $X_1$, 
      \item then the non-recursive choice rules whose head is in $X_1$, 
      \item then the recursive rules whose head is in $X_1$, 
      \item then the constraint rules that are independent of the rest of the rules,
      \item then the non-recursive normal rules whose head is in $X_2$, 
      \item and so on\ldots
    \end{itemize}
    %for some ordering $(p_1, p_2, \ldots)$ of the atoms of $P$ 
      \item $\Afixp{C_n}{\ldots\Afixp{C_m}{\Afixp{C_{m+1}}{\ldots\Afixp{C_1}{\{\emptyset\}}}}} =
             \Afixp{C_n}{\ldots\Afixp{C_m \cup C_{m+1}}{\ldots\Afixp{C_1}{\{\emptyset\}}}}$ whenever 
            the rules of $C_m$ do not depend on the rules of $C_{m+1}$ and vice versa
    \item Then we can group in separate components
          the normal, choice, recursive  and constraint rules for every partition, and also the initial facts
  \end{itemize}
\end{frame}

% ----------------------------------------------------------------------
\section{With Variables}
% ----------------------------------------------------------------------

% ----------------------------------------------------------------------
\begin{frame}{Example}
\xtodo
\end{frame}

% ----------------------------------------------------------------------
\begin{frame}{Extended logic programs \alert{with variables}}
  \vfill
  \begin{itemize}
    \item Update the definitions of program and dependency graph as usual
    \bigskip
    \item \alert{Update the definition of \A{P}}
    \bigskip
  \item[$*$] Question: inforce finiteness, or redefine \Afixp{P}? 
  \end{itemize}
  \vfill 
\end{frame}

\againframe<5->{programsframe}

\againframe<12-13>{operatorframe}

\againframe<6-8>{nonrecframe}

\againframe<6-8>{easyframe}

% ----------------------------------------------------------------------
\section{Conclusion}
% ----------------------------------------------------------------------

% ----------------------------------------------------------------------
\begin{frame}{Conclusion}
\vfill
\begin{itemize}
\item Formal semantics for Easy ASP
\bigskip
\item Hopefully useful for explaining ASP
\bigskip
\item Extensions: arithmetics, aggregates, intervals, pooling
\bigskip
\item More extensions: functions, epistemic operators
\end{itemize}
\vfill
\end{frame}