fixpoint-theory-nov24/betastable/sections/preliminaries.tex

\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$
\end{definitionOf}

The symmetric version

\begin{definitionOf}{deterministicbetastablerevisionoperator}
    Given \AnApproximator $o: \LL^2 \rightarrow \LL^2$
    \begin{align*}
        \Sdetbeta(o)(x, y)_1 \define \glb_{\lte} \big( \fixpointsOf(o(\partialApp, y)_1)  \setminus ((x \upclosure) \setminus (y \downclosure)) \big)
        \\
        \Sdetbeta(o)(x, y)_2 \define \glb_{\lte} \big( \fixpointsOf(o(x, \partialApp)_2) \setminus ((y \downclosure) \setminus (x \upclosure)) \big)
    \end{align*}

    % This symmetric version likely only works on so-called "A-prudent" pairs
    \begin{align*}
        \Sdetbeta(o)(x, y)_1 \} &\define \glb ( 
            \fixpointsOf(o(\partialApp, y)_1) \setminus
            \Big( ((x \glbBinary y) \upclosure) \symmetricdifference ((x \lubBinary y) \downclosure) \Big)
         )\\
        \Sdetbeta(o)(x, y)_2 &\define \Sdetbeta(o)(y, x)_1
    \end{align*}
\end{definitionOf}


\begin{theorem}
    For \AnApproximator $o: \LL^2 \rightarrow \LL^2$ s.t.\ $o\image{\LL^c} \subseteq \LL^c$, we have that
    $\Sdet(o\restriction_{\LL^c})$ and $\Sdetbeta(o)$ are equivalent.
\end{theorem}
\begin{proof}
    First we simplify $\Sdetbeta(o)(x, y)_1$
    \begin{calculation}[=]
        \minLattice_{\lte} ( 
            \fixpointsOf(o(\partialApp, y)_1) \setminus
            \Big( ((x \glbBinary y) \upclosure) \symmetricdifference ((x \lubBinary y) \downclosure) \Big)
        \step{inside: 
        \begin{subcalculation}[=]
            ((x \glbBinary y) \upclosure) \symmetricdifference ((x \lubBinary y) \downclosure)
            \step{Applying $x \lte y$}
            (x \upclosure) \symmetricdifference (y \downclosure)
            \step{Expand $\symmetricdifference$}
            (x \upclosure \union~ y \downclosure) \setminus (x \upclosure \intersect~ y \downclosure)
            \step{Using $\fixpointsOf(o(\partialApp, y)_1) \subseteq (y \downclosure)$ we don't quite have this yet tho}
            \LL \setminus (x \upclosure \intersect~ y \downclosure)
        \end{subcalculation}}
        \step[]{Aside \begin{subcalculation}
            \step[]{By Assumption}
            \forall x \in [\bot, y],~ o(\partialApp, y)_1 \in [\bot, y]
            \step[\implies]{Follows}
            \fixpointsOf(o)
        \end{subcalculation}}
        \step{Leverage $\fixpointsOf(o(\partialApp, y)_1) \subseteq [\bot, y]$}
        BNy bye
        \step*{sdshds}
        jdskdjsk
    \end{calculation}
\end{proof}


\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}