.

betastable/Makefile

@@ -0,0 +1,11 @@
+all: report.pdf
+
+%.pdf: %.tex
+	latexmk -f -e '$$max_repeat=10' -pdf $<
+
+clean:
+	${RM} *.pdf
+	${RM} *.bbl
+	${RM} *.blg
+
+	latexmk -C

betastable/report.tex

@@ -0,0 +1,129 @@
+\documentclass{article}
+
+\usepackage{xspace}
+\usepackage{hyperref}
+\usepackage{bm}
+\usepackage[english]{babel}
+\usepackage{amsthm}
+\usepackage{amsmath}
+\usepackage{mathtools}
+\usepackage{hyperref}
+\hypersetup{
+colorlinks=true,
+linkcolor=black,
+filecolor=black,      
+urlcolor=black,
+pdfpagemode=FullScreen,
+}
+
+\input{../notation.tex}
+\input{../glossary.tex}
+\pagenumbering{arabic}
+\pagestyle{plain}
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{corollary}{Corollary}
+\newtheorem{lemma}{Lemma}
+\newtheorem{proposition}{Proposition}
+\newtheorem{definition}{Definition}
+\newtheorem{example}{Example}
+
+
+\title{Consistent n-Approximators ($\beta$)}
+\author{}
+\date{}
+
+\begin{document}
+
+\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}
+
+\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
+    \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}
+
+
+% iven an \gls{ndao} $o$, its {\em $\beta$-n-stable fixpoints} are fixpoints of the following    
+%     \begin{align*}
+%         B^o_{high}(x) &\define \{ a ~|~ a \in o({x}, a), \neg \exists a',
+%         \\ &\hspace{1.5cm}(\boxed{x \preceq_{}}~ a' \prec_{} a) \land (a' \in o({x}, a))) \}\\
+%         S(o)(x, y) &\define (C^{o}_{low}(y), B^{o}_{high}(x))
+%     \end{align*}}
+
+% \newcommand{\betastablefixpoint}{\hyperlink{glossary:betastablefixpoint}{$\beta$-stable fixpoint}}
+% \newglossaryentry{betastablefixpoint}{
+%     name={$\beta$-stable fixpoint},
+%     description={
+%         An \gls{interpretation} $(T, P)$ is a {\em $\alpha$-stable fixpoint} (or a $\beta$-stable fixpoint) if it is a \gls{fixpoint} of some $h \in H$ and for each $h' \in H$, none of the following hold
+%         \begin{enumerate}[(i.)]
+%             \item $\stablerevisionoperator(h')(T, P)_1 \prec_{} T$,
+%             \item ($\alpha$-stable only)~$\stablerevisionoperator(h')(T, P)_2 \prec_{} P$, nor
+%             \item ($\beta$-stable only) $\exists Z \in \L, T \preceq_{} (h'(T, Z)_2 = Z) \prec_{} P$
+%         \end{enumerate}
+% }}
+
+
+
+
+
+
+\bibliographystyle{plain}
+\bibliography{../references}
+
+\end{document}

glossary.tex

@@ -1,21 +1,45 @@
-\newcommand{\definition}[2]{\hypertarget{glossary:#1}{#2}}
+\newcommand{\definitionBody}[2]{\hypertarget{glossary:#1}{#2}}
 \newcommand{\definitionLink}[2]{\hyperlink{glossary:#1}{#2}\xspace}
 
 
 \newcommand{\Monotone}{\definitionLink{monotone}{monotone}}
 \newcommand{\Image}{\definitionLink{image}{monotone}}
-\let\imageNoLink\image
+\let\imageNoLink\image{}
 \renewcommand{\image}[1]{\imageNoLink{#1}}
-\let\lubNoLink\lub
+\let\lubNoLink\lub{}
 \renewcommand{\lub}{\definitionLink{lubglb}{\lubNoLink}}
-\let\glbNoLink\glb
+\let\glbNoLink\glb{}
 \renewcommand{\glb}{\definitionLink{lubglb}{\glbNoLink}}
 \newcommand{\CompleteLattice}{\definitionLink{completelattice}{complete lattice}}
+\let\LLNoLink\LL{}
+\renewcommand{\LL}{\definitionLink{completelattice}{\LLNoLink}}
 
-\let\topNoLink\top
+\let\topNoLink\top{}
 \renewcommand{\top}{\definitionLink{topbot}{\topNoLink}}
-\let\botNoLink\bot
+\let\botNoLink\bot{}
 \renewcommand{\bot}{\definitionLink{topbot}{\botNoLink}}
 
 \let\fixpointsOfNoLink\fixpointsOf{}
 \renewcommand{\fixpointsOf}{\definitionLink{fixpointsOf}{\fixpointsOfNoLink}}
+
+\let\powersetNoLink\powerset{}
+\renewcommand{\powerset}{\definitionLink{powerset}{\powersetNoLink}}
+\let\powersetONoLink\powersetO{}
+\renewcommand{\powersetO}{\definitionLink{powerset}{\powersetONoLink}}
+
+\newcommand{\Poset}{\definitionLink{poset}{poset}}
+\let\lteNoLink\lte{}
+\renewcommand{\lte}{\definitionLink{poset}{\lteNoLink}}
+\let\lteSubNoLink\lteSub{}
+\renewcommand{\lteSub}[1]{\definitionLink{poset}{\lteSubNoLink{#1}}}
+
+
+\newcommand{\Ndao}{\definitionLink{ndao}{ndao}}
+\newcommand{\AnNdao}{an \definitionLink{ndao}{ndao}}
+\newcommand{\AnNdaoO}{An \definitionLink{ndao}{ndao}}
+\newcommand{\Interpretation}{\definitionLink{interpretation}{interpretation}}
+
+\newcommand{\Prefixpoint}{\definitionLink{prefixpoint}{prefixpoint}}
+
+\newcommand{\minLattice}{\bm{min}}
+\newcommand{\maxLattice}{\bm{max}}

notation.tex

@@ -1,8 +1,13 @@
 \newcommand{\fixpointsOf}{\textbf{\textit{fix}}}
-\renewcommand{\L}{\mathcal{L}}
+\newcommand{\LL}{\mathcal{L}}
 \newcommand{\lte}{\preceq}
+\newcommand{\lteSub}[1]{\lteNoLink_{#1}}
 \newcommand{\image}[1]{[#1]}
 \newcommand{\define}{\coloneqq}
 \newcommand{\union}{\cup}
 \newcommand{\glb}{\bigwedge}
 \newcommand{\lub}{\bigvee}
+\newcommand{\powerset}{\wp}
+\newcommand{\powersetO}{\wp^o}
+\newcommand{\upclosure}{\uparrow}
+\newcommand{\downclosure}{\downarrow}

note.out

@@ -0,0 +1,2 @@
+\BOOKMARK [1][-]{section.1}{\376\377\000B\000a\000c\000k\000g\000r\000o\000u\000n\000d}{}% 1
+\BOOKMARK [1][-]{section.2}{\376\377\000C\000o\000n\000t\000e\000n\000t}{}% 2

note.tex

@@ -7,7 +7,14 @@
 \usepackage{amsthm}
 \usepackage{amsmath}
 \usepackage{mathtools}
-\newcommand{\jh}[1]{{\leavevmode\color{blue!50!red}#1}}
+\usepackage{hyperref}
+\hypersetup{
+colorlinks=true,
+linkcolor=black,
+filecolor=black,      
+urlcolor=black,
+pdfpagemode=FullScreen,
+}
 
 \input{notation.tex}
 \input{glossary.tex}
@@ -23,18 +30,17 @@
 
 % \maketitle
 
-\definition{monotone}{define monotone}
-\definition{image}{define set image}
-\definition{lubglb}{define glb and lub}
-\definition{topbot}{define $\top$ and $\bot$}
-\definition{completelattice}{define complete lattice}
 
 Hello world\cite{tarskilatticetheoretical1955}
 First, we generalize Knaster-Tarski Fixpoint Theorem.
 
-$$\fixpointsOf(S)$$
 
 
+\section{Background}
+\input{sections/background.tex}
+
+\section{Content}
+
 \begin{theorem}[Tarski-Knaster Fixpoint Theorem~\cite{tarskilatticetheoretical1955}]\label{tarskitheorem}
     For a \Monotone function $o$ over a \CompleteLattice $\langle \L, \lte \rangle$, we have that $\langle \fixpointsOf(o), \lte \rangle$ is a \CompleteLattice.
 \end{theorem}

sections/background.tex

@@ -0,0 +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}{
+    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$.
+With abuse to notation, when given a set of functions $F$, we write $\bigcup \{ f\image{A} ~|~ f \in F \}$ as $F\image{A}$.}