\documentclass{article}

\input{common}

\title{Summary of Important Definitions}
\date{May 11th}


\begin{document}
    \maketitle



    \section{Lattice Theory}

    \begin{definition}
        A {\em partial order} $\preceq$ is a relation over a set $S$ such that for every triple of elements $x, y, z \in S$ the following hold
        \begin{itemize}
            \item (reflexivity) $x \preceq x$
            \item (antisymmetry) $(x \preceq y \land y \preceq x) \implies x = y$
            \item (transitivity) $(x \preceq y \land y \preceq z) \implies (x \preceq z)$
        \end{itemize}
    \end{definition}


    \begin{definition}
        Given a partial order $\preceq$ over a set $S$ and a subset $X \subseteq S$, a {\em lower bound} of $X$  (resp.\ an {\em upper bound} of $X$) is an element $x \in S$ (Note that it may be the case that $x \not\in X$) such that 
        \begin{itemize}
            \item $\forall y \in X, \boxed{x} \preceq y$
            \item (resp. $\forall y \in X, \boxed{y} \preceq x$)
        \end{itemize}
        The {\em greatest lower bound} of a set $X \subseteq S$ (denoted as $\textbf{glb}(X)$) is a unique upperbound of the set of all lowerbounds of $X$.
        The {\em least upper bound} of a set $X \subseteq S$ (denoted as $\textbf{lub}(X)$) is a unique lowerbound of the set of all upperbounds of $X$.
        In general, $\textbf{lub}(X)$ and $\textbf{glb}(X)$ may not exist.
    \end{definition}

    \begin{definition}
        A (complete) lattice $\langle \mathcal{L}, \preceq \rangle$ is a set of elements $\mathcal{L}$ and a partial order $\preceq$ over $\mathcal{L}$ such that for any set $S \subseteq \mathcal{L}$
        \begin{itemize}
            \item $\textbf{lub}(X)$ and $\textbf{glb}(X)$ exist and are unique.
        \end{itemize}
    \end{definition}

    \subsection{Fixpoint Operators}

    \begin{definition}
        Given a complete lattice $\langle \mathcal{L}, \preceq \rangle$, a fixpoint operator over the lattice is a function $\Phi: \mathcal{L} \rightarrow \mathcal{L}$ that is {\em $\preceq$-monotone}
        \begin{itemize}
            \item $\Phi$ is $\preceq$-monotone if for all $x, y \in \mathcal{L}$
            \begin{align*}
                x \preceq y \implies \Phi(x) \preceq \Phi(y)
            \end{align*}
            (Note: this does not mean the function is inflationary, i.e., $x \preceq \Phi(x)$ may not hold)
        \end{itemize}
        A {\em fixpoint} is an element $x \in \mathcal{L}$ s.t. $\Phi(x) = x$.
    \end{definition}

    \begin{theorem}[Knaster-Tarski]
        The set of all fixpoints of a fixpoint operator $\Phi$ on a complete lattice is itself a complete lattice. The least element of this new lattice exists and is called the least fixpoint (denoted as $\lfp~{\Phi}$)
    \end{theorem}

    Some intuitions about lattices
    \begin{itemize}
        \item The entire lattice has a biggest element $\lub{}(\mathcal{L}) = \top$ and a smallest element $\glb{}(\mathcal{L}) = \bot$
        \item When a lattice has a finite height (or finite domain). The least fixed point of a fixpoint operator can be computed by iteratively applying the fixpoint operator to $\bot$
        \item An operator may return an element that is not comparable to the input, however, after a comparable element is returned (either greater or less than) that comparability and direction are maintained for all subsequent iterations.
        \item Further, because $\bot$ is less than all elements in the lattice, it is always the case that $\bot \preceq \Phi(\bot)$
    \end{itemize}

    \section{Partial Stable Model Semantics}

    \begin{definition}
        A (ground and normal) {\em answer set program} $\P$ is a set of rules where each rule $r$ is of the form
        \begin{align*}
            h \leftarrow a_0,~ a_1,~ \dots,~ a_n,~ \Not b_0,~\Not b_1,~\dots,~\Not b_k
        \end{align*}
        where we define the following shorthand for a rule $r \in \P$
        \begin{align*}
            \head(r) &= h\\
            \bodyp(r) &= \{ a_0,~ a_1,~ \dots,~ a_n \}\\
            \bodyn(r) &= \{ b_0,~ b_1,~ \dots,~ b_k \}
        \end{align*}
    \end{definition}

    \begin{definition}
        A two-valued interpretation $I$ of a program $\P$ is a set of atoms that appear in $\P$.
    \end{definition}

    \begin{definition}
        An interpretation $I$ is a \boxedt{model} of a program $\P$ if for each rule $r \in \P$
        \begin{itemize}
            \item If $\bodyp(r) \subseteq I$ and $\bodyn(r) \intersect I = \emptyset$ then $\head(r) \in I$.
        \end{itemize}
    \end{definition}

    \begin{definition}
        An interpretation $I$ is a \boxedt{stable model} of a program $\P$ if $I$ is a model of $\P$ \textbf{and}
        for every interpretation $I' \subseteq I$ there exists a rule $r \in \P$ such that
        \begin{itemize}
            \item $\bodyp(r) \subseteq I'$, $\bodyn(r) \intersect I \not= \emptyset$ (Note that this is $I$ and not $I'$) and $\head(r) \not\in I'$
        \end{itemize}
    \end{definition}

    \begin{definition}
        A three-valued interpretation $(T, P)$ of a program $\P$ is a pair of sets of atoms such that $T \subseteq P$.
        The \boxedt{truth-ordering} respects $\ff < \uu < \tt$ and is defined for two three-valued interpretations $(T, P)$ and $(X, Y)$ as follows.
        \begin{align*}
            (T, P) \preceq_t (X, Y) \textrm{ iff } T \subseteq X \land P \subseteq Y
        \end{align*}
        The \boxedt{precision-ordering} respects the partial order $\uu < \tt$, $\uu < \ff$ and is defined for two three-valued interpretations $(T, P)$ and $(X, Y)$ as follows.
        \begin{align*}
            (T, P) \preceq_p (X, Y) \textrm{ iff } T \subseteq X \land \boxed{Y \subseteq P}
        \end{align*}
    \end{definition}

    \begin{definition}
        A three-valued interpretation $(T, P)$ is a {\em model} of a program $\P$ if for each rule $r \in \P$
        \begin{itemize}
            \item $\body(r) \subseteq P \land \bodyn(r) \intersect T = \emptyset$ implies $\head(r) \in P$, and
            \item $\body(r) \subseteq T \land \bodyn(r) \intersect P = \emptyset$ implies $\head(r) \in T$.
        \end{itemize}
    \end{definition}

    \begin{definition}
        A three-valued interpretation $(T, P)$ is a {\em stable model} of a program $\P$ if it is a model of $\P$ and if for every three-valued interpretation $(X, Y)$ such that $(X, Y) \preceq_t (T, P)$ there exists a rule $r \in \P$ such that either
        \begin{itemize}
            \item $\bodyp(r) \subseteq Y \land \bodyn(r) \intersect T = \emptyset$ and $\head(r) \not\in Y$ \textbf{OR}
            \item $\bodyp(r) \subseteq X \land \bodyn(r) \intersect P = \emptyset$ and $\head(r) \not\in X$
        \end{itemize}
    \end{definition}


    \section{Approximation Fixpoint Theory}

    We can think of a three-valued interpretation $(T, P)$ as an approximation on the set of true atoms.
    $T$ is a lower bound and $P$ is the upper bound.

    \begin{definition}
        An {\em approximator} is a fixpoint operator on the complete lattice $\langle \wp(\mathcal{L})^2, \preceq_p \rangle$ (called a bilattice)
    \end{definition}
    Given a function $f(T, P): S^2 \rightarrow S^2$, we define two separate functions
    \begin{align*}
        f(\cdot, P)_1:~ &S \rightarrow S\\
        f(T, \cdot)_2:~ &S \rightarrow S
    \end{align*}
    such that 
    \begin{align*}
        f(T, P) = \Big(&(f(\cdot, P)_1)(T), \\&(f(T, \cdot)_2)(P)\Big)
    \end{align*}

    \begin{definition}
        Given an approximator $\Phi(T, P)$ the stable revision operator is defined as follows
        \begin{align*}
            S(T, P) = (\lfp{(\Phi(\cdot, P)_1)},~ \lfp{(\Phi(T, \cdot)_2)})
        \end{align*}
        Note: the $\lfp$ is applied to a unary operator, thus it's the least fixpoint of the lattice $\langle \wp(\mathcal{L}), \subseteq \rangle$ whose least element is $\emptyset$.
    \end{definition}

    \subsection{An Approximator for Partial Stable Semantics}
    
    \begin{align*}
        \Gamma(T, P) &\define \{ \head(r) ~|~ r \in \P, T \subseteq \bodyp(r), \bodyn(r) \intersect P = \emptyset \}\\
        \Gamma(P, T) &\define \{ \head(r) ~|~ r \in \P, P \subseteq \bodyp(r), \bodyn(r) \intersect T = \emptyset \}\\
        \Phi(T, P) &\define \Bigl( \Gamma(T, P), \Gamma(P, T) \Bigr)
    \end{align*}

    Without stable revision where $(T, P) = (\{  a, b \}, \{  a, b \})$
    \begin{align*}
        \Phi(T, P) = (\{ a, b \}, \{ a, b \}) \textrm{   (fixpoint reached)}
    \end{align*}
    With stable revision
    \begin{align*}
        S(T, P) = (\emptyset, \emptyset) \textrm{   (fixpoint reached)}
    \end{align*}

    
    \section{The Polynomial Heirarchy}
    Intuitive definitions of ${\sf NP}$
    \begin{itemize}
        \item the class of problems which have algorithms that can verify solutions in polynomial time.
        \item A problem that can be solved by reducing it to a SAT expression of the form
        \begin{align*}
            \exists (a \lor b \lor c) \land (\neg a \lor \neg d \lor c)~\land \cdots
        \end{align*}
        \item (Alternating turing machine) A problem that is solved by some path of an algorithm that is allowed to branch is parallel
    \end{itemize}
    Intuitive definitions of ${\sf NP^{NP}}$ a.k.a.\ $\Sigma_2^P$
    \begin{itemize}
        \item the class of problems which have algorithms that can verify solutions in ${\sf NP}$ time.
        \item A problem that can be solved by reducing it to a SAT expression of the form
        \begin{align*}
            \exists c,~ \forall a,~ b,~ (a \lor b \lor c) \land (\neg a \lor \neg d \lor c)~\land \cdots
        \end{align*}
        \item (Alternating Turing machine) A problem that is solved by some path of an algorithm that is allowed to branch in parallel. A branch is allowed to switch to ``ALL'' mode only once and require that all subsequent forks return success
    \end{itemize}


\end{document}