diff --git a/betastable/Makefile b/betastable/Makefile new file mode 100644 index 0000000..a92e11d --- /dev/null +++ b/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 diff --git a/betastable/report.out b/betastable/report.out new file mode 100644 index 0000000..e69de29 diff --git a/betastable/report.tex b/betastable/report.tex new file mode 100644 index 0000000..a704613 --- /dev/null +++ b/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} diff --git a/glossary.tex b/glossary.tex index b04a844..b549b22 100644 --- a/glossary.tex +++ b/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}} \ No newline at end of file diff --git a/notation.tex b/notation.tex index 9b82aef..d3dc1e8 100644 --- a/notation.tex +++ b/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} diff --git a/note.out b/note.out index e69de29..62081c2 100644 --- a/note.out +++ b/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 diff --git a/note.tex b/note.tex index d7e492b..ac8de84 100644 --- a/note.tex +++ b/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} diff --git a/sections/background.tex b/sections/background.tex index e69de29..0ba0182 100644 --- a/sections/background.tex +++ b/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}$.}