From f7ad76a40e2bc48f7f1c923e6f4e75b7b8c1592a Mon Sep 17 00:00:00 2001 From: Spencer Killen Date: Mon, 20 Jan 2025 15:11:17 -0700 Subject: [PATCH] . --- betastable/report.out | 4 ++- betastable/report.tex | 47 +++------------------------ betastable/sections/preliminaries.tex | 2 +- betastable/sections/sketchjan20.tex | 6 ++++ betastable/sections/sketchnov20.tex | 43 ++++++++++++++++++++++++ glossary.tex | 4 ++- 6 files changed, 60 insertions(+), 46 deletions(-) create mode 100644 betastable/sections/sketchjan20.tex create mode 100644 betastable/sections/sketchnov20.tex diff --git a/betastable/report.out b/betastable/report.out index 410b601..238315a 100644 --- a/betastable/report.out +++ b/betastable/report.out @@ -1,3 +1,5 @@ \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 +\BOOKMARK [1][-]{section.3}{\376\377\000D\000e\000t\000e\000r\000m\000i\000n\000i\000s\000t\000i\000c\000\040\000A\000F\000T}{}% 3 +\BOOKMARK [1][-]{section.4}{\376\377\000S\000k\000e\000t\000c\000h\000\040\000N\000o\000v\000\040\0002\0000}{}% 4 +\BOOKMARK [1][-]{section.5}{\376\377\000S\000k\000e\000t\000c\000h\000\040\000J\000a\000n\000\040\0002\0000}{}% 5 diff --git a/betastable/report.tex b/betastable/report.tex index 807e5fd..69c71c8 100644 --- a/betastable/report.tex +++ b/betastable/report.tex @@ -45,50 +45,11 @@ pdfpagemode=FullScreen, \section{Preliminaries} \input{sections/preliminaries.tex} +\section{Sketch Nov 20} +\input{sections/sketchnov20.tex} -\begin{definition} - \AnNdaoO is {\em extra consistent} if for every $\lte$-\Prefixpoint $y$ of $o(x, \cdot)_2$, $x \lte y$. -\end{definition} - - - -\begin{definition} - "beta" stable revision - \begin{align*} - S(o)(x, y)_2 \define \minLattice_{\lte}(\fixpointsOf(o(x, \cdot)) \setminus ((y \downclosure) \setminus (x \upclosure))) - \end{align*} -\end{definition} - - -\begin{theorem} - For an extra consistent \Ndao $o$, regular stable revision is equivalent to beta stable revision -\end{theorem} - -\begin{example} - SHowing without ultra consistency - \begin{align*} - o(x, y) \define (\{ \bot \}, \{ \bot \}) - \end{align*} - below properties don't hold -\end{example} - -\begin{proposition}\label{prop:ultra-consistency} - Works fo rdouble sided ordering - Given \AnNdaoO $o: \LL^2 \rightarrow \powersetO(\L)^2$ that is \Monotone from $\lte_p^2$ to $<_p^2$,\ we have for any consistent pair $(x, y) \in \LL^2$, - \begin{align*} - o(x, y) \lte_p^2 (o(x, y)_2, o(x, y)_1) - \end{align*} -\end{proposition} - -\begin{lemma} - This probably needs double sides :() - Given an \Ndao $o$, if $y$ is a \Prefixpoint of $o(x, \cdot)_2$, then for some $y' \in o(x, \cdot)_2$, we have - $x \lte y' \lte y$. -\end{lemma} -\begin{proof} - begin -\end{proof} - +\section{Sketch Jan 20} +\input{sections/sketchjan20.tex} % iven an \gls{ndao} $o$, its {\em $\beta$-n-stable fixpoints} are fixpoints of the following % \begin{align*} diff --git a/betastable/sections/preliminaries.tex b/betastable/sections/preliminaries.tex index 5b23277..14a004b 100644 --- a/betastable/sections/preliminaries.tex +++ b/betastable/sections/preliminaries.tex @@ -16,7 +16,7 @@ With abuse to notation, when given a set of functions $F$, we write $\bigcup \{ -\section{Deternministic AFT} +\section{Deterministic AFT} The original definition of approximators from Denecker et al.\ \cite{denecker2000approximations}, which has been relaxed following Heyninck et al.\ \cite{nondet2}. diff --git a/betastable/sections/sketchjan20.tex b/betastable/sections/sketchjan20.tex new file mode 100644 index 0000000..e074fee --- /dev/null +++ b/betastable/sections/sketchjan20.tex @@ -0,0 +1,6 @@ + +\begin{definitionOf}{chain} + Given a \Poset $\langle \LL, \lte \rangle$, a {\em chain} is a (possibly empty) set $C \subseteq \LL$ that is totally ordered, that is, + for all $x, y \in C$ either $x \lte y$ or $y \lte x$. + +\end{definitionOf} \ No newline at end of file diff --git a/betastable/sections/sketchnov20.tex b/betastable/sections/sketchnov20.tex new file mode 100644 index 0000000..4576498 --- /dev/null +++ b/betastable/sections/sketchnov20.tex @@ -0,0 +1,43 @@ + +\begin{definition} + \AnNdaoO is {\em extra consistent} if for every $\lte$-\Prefixpoint $y$ of $o(x, \cdot)_2$, $x \lte y$. +\end{definition} + + + +\begin{definition} + "beta" stable revision + \begin{align*} + S(o)(x, y)_2 \define \minLattice_{\lte}(\fixpointsOf(o(x, \cdot)) \setminus ((y \downclosure) \setminus (x \upclosure))) + \end{align*} +\end{definition} + + +\begin{theorem} + For an extra consistent \Ndao $o$, regular stable revision is equivalent to beta stable revision +\end{theorem} + +\begin{example} + SHowing without ultra consistency + \begin{align*} + o(x, y) \define (\{ \bot \}, \{ \bot \}) + \end{align*} + below properties don't hold +\end{example} + +\begin{proposition}\label{prop:ultra-consistency} + Works fo rdouble sided ordering + Given \AnNdaoO $o: \LL^2 \rightarrow \powersetO(\L)^2$ that is \Monotone from $\lte_p^2$ to $<_p^2$,\ we have for any consistent pair $(x, y) \in \LL^2$, + \begin{align*} + o(x, y) \lte_p^2 (o(x, y)_2, o(x, y)_1) + \end{align*} +\end{proposition} + +\begin{lemma} + This probably needs double sides :() + Given an \Ndao $o$, if $y$ is a \Prefixpoint of $o(x, \cdot)_2$, then for some $y' \in o(x, \cdot)_2$, we have + $x \lte y' \lte y$. +\end{lemma} +\begin{proof} + begin +\end{proof} diff --git a/glossary.tex b/glossary.tex index 3670186..8041629 100644 --- a/glossary.tex +++ b/glossary.tex @@ -72,4 +72,6 @@ \newcommand{\Prefixpoint}{\definitionLink{prefixpoint}{prefixpoint}} \newcommand{\minLattice}{\bm{min}} -\newcommand{\maxLattice}{\bm{max}} \ No newline at end of file +\newcommand{\maxLattice}{\bm{max}} + +\newcommand{\Chain}{\definitionLink{chain}{chain}}