.

betastable/report.out

@@ -0,0 +1,3 @@
+\BOOKMARK [1][-]{section.1}{\376\377\000P\000r\000e\000l\000i\000m\000i\000n\000a\000r\000i\000e\000s}{}% 1
+\BOOKMARK [1][-]{section.2}{\376\377\000L\000a\000t\000t\000i\000c\000e\000\040\000T\000h\000e\000o\000r\000y}{}% 2
+\BOOKMARK [1][-]{section.3}{\376\377\000D\000e\000t\000e\000r\000n\000m\000i\000n\000i\000s\000t\000i\000c\000\040\000A\000F\000T}{}% 3

betastable/report.tex

@@ -1,6 +1,9 @@
 \documentclass{article}
 
+\usepackage{natbib}
 \usepackage{xspace}
+\usepackage{xparse}
+\usepackage{environ}
 \usepackage{hyperref}
 \usepackage{bm}
 \usepackage[english]{babel}
@@ -37,29 +40,15 @@ pdfpagemode=FullScreen,
 
 \maketitle
 
-\begin{definition}
+\section{Preliminaries}
-    \AnNdaoO is a $\langle \lte, \lte \rangle$-\Monotone function $o: \LL^2 \rightarrow \powersetO(\LL^2)$ s.t.\ for any $x \in \LL^2$
+\input{sections/preliminaries.tex}
-    \begin{itemize}
+
-        \item $o(x, x)_1 = o(x, x)_2$
-    \end{itemize}
-\end{definition}
 
 \begin{definition}
     \AnNdaoO is {\em extra consistent} if for every $\lte$-\Prefixpoint $y$ of $o(x, \cdot)_2$, $x \lte y$.
 \end{definition}
-What about the bottom half does it matter?
 
-\begin{lemma}[From Heyninck]
-    \AnNdaoO is consistent, for every $(x, y)$, $o(x, y)_1 \times o(x, y)_2$ contains at least one consistent pair.
-\end{lemma}
 
-\begin{definition}
-    Regular stable revision
-    \begin{align*}
-        S(o)(x, y)_1 \define \minLattice_{\lte}(\fixpointsOf(o(\cdot, y))) \\
-        S(o)(x, y)_2 \define \minLattice_{\lte}(\fixpointsOf(o(x, \cdot)))
-    \end{align*}
-\end{definition}
 
 \begin{definition}
     "beta" stable revision

betastable/sections/preliminaries.tex

@@ -0,0 +1,112 @@
+\section{Lattice Theory}
+
+
+
+\definitionBody{powerset}{Given a set $S$, we denote its powerset, i.e.\ $\{ x \subseteq S \}$ with $\powerset(S)$. We use $\powersetO(S)$ to denote the powerset of $S$ without the empty set.}
+\definitionBody{poset}{
+    We call $\langle S, \lte \rangle$ a {\em poset} (a partially ordered set) if $\lte$ is reflexive, transitive and antisymmetric. 
+}
+\definitionBody{lubglb}{An element is an {\em upper or lower bound} of a subset $S$ of a \Poset if it is greater than or equal or less than or equal, respectively, to every element inside $S$.}
+\definitionBody{completelattice}{A {\em complete lattice} is a \Poset $\langle \LL, \lte \rangle$ s.t.\ every subset $S$ of $\LL$ has a unique greatest lower bound $\glb^{\LL} S$ and least upper bound $\lub^{\LL} S$}
+\definitionBody{topbot}{We use $\top^{\LL}$ and $\bot^{\LL}$ to denote $\lub^{\LL} \LL$ and $\glb^{\LL} \LL$ respectively.}
+\definitionBody{monotone}{A function $f: A \rightarrow B$ is {\em monotone} w.r.t. the orderings $\langle A, \lteSub{A} \rangle$ and $\langle B, \lteSub{B} \rangle$ if for all $a_1, a_2 \in A$, $a_1 \lte a_2$ implies $f(a_1) \lte f(a_2)$}
+\definitionBody{image}{Given a function $f: A \rightarrow B$, we use $f[A]$ to denote the {\em image of $f$} w.r.t.\ $A$, i.e.\ the set $\{ f(a) ~|~ a \in A \} \subseteq B$.
+With abuse to notation, when given a set of functions $F$, we write $\bigcup \{ f\image{A} ~|~ f \in F \}$ as $F\image{A}$.}
+
+
+
+
+\section{Deternministic AFT}
+
+The original definition of approximators from Denecker et al.\ \cite{denecker2000approximations}, which has been relaxed following Heyninck et al.\ \cite{nondet2}.
+
+
+% \begin{definition}
+%     \definitionBody{deterministicapproximator}{
+%         A {\em deterministic approximator} $o: \LL \rightarrow \LL$ is an \Exact \Monotone function over a \CompleteLattice $\langle \LL, \lte \rangle$
+%     }
+% \end{definition}
+
+\begin{definitionOf}{deterministicapproximator}
+    A {\em deterministic approximator} $o: \LL \rightarrow \LL$ is an \Exact \Monotone function over a \CompleteLattice $\langle \LL, \lte \rangle$
+\end{definitionOf}
+
+\begin{definitionOf}{deterministicstablerevisionoperator}
+    Given \AnApproximator $o: \LL \rightarrow \LL$, its {\em stable revision operator $S(o): \LL^2 \rightarrow \LL^2$} as follows:
+    \begin{align*}
+        S(o)(x, y) \define (\lfp~o(\partialApp, y), \lfp~(x, \partialApp))
+    \end{align*}
+\end{definitionOf}
+
+In later work, Denecker et al.~\cite{DeneckerMT04} establish an alternative theory of AFT based around operators that are restricted to the smaller domain, $\LL^c = \{ (x, y) \in \LL^2 ~|~ x \lte y \}$.
+The set $\L^c$ only contains the pairs that are \ConsistentPair.
+\definitionBody{consistentpair}{A pair $(x, y)$ is {\em consistent} if $x \lte y$.}
+\begin{definitionOf}{deterministicbetaapproximator}
+    A {\em $\beta$-approximator} $o \LL^c \rightarrow \LL^c$ is \AnApproximator restricted and closed under $\LL^c$
+\end{definitionOf}
+
+% Critically, stable revision is defined differently for \BetaApproximators
+In the same work, Denecker et al.~\cite{DeneckerMT04} use a slightly different notion of stable revision.
+Because, for a \BetaApproximator $o$, the function for any $(x, y) \in \LL^c$
+\begin{align*}
+    o(\partialApp, y)_1:& \latticeinterval{\bot}{y} \rightarrow \latticeinterval{\bot}{y} \\
+    o(x, \partialApp)_2:& \latticeinterval{x}{\top} \rightarrow \latticeinterval{x}{\top}
+\end{align*}
+So naturally, \Definition{deterministicstablerevisionoperator} applied to \BetaApproximators also uses this limited range.
+For our purposes, we adapt their definition to fit \Approximators and \BetaApproximators.
+\begin{definitionOf}{deterministicbetastablerevisionoperator}
+    Given \AnApproximator $o: \LL^2 \rightarrow \LL^2$
+    \begin{align*}
+        \Sdetbeta(o)(x, y)_1 \define \minLattice_{\lte} \big( \fixpointsOf(o(\partialApp, y)_1)  \setminus ((x \upclosure) \setminus (y \downclosure)) \big)
+        \\
+        \Sdetbeta(o)(x, y)_2 \define \minLattice_{\lte} \big( \fixpointsOf(o(x, \partialApp)_2) \setminus ((y \downclosure) \setminus (x \upclosure)) \big)
+    \end{align*}
+\end{definitionOf}
+
+The symmetric version
+
+\begin{definitionOf}{deterministicbetastablerevisionoperator}
+    Given \AnApproximator $o: \LL^2 \rightarrow \LL^2$
+    \begin{align*}
+        \Sdetbeta(o)(x, y)_1 &\define \minLattice_{\lte} \Bigg( \fixpointsOf(o(\partialApp, y)_1)  \setminus \bigg( 
+            \Big( ((x \glbBinary y) \upclosure) \union ((x \lubBinary y) \downclosure) \Big)
+            \setminus
+            \Big( ((x \glbBinary y) \upclosure) \intersect ((x \lubBinary y) \downclosure) \Big)
+        \bigg) \Bigg)
+        \\
+        \Sdetbeta(o)(x, y)_2 &\define \Sdetbeta(o)(y, x)_1
+    \end{align*}
+\end{definitionOf}
+
+
+\begin{propositionOf}{deterministicstablerevisionoperatorsymmetry}
+    Given an \Approximator $o: \LL^2 \rightarrow \LL^2$ that is \Symmetric, its \BetaStableRevisionOperator $S(o)$ is also \Symmetric.
+    Under symmetry the two are equivalent for consistent partition
+\end{propositionOf}
+\begin{proof}
+    By \Symmetry, we have $\fixpointsOf(o(\partialApp, y)_1) = \fixpointsOf(o(x, \partialApp)_2)$
+\end{proof}
+\Proposition{deterministicstablerevisionoperatorsymmetry}
+
+
+\begin{definition}
+    \AnNdaoO is a $\langle \lte, \lte \rangle$-\Monotone function $o: \LL^2 \rightarrow \powersetO(\LL^2)$ s.t.\ for any $x \in \LL^2$
+    \begin{itemize}
+        \item $o(x, x)_1 = o(x, x)_2$
+    \end{itemize}
+\end{definition}
+
+
+What about the bottom half does it matter?
+
+\begin{lemma}[From Heyninck]
+    \AnNdaoO is consistent, for every $(x, y)$, $o(x, y)_1 \times o(x, y)_2$ contains at least one consistent pair.
+\end{lemma}
+
+\begin{definition}
+    Regular stable revision
+    \begin{align*}
+        S(o)(x, y)_1 \define \minLattice_{\lte}(\fixpointsOf(o(\cdot, y))) \\
+        S(o)(x, y)_2 \define \minLattice_{\lte}(\fixpointsOf(o(x, \cdot)))
+    \end{align*}
+\end{definition}

glossary.tex

@@ -1,8 +1,38 @@
 \newcommand{\definitionBody}[2]{\hypertarget{glossary:#1}{#2}}
 \newcommand{\definitionLink}[2]{\hyperlink{glossary:#1}{#2}\xspace}
+\newcommand{\Definition}[1]{\definitionLink{#1}{Definition~\ref{definition:#1}}}
+\NewEnviron{definitionOf}[1]{
+    \begin{definition}\label{definition:#1}
+        \definitionBody{#1}{\BODY}
+    \end{definition}
+}
+\NewEnviron{propositionOf}[1]{
+    \begin{proposition}\label{proposition:#1}
+        \BODY
+    \end{proposition}
+}
+\newcommand{\Proposition}[1]{\hyperref[proposition:#1]{Proposition~\ref{proposition:#1}}}
 
 
+
+\newcommand{\LeastFixpoint}{\definitionLink{leastfixpoint}{least fixpoint}}
+\newcommand{\ConsistentPair}{\definitionLink{consistentpair}{consistent}}
 \newcommand{\Monotone}{\definitionLink{monotone}{monotone}}
+\newcommand{\Exact}{\definitionLink{deterministicexactapproximator}{exact}}
+\newcommand{\Symmetric}{\definitionLink{deterministicsymmetricapproximator}{symmetric}}
+\newcommand{\Symmetry}{\definitionLink{deterministicsymmetricapproximator}{symmetry}}
+\newcommand{\BetaApproximator}{\definitionLink{deterministicbetaapproximator}{$\beta$-approximator}}
+\newcommand{\BetaStableRevisionOperator}{\definitionLink{deterministicbetastablerevisionoperator}{$\beta$-stable revision operator}}
+\newcommand{\BetaApproximators}{\definitionLink{deterministicbetaapproximator}{$\beta$-approximators}}
+\newcommand{\Approximator}{\definitionLink{deterministicapproximator}{approximator}}
+\newcommand{\Approximators}{\definitionLink{deterministicapproximator}{approximators}}
+\newcommand{\AnApproximator}{\definitionLink{deterministicapproximator}{an approximator}}
+
+\let\SdetNoLink\Sdet
+\renewcommand{\Sdet}{\definitionLink{deterministicstablerevisionoperator}{\SdetNoLink}}
+\let\SdetbetaNoLink\Sdetbeta
+\renewcommand{\Sdetbeta}{\definitionLink{deterministicbetastablerevisionoperator}{\SdetbetaNoLink}}
+
 \newcommand{\Image}{\definitionLink{image}{monotone}}
 \let\imageNoLink\image{}
 \renewcommand{\image}[1]{\imageNoLink{#1}}

notation.tex

@@ -5,9 +5,18 @@
 \newcommand{\image}[1]{[#1]}
 \newcommand{\define}{\coloneqq}
 \newcommand{\union}{\cup}
+\newcommand{\intersect}{\cap}
 \newcommand{\glb}{\bigwedge}
 \newcommand{\lub}{\bigvee}
+\newcommand{\glbBinary}{\land}
+\newcommand{\lubBinary}{\lor}
 \newcommand{\powerset}{\wp}
 \newcommand{\powersetO}{\wp^o}
 \newcommand{\upclosure}{\uparrow}
 \newcommand{\downclosure}{\downarrow}
+\newcommand{\partialApp}{\cdot}
+\newcommand{\lfp}{\textbf{lfp}}
+\newcommand{\latticeinterval}[2]{[#1, #2]}
+
+\newcommand{\Sdet}{S}
+\newcommand{\Sdetbeta}{S^{\beta}}

sections/background.tex

@@ -1,13 +1,13 @@
 
 
 
-\definition{powerset}{Given a set $S$, we denote its powerset, i.e.\ $\{ x \subseteq S \}$ with $\powerset(S)$. We use $\powersetO(S)$ to denote the powerset of $S$ without the empty set.}
+\definitionBody{powerset}{Given a set $S$, we denote its powerset, i.e.\ $\{ x \subseteq S \}$ with $\powerset(S)$. We use $\powersetO(S)$ to denote the powerset of $S$ without the empty set.}
-\definition{poset}{
+\definitionBody{poset}{
     We call $\langle S, \lte \rangle$ a {\em poset} (a partially ordered set) if $\lte$ is reflexive, transitive and antisymmetric. 
 }
-\definition{lubglb}{An element is an {\em upper or lower bound} of a subset $S$ of a \Poset if it is greater than or equal or less than or equal, respectively, to every element inside $S$.}
+\definitionBody{lubglb}{An element is an {\em upper or lower bound} of a subset $S$ of a \Poset if it is greater than or equal or less than or equal, respectively, to every element inside $S$.}
-\definition{completelattice}{A {\em complete lattice} is a \Poset $\langle \LL, \lte \rangle$ s.t.\ every subset $S$ of $\LL$ has a unique greatest lower bound $\glb^{\LL} S$ and least upper bound $\lub^{\LL} S$}
+\definitionBody{completelattice}{A {\em complete lattice} is a \Poset $\langle \LL, \lte \rangle$ s.t.\ every subset $S$ of $\LL$ has a unique greatest lower bound $\glb^{\LL} S$ and least upper bound $\lub^{\LL} S$}
-\definition{topbot}{We use $\top^{\LL}$ and $\bot^{\LL}$ to denote $\lub^{\LL} \LL$ and $\glb^{\LL} \LL$ respectively.}
+\definitionBody{topbot}{We use $\top^{\LL}$ and $\bot^{\LL}$ to denote $\lub^{\LL} \LL$ and $\glb^{\LL} \LL$ respectively.}
-\definition{monotone}{A function $f: A \rightarrow B$ is {\em monotone} w.r.t. the orderings $\langle A, \lteSub{A} \rangle$ and $\langle B, \lteSub{B} \rangle$ if for all $a_1, a_2 \in A$, $a_1 \lte a_2$ implies $f(a_1) \lte f(a_2)$}
+\definitionBody{monotone}{A function $f: A \rightarrow B$ is {\em monotone} w.r.t. the orderings $\langle A, \lteSub{A} \rangle$ and $\langle B, \lteSub{B} \rangle$ if for all $a_1, a_2 \in A$, $a_1 \lte a_2$ implies $f(a_1) \lte f(a_2)$}
-\definition{image}{Given a function $f: A \rightarrow B$, we use $f[A]$ to denote the {\em image of $f$} w.r.t.\ $A$, i.e.\ the set $\{ f(a) ~|~ a \in A \} \subseteq B$.
+\definitionBody{image}{Given a function $f: A \rightarrow B$, we use $f[A]$ to denote the {\em image of $f$} w.r.t.\ $A$, i.e.\ the set $\{ f(a) ~|~ a \in A \} \subseteq B$.
 With abuse to notation, when given a set of functions $F$, we write $\bigcup \{ f\image{A} ~|~ f \in F \}$ as $F\image{A}$.}