From 376900f28c80afa0a911d3cc97f0722184152188 Mon Sep 17 00:00:00 2001 From: Spencer Killen Date: Wed, 27 Nov 2024 17:41:29 -0700 Subject: [PATCH] . --- betastable/report.out | 3 + betastable/report.tex | 23 ++---- betastable/sections/preliminaries.tex | 112 ++++++++++++++++++++++++++ glossary.tex | 30 +++++++ notation.tex | 9 +++ sections/background.tex | 14 ++-- 6 files changed, 167 insertions(+), 24 deletions(-) create mode 100644 betastable/sections/preliminaries.tex diff --git a/betastable/report.out b/betastable/report.out index e69de29..410b601 100644 --- a/betastable/report.out +++ b/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 diff --git a/betastable/report.tex b/betastable/report.tex index a704613..cb96ec1 100644 --- a/betastable/report.tex +++ b/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} - \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} +\section{Preliminaries} +\input{sections/preliminaries.tex} + \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 diff --git a/betastable/sections/preliminaries.tex b/betastable/sections/preliminaries.tex new file mode 100644 index 0000000..ced708d --- /dev/null +++ b/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} \ No newline at end of file diff --git a/glossary.tex b/glossary.tex index b549b22..3670186 100644 --- a/glossary.tex +++ b/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}} diff --git a/notation.tex b/notation.tex index d3dc1e8..c856ada 100644 --- a/notation.tex +++ b/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}} \ No newline at end of file diff --git a/sections/background.tex b/sections/background.tex index 0ba0182..fdfec3b 100644 --- a/sections/background.tex +++ b/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.} -\definition{poset}{ +\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. } -\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$.} -\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$} -\definition{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)$} -\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{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}$.}