From ac11a73a1a264e45a26ccb151720330fdc568b0e Mon Sep 17 00:00:00 2001 From: Spencer Killen Date: Thu, 11 May 2023 20:01:21 -0600 Subject: [PATCH] init --- .gitignore | 5 ++ Makefile | 11 ++++ common.tex | 131 +++++++++++++++++++++++++++++++++++++ document.tex | 179 +++++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 326 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 common.tex create mode 100644 document.tex diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..86b6a50 --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +* +!.gitignore +!*.tex +!*.bib +!Makefile diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..a464367 --- /dev/null +++ b/Makefile @@ -0,0 +1,11 @@ +all: document.pdf + +%.pdf: %.tex common.tex + latexmk -pdf $< + +clean: + ${RM} *.pdf + ${RM} *.bbl + ${RM} *.blg + + latexmk -C diff --git a/common.tex b/common.tex new file mode 100644 index 0000000..ee122e2 --- /dev/null +++ b/common.tex @@ -0,0 +1,131 @@ +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage{amssymb} +\usepackage{amsthm} +\usepackage{graphicx} +\usepackage{float} +\usepackage{verbatim} +\usepackage{enumerate} +\usepackage{mathtools} +\usepackage{accents} +\usepackage{bm}% boldmath + +\usepackage[acronym,hyperfirst=false]{glossaries} + +\newtheorem{theorem}{Theorem}[section] +\newtheorem{proposition}{Proposition}[section] +\newtheorem{example}{Example} +\newtheorem{lemma}{Lemma}[section] +\newtheorem{corollary}[theorem]{Corollary} +\newtheorem{definition}{Definition}[section] +\newtheorem{remark}{Remark} + +\newcommand{\Definition}[1]{Definition~\ref{#1}} +\newcommand{\Section}[1]{Section~\ref{#1}} +\newcommand{\Chapter}[1]{Chapter~\ref{#1}} +\newcommand{\Theorem}[1]{Theorem~\ref{#1}} +\newcommand{\Proposition}[1]{Proposition~\ref{#1}} +\newcommand{\Example}[1]{Example~\ref{#1}} +\newcommand{\Lemma}[1]{Lemma~\ref{#1}} +\newcommand{\Figure}[1]{Figure~\ref{#1}} +\newcommand{\Corollary}[1]{Corollary~\ref{ #1}} +\newcommand{\Remark}[1]{Remark~\ref{#1}} +\newcommand{\Algorithm}[1]{Algorithm~\ref{#1}} +\newcommand{\Line}[1]{line~\ref{#1}} + +\renewcommand{\P}{\mathcal{P}} +\newcommand{\Not}{\textrm{\bf not\,}} +\newcommand{\head}{head} +\newcommand{\intersect}{\cap} +\newcommand{\union}{\cup} +\newcommand{\atoms}{Atoms} +\newcommand{\bodyp}{body^{+}} +\newcommand{\bodyn}{body^{-}} +\newcommand{\body}{body} +\newcommand{\op}[1]{\textbf{#1}} +\newcommand{\pmodels}{\models} + +\newcommand{\KB}{\mathcal{K}} +\newcommand{\bfK}{\textit{\em \textbf{K}}} +\renewcommand{\O}{\mathcal{O}} +\renewcommand{\P}{\mathcal{P}} +\newcommand{\KAK}{\textbf{KA}(\KB)} +\newcommand{\Katom}{\textbf{K}-atom~} +\newcommand{\Katoms}{\textbf{K}-atoms~} +\newcommand{\comp}[1]{\overline{#1}} + +\newcommand{\A}{\textbf{A}} +\newcommand{\T}{\textbf{T}} +\newcommand{\F}{\textbf{F}} + +\newcommand{\boldK}{\bf {K}} +\newcommand{\PP}{\mathcal{x}_{\KBB}} +\newcommand{\M}{\mathcal{M}} +\newcommand{\Ma}{M_0} +\newcommand{\Mb}{M_1} +\newcommand{\MM}{\langle M, M_1 \rangle} +\newcommand{\N}{\mathcal{N}} +\newcommand{\Na}{N_0} +\newcommand{\Nb}{N_1} +\newcommand{\NN}{\langle N, N_1 \rangle} +\newcommand{\MN}{\langle M, N \rangle} +\newcommand{\ff}{{\bf f}} +\newcommand{\uu}{{\bf u}} +\renewcommand{\tt}{{\bf t}} +\newcommand{\mneval}[1]{(I, \MN, \MN)( #1 )} +\newcommand{\meval}[1]{\mneval{#1}} +\newcommand{\mmeval}[1]{\mneval{#1}} +\newcommand{\KBA}{\textsf{KA}} +\newcommand{\OO}{\mathcal{O}} +\newcommand{\OBO}[1]{{{\sf OB}_{\OO,#1}}} +\renewcommand{\P}{\mathcal{P}} +\newcommand{\Q}{\mathcal{Q}} +\newcommand{\Pcomp}{\P_{\textrm{\tiny COMP}}} +\newcommand{\Ploop}{\P_{\textrm{\tiny LOOP}}} +\newcommand{\Atoms}{Atoms} +\newcommand{\Loops}{Loops} +\renewcommand{\implies}{\supset} +\renewcommand{\impliedby}{\subset} +\newcommand{\Rule}{rule} +\newcommand{\eval}[2]{#1\big\{#2\big\}} +\newcommand{\lub}[1]{{\bf lub_{#1}~}} +\newcommand{\glb}[1]{{\bf glb_{#1}~}} +\newcommand{\lfp}{{\bf lfp}} +\newcommand{\fix}[1]{{\bf broken} ~{#1}} +\newcommand{\fixpoints}{\textbf{fixpoints}} + +% https://tex.stackexchange.com/questions/118240/how-to-draw-a-border-around-character-in-a-formula +\makeatletter +\renewcommand{\boxed}[1]{\text{\fboxsep=.2em\fbox{\m@th$\displaystyle#1$}}} +\makeatother +\newcommand{\boxedt}[1]{\boxed{\textrm{#1}}} + +\newcommand{\argblank}{\underline{\hspace{.3cm}}} +\renewcommand{\L}{\mathcal{L}} +\newcommand{\squnion}{\sqcup} +\renewcommand{\implies}{\Rightarrow} +\newcommand{\define}{\coloneqq} +\newcommand{\lcomp}[1]{{#1}^{\mathbf{\hspace{.075em}c}}} + +\newcommand{\noncompare}{\bowtie} +% https://tex.stackexchange.com/questions/378087 +\makeatletter +\newcommand\ineq{}% for safety +\DeclareRobustCommand{\ineq}{\mathrel{\mathpalette\rance@ineq\relax}} +\newcommand{\rance@ineq}[2]{% + \vcenter{\hbox{% + $\m@th#1\mkern1.5mu\underline{\mkern-1.5mu\bowtie\mkern-1.5mu}\mkern1.5mu$% + }}% +} +\makeatother +\newcommand{\noncompareeq}{\ineq} + + + + +\newcommand{\omax}{\textbf{max}} +\newcommand{\omin}{\textbf{min}} + +\newcommand{\project}[2]{\Pi_{#1}(#2)} + +\newcommand{\mknfmodels}{\models_{\mbox{\tiny{\sf MKNF}}}} \ No newline at end of file diff --git a/document.tex b/document.tex new file mode 100644 index 0000000..6fa722a --- /dev/null +++ b/document.tex @@ -0,0 +1,179 @@ +\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} + + \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} \ No newline at end of file