diff --git a/betastable/.vscode/settings.json b/betastable/.vscode/settings.json new file mode 100644 index 0000000..afb940f --- /dev/null +++ b/betastable/.vscode/settings.json @@ -0,0 +1,3 @@ +{ + "discord.enabled": true +} \ No newline at end of file diff --git a/betastable/report.tex b/betastable/report.tex index 69c71c8..10ec6e7 100644 --- a/betastable/report.tex +++ b/betastable/report.tex @@ -12,6 +12,8 @@ \usepackage{amssymb} \usepackage{mathtools} \usepackage{hyperref} +\usepackage{xfrac} +\usepackage{stackengine} \usepackage[block]{calculation} \hypersetup{ colorlinks=true, @@ -32,6 +34,7 @@ pdfpagemode=FullScreen, \newtheorem{proposition}{Proposition} \newtheorem{definition}{Definition} \newtheorem{example}{Example} +\newtheorem{remark}{Remark} \title{Consistent n-Approximators ($\beta$)} diff --git a/betastable/sections/sketchjan20.tex b/betastable/sections/sketchjan20.tex index e074fee..b94182b 100644 --- a/betastable/sections/sketchjan20.tex +++ b/betastable/sections/sketchjan20.tex @@ -2,5 +2,62 @@ \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 +\end{definitionOf} + +\begin{definitionOf}{setordering} + Given a preorder, $\langle \LL, \lte \rangle$ + We define a set ordering $\langle \powersetO(\LL), \lte \rangle$ + s.t. for any $X, Y \subseteq \LL$ + \begin{align*} + X \lte Y \textrm{ iff } (X \upclosure) \supseteq Y + \end{align*} +\end{definitionOf} + +\begin{definitionOf}{chaincompleteposet} + We call \Poset $\langle \LL, \lte \rangle$ {\em chain-complete} if $\lub \LL$ is unique and in $\LL$ and for ever chain $C \subseteq \LL$ + \begin{enumerate} + \item $\lub \LL$ is unique and in $\LL$, and + \item for every chain $C \subseteq \LL$, we have $\lub C \in \LL$ + \end{enumerate} +\end{definitionOf} + +\begin{definitionOf}{antisymmequiv} + Given a set $\powersetO(\LL)^2$, define $\antisymmequiv{\powersetO(\LL)^2}$ to be the set obtained by removing any elements $x \in \powersetO(\LL)^2$ s.t. $x \not= x \upprecision$. +\end{definitionOf} + +\begin{remark} + The \Preorder $\langle \powersetO(\LL)^2, \lteSetLPrecision \rangle$ lacks \Antisymmetry, thus it is not a \Poset. + We can construct and equivalence relation $\equiv$ based on the \Antisymmetry condition: + $x \equiv x' \textrm{ iff } x \lteSetLPrecision x' \textrm{ and } x' \lteSetLPrecision x$. + Each equivalence class $[x]$ can be uniquely represented by $x \upprecision$. Thus, another way of viewing + $\langle \antisymmequiv{\powersetO(\LL)^2}, \lteSetLPrecision \rangle$ + is as the quotient under the above equivalence relation. +\end{remark} + +\begin{lemma} + Given $\langle \antisymmequiv{\powersetO(\LL)^2}, \lteSetLPrecision \rangle$, and $x, y \in \powersetO(\LL)^2$ + \begin{enumerate} + \item $x \lteSetRPrecision y$. + \item if $x \lteSetLPrecision y$ then $x \lteSetLRPrecision y$. + \end{enumerate} +\end{lemma} +\begin{proof} + (1) We have $\top_{\ltePrecision} \in y$. (2) Follows from (1). +\end{proof} + + +\begin{propositionOf}{chaincompletepreserve} + Let $\langle \LL, \lte \rangle$ be a \CompleteLattice and $o: \LL^2 \rightarrow \powersetO(\LL)$ \AnNdao. + The structure $\langle \antisymmequiv{o\image{R}}, \lteSetL \rangle$ is a \ChainCompletePoset where $R$ is one of the following: + \begin{enumerate} + \item\label{chaincompletepreserve:enum:a} $\LL^2$, + \item\label{chaincompletepreserve:enum:b} $\LLc$ + \item\label{chaincompletepreserve:enum:c} $\postfixpointsOf(o)$ + \item\label{chaincompletepreserve:enum:d} $\prefixpointsOf(S(o))$ + \end{enumerate} +\end{propositionOf} +\begin{proof} + This should be simpler, the incoming is chain complete poset so should inject one ? + + +\end{proof} \ No newline at end of file diff --git a/glossary.tex b/glossary.tex index 8041629..a641e77 100644 --- a/glossary.tex +++ b/glossary.tex @@ -57,12 +57,22 @@ \let\powersetONoLink\powersetO{} \renewcommand{\powersetO}{\definitionLink{powerset}{\powersetONoLink}} +\newcommand{\Preorder}{\definitionLink{preorder}{preorder}} +\newcommand{\Antisymmetry}{\definitionLink{antisymmetry}{antisymmetry}} \newcommand{\Poset}{\definitionLink{poset}{poset}} +\newcommand{\ChainCompletePoset}{\definitionLink{chaincompleteposet}{chain-complete poset}} +\newcommand{\ChainCompletePosets}{\definitionLink{chaincompleteposet}{chain-complete posets}} +\newcommand{\AChainCompletePoset}{\definitionLink{chaincompleteposet}{a chain-complete poset}} \let\lteNoLink\lte{} \renewcommand{\lte}{\definitionLink{poset}{\lteNoLink}} \let\lteSubNoLink\lteSub{} \renewcommand{\lteSub}[1]{\definitionLink{poset}{\lteSubNoLink{#1}}} +\let\gteNoLink\gte{} +\renewcommand{\gte}{\definitionLink{poset}{\gteNoLink}} +\let\gteSubNoLink\gteSub{} +\renewcommand{\gteSub}[1]{\definitionLink{poset}{\gteSubNoLink{#1}}} + \newcommand{\Ndao}{\definitionLink{ndao}{ndao}} \newcommand{\AnNdao}{an \definitionLink{ndao}{ndao}} diff --git a/notation.tex b/notation.tex index 1289f9c..7466a77 100644 --- a/notation.tex +++ b/notation.tex @@ -1,11 +1,25 @@ + \newcommand{\fixpointsOf}{\textbf{\textit{fix}}} +\newcommand{\prefixpointsOf}{\textbf{\textit{prefix}}} +\newcommand{\postfixpointsOf}{\textbf{\textit{postfix}}} \newcommand{\LL}{\mathcal{L}} \newcommand{\lte}{\preceq} +\newcommand{\ltePrecision}{\preceq_p^2} \newcommand{\lteSub}[1]{\lteNoLink_{#1}} +\newcommand{\gteSub}[1]{\gteNoLink_{#1}} +\newcommand{\gte}{\succeq} +\newcommand{\lteSetR}{\preccurlyeq} +\newcommand{\lteSetRPrecision}{\preccurlyeq_p^2} +\newcommand{\lteSetL}{\curlyeqprec} +\newcommand{\lteSetLPrecision}{\curlyeqprec_p^2} +\newcommand{\lteSetLR}{\mathbin{\stackMath\topinset{\preccurlyeq}{\curlyeqprec}{}{}}} +\newcommand{\lteSetLRPrecision}{\mathbin{\stackMath\topinset{\preccurlyeq}{\curlyeqprec}{}{}_p^2}} \newcommand{\image}[1]{[#1]} \newcommand{\define}{\coloneqq} \newcommand{\union}{\mathbin{\cup}} +\newcommand{\unionBig}{\bigcup} \newcommand{\intersect}{\mathbin{\cap}} +\newcommand{\intersectBig}{\bigcap} \newcommand{\symmetricdifference}{\mathbin{\Delta}} \newcommand{\glb}{\bigwedge} \newcommand{\lub}{\bigvee} @@ -14,6 +28,7 @@ \newcommand{\powerset}{\wp} \newcommand{\powersetO}{\wp^o} \newcommand{\upclosure}{\uparrow} +\newcommand{\upprecision}{\uparrow^2_p} \newcommand{\downclosure}{\downarrow} \newcommand{\partialApp}{\cdot} \newcommand{\lfp}{\textbf{lfp}} @@ -22,4 +37,13 @@ \newcommand{\Sdet}{S} \newcommand{\Sdetbeta}{S^{\beta}} \let\restrictionWithSpaces\restriction -\renewcommand{\restriction}{{\restrictionWithSpaces}} \ No newline at end of file +\renewcommand{\restriction}{{\restrictionWithSpaces}} + +\newcommand{\quotient}[2]{\sfrac{#1}{#2}} + +\newcommand{\antisymmequiv}[1]{\quotient{#1}{\upprecision}} + +\newcommand{\LLc}{\LLNoLink^{c}} + +\newcommand{\projL}{\Pi_{1}} +\newcommand{\projR}{\Pi_{2}} \ No newline at end of file