init
This commit is contained in:
commit
ac11a73a1a
GPG Key ID:
F307025B65C860BA
|
|
@ -0,0 +1,5 @@
|
|||
*
|
||||
!.gitignore
|
||||
!*.tex
|
||||
!*.bib
|
||||
!Makefile
|
||||
|
|
@ -0,0 +1,11 @@
|
|||
all: document.pdf
|
||||
|
||||
%.pdf: %.tex common.tex
|
||||
latexmk -pdf $<
|
||||
|
||||
clean:
|
||||
${RM} *.pdf
|
||||
${RM} *.bbl
|
||||
${RM} *.blg
|
||||
|
||||
latexmk -C
|
||||
|
|
@ -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}}}}
|
||||
|
|
@ -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}
|
||||
Loading…
Reference in New Issue