diff --git a/glossary.tex b/glossary.tex index 5641d24..b04a844 100644 --- a/glossary.tex +++ b/glossary.tex @@ -6,8 +6,16 @@ \newcommand{\Image}{\definitionLink{image}{monotone}} \let\imageNoLink\image \renewcommand{\image}[1]{\imageNoLink{#1}} +\let\lubNoLink\lub +\renewcommand{\lub}{\definitionLink{lubglb}{\lubNoLink}} +\let\glbNoLink\glb +\renewcommand{\glb}{\definitionLink{lubglb}{\glbNoLink}} \newcommand{\CompleteLattice}{\definitionLink{completelattice}{complete lattice}} +\let\topNoLink\top +\renewcommand{\top}{\definitionLink{topbot}{\topNoLink}} +\let\botNoLink\bot +\renewcommand{\bot}{\definitionLink{topbot}{\botNoLink}} \let\fixpointsOfNoLink\fixpointsOf{} \renewcommand{\fixpointsOf}{\definitionLink{fixpointsOf}{\fixpointsOfNoLink}} diff --git a/notation.tex b/notation.tex index 9ad9192..9b82aef 100644 --- a/notation.tex +++ b/notation.tex @@ -3,4 +3,6 @@ \newcommand{\lte}{\preceq} \newcommand{\image}[1]{[#1]} \newcommand{\define}{\coloneqq} -\newcommand{\union}{\cup} \ No newline at end of file +\newcommand{\union}{\cup} +\newcommand{\glb}{\bigwedge} +\newcommand{\lub}{\bigvee} diff --git a/note.tex b/note.tex index 6bc17db..d7e492b 100644 --- a/note.tex +++ b/note.tex @@ -15,6 +15,9 @@ \pagestyle{plain} \newtheorem{theorem}{Theorem} +\newtheorem{corollary}{Corollary} +\newtheorem{lemma}{Lemma} +\newtheorem{proposition}{Proposition} \begin{document} @@ -22,6 +25,8 @@ \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} @@ -30,31 +35,76 @@ First, we generalize Knaster-Tarski Fixpoint Theorem. $$\fixpointsOf(S)$$ -\begin{theorem}[Tarski-Knaster Fixpoint Theorem~\cite{tarskilatticetheoretical1955}] +\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} \begin{theorem} + Trivial attempt using set preimage / image to attain LUB / GLB in image lattice does not work. + + Consider antichain of 2 that map to a chain in image. + The antichain's LUB does maps to a third, distinct element which extends the chain to three in the image + + If we attain LUB of preimage, then its not the least element :) +\end{theorem} + +\begin{theorem}\label{imagelattice} For a \Monotone function $o$ over a \CompleteLattice $\langle \L, \lte \rangle$, we have that $\langle o\imageNoLink{\L}, \lte \rangle$ is a \CompleteLattice. \end{theorem} \begin{proof} - Consider $\langle \L', \lte' \rangle$ where + Consider $\langle \L', \lte \rangle$ where \begin{align*} \L' \define \{ x' ~|~ x \in \L \} \\ - x' \lte' y' \iff x \lte y \textrm{ where } x, y \in \L + x' \lte y' \iff x \lte y \textrm{ where } x, y \in \L \end{align*} Clearly, $\langle \L', \lte' \rangle$ is a \CompleteLattice. - Combining $\L$ and $\L'$ + Combining $\L$ and $\L'$, we formulate $\L^*$: \begin{align*} - \L^* \define \{ \top^*, \bot^* \} \union \L \union \L' \\ - \forall x^*, y^* \in \L^*, x^* \lte y^* \iff \begin{cases} - (x^* = \bot^*) \lor (y^* = \top^*) \\ - two \\ - three + \L^* &\define \{ \top^*, \bot^* \} \union \L \union \L' \\ + \forall x^*, y^* \in \L^*, x^* \lte y^* &\iff \begin{cases} + (x^* = \bot^*) \lor (y^* = \top^*), \\ + \textrm{or } x, y \in \L, \\ + \textrm{or } x', y' \in \L' \end{cases} \end{align*} + It is easy to show that $\langle \L^*, \lte \rangle$ is a \CompleteLattice. + Consider the operator $o^*$ that maps elements from $\L$ to $\L'$ and every element in $\L'$ to itself. + \begin{align*} + o^*(x) \define \begin{cases} + o(x)' & \textrm{if } x \in \L \\ + x & \textrm{otherwise} + \end{cases} + \end{align*} + We have $o^*\image{\L \union \L'} \subseteq L'$ and $\fixpointsOf(o^*) = o\image{\L}' \union \{ \bot^*, \top^* \}$. + By Tarski-Knaster Fixpoint Theorem (Theorem \ref{tarskitheorem}), $\fixpointsOf(o^*)$ is a \CompleteLattice. + Thus, $o\image{\L} \union \{ \bot^*, \top^* \}$ is a \CompleteLattice. For any $S \subseteq \L$, we have $\glb S \not\in \{ \bot^*, \top^* \}$ and $\lub S \not\in \{ \bot^*, \top^* \}$, thus $\langle o\image{\L}, \preceq \rangle$ is a \CompleteLattice. \end{proof} +The following follows directly from the contrapositive of Theorem \ref{imagelattice}. +\begin{corollary} + If $\langle o\image{\L}, \lte \rangle$ is not a \CompleteLattice, then $o$ is not \Monotone. +\end{corollary} + + +\begin{definition} + An approximator set $H$ captures a nondeterministic approximator $o$ if for each consistent pair $(x, y)$ + \begin{align*} + (H\image{(x, y)}_1, H\image{(x, y)}_2) = o(x, y) + \end{align*} +\end{definition} + +\begin{theorem} + A nondeterministic approximator $o$ has a set of +\end{theorem} + +\begin{theorem} + For any nondeterministic approximator $o$, there exists an approximator set $H$ s.t.\ gamma stable models correspond to n-stable models +\end{theorem} +\begin{proof} + foo +\end{proof} + + \bibliographystyle{plain} \bibliography{references}