\documentclass[letterpaper]{article}
\include{header}

\renewcommand\l{\lambda}
\newcommand\lub{\bigsqcup}
\newcommand\po{\sqsubseteq}
\newcommand\impl{\Rightarrow}
\newcommand\Def{{\bf Definition}:\ \ }
\newcommand\Prop{{\bf Property}:\ \ }
\newcommand\Pf{{\bf Proof}:\ \ }
\newcommand\Claim{{\bf Claim}:\ \ }
\newcommand\Lemma[1]{{\bf Lemma #1:}\ \ }
\newcommand\pfunc{\longrightarrow\!\!\!\!\!\!\!\!\circ\;\;\; }
\newcommand\compose{\circ}
\newcommand\upb{{\it upper-bound }}
\newcommand\lupb{{\it least-upper-bound }}
\newcommand\LUB{{\it LUB }}
\newcommand\LUBS{\LUB\!\!s\ }
\newcommand\Fenv{\varphi}

\newcommand\myhline{{-----------------------------------------------------------------------------------------------------------------}\nl}


\begin{document}
  \Def a {\bf partial order} (sometimes called a {\it partially ordered set} or {\it poset}) is a pair, $(D, \po)$ where:\nl
  \ipar{
    $D$ is a set and\nl
    $\po$ is a reflexive, transitive, and anti-symetric relation such that:
    \ipar{
      $\forall x.\ x \po x$\nl
      $\forall x,y,z.\ (x \po y) \land (y \po z)\ \impl\ (x \po z)$\nl
      $\forall xy.\ (x \po y) \land (y \po x)\ \impl\ (x = y)$\nl
    }
  }

  \Def Let $X$ be a subset of $D$, then:\nl
  \ipar{
    $d \in D$ is an {\bf upper-bound} (or UB) for $X$ iff $\forall x \in X.\ (x \po d)$
  }

  \begin{figure}[h]
    \setlength{\unitlength}{0.08in}
    \centering
    \begin{picture}(50,10)
      \put(0,7)   {\text{$c$}}
      \put(7.4,7) {$d$}
      \put(0,0)   {$a$}
      \put(7.4,0) {$b$}
      \put(15,6)  {\text{$c$\ \ is an {\it upper-bound} for $\{a,b,c\}$ and}}
      \put(15,4)  {\text{$c\ \&\ d$ are both {\it upper-bounds} for $\{a,b\}$}}
      \put(1,1) {\line(0,1){6}}
      \put(1,1) {\line(1,1){6}}
      \put(7,1) {\line(0,1){6}}
      \put(7,1) {\line(-1,1){6}}
    \end{picture}
  \end{figure}


  \Def $d$ is a {\bf least-upper-bound} (or LUB) for $X$ iff:\nl
  \ipar{
    (1) $d$ is an \upb for $X$ and\nl
    (2) if $d'$ is any \upb for $X$ then $d \po d'$\nl
  }

  \Prop if $d$\ \&\ $d'$ are both \LUBS of $X$ then $d = d'$\nl

  \Pf Since $d$ and $d'$ are \LUBS of $X$, $(d \po d')$ and $(d' \po d)$, $(d = d')$ 
  by {\it anti-symetry} of $\po$\nl
  \ipar{
    - If $\po$ is not {\it anti-symetric} we call it a {\it pre-order}\nl
    - We write $\lub X$ for the \lupb of $X$, if it exists\nl
  }

  What kinds of sets have \LUBS?
  \ipar{
    (1) no restrition: ({\it poset})\nl
    (2) Every finite subset has a \LUB ({\it lattice})\nl
    (3) Every subset has a \LUB ({\it complete lattice})\nl
  }
  
  Somewhere between 1\ \&\ 2 is our interesting class of sets\nl

  \Def Given a {\it poset} $(D, \po)$, $X \subseteq D$ is {\bf directed} iff every finite set $F \subseteq X$ has an \upb in $X$

  \begin{figure}[h]
    \setlength{\unitlength}{0.08in}
    \centering
    \begin{picture}(50,10)
      \put(0,7)   {$c$}
      \put(7.4,7) {$d$}
      \put(0,0)   {$a$}
      \put(7.4,0) {$b$}
      \put(15,4)  {
        \begin{tabular}[h]{l|l}
          directed & not directed \\ \hline
          $\{a,c\}$   & $\{a,b\}$ \\
          $\{a,b,c\}$ & $\{a,b,c,d\}$ \\
          singleton sets \\
          pairs of $\po$ \\
        \end{tabular}
      }
      \put(1,1) {\line(0,1){6}}
      \put(1,1) {\line(1,1){6}}
      \put(7,1) {\line(0,1){6}}
      \put(7,1) {\line(-1,1){6}}
    \end{picture}
  \end{figure}
  
  \Def a {\bf complete-partial-order} (CPO) is a {\it poset} where every {\it directed} subset has a \LUB.\nl
  
  \Def a {\bf pointed-CPO\/} is a CPO with a {\it least-element}, usually {\it bottom}, $(\bot)$\nl

  Any finite PO is a CPO since any directed set $X$ is finite, choose $F = X$ so $X$ has an \upb in $X$, that must be the \LUB.\nl
  
  \pagebreak
  Interesting {\it posets}:\nl
    \ipar{
      \begin{tabular}[h]{rl}
        Singleton: &$\{\cdot\}$, $\mathbf{1}$, or $\mathbf{U}$\\
        2 element: &
        \begin{picture}(20,30)
          \put(2,-10)   {$\bot$}
          \put(2,10) {$\top$}
          \put(0,-6)  {\circle{2}}
          \put(0,13) {\circle{2}}        
          \put(0,-6) {\line(0,1){19}}
        \end{picture}
        or\ \ $\mathbf{O}$
        \\\\
        3 element:&
        \begin{picture}(70,30)
          \put(23.4,-20)   {$\bot$}
          \put(-5,10) {$true$}
          \put(40,10) {$false$}
          \put(27,-10)  {\circle{2}}
          \put(48.5,6)  {\circle{2}}
          \put(5.5,6) {\circle{2}}        
          \put(27,-10) {\line(-4,3){21.5}}
          \put(27,-10) {\line(4,3){21.5}}
        \end{picture}
        , $\mathbf{B}$, or\ \ $\mathbf{T}$\\\\\\
        
        \;\;\;\;\;\;$\omega^\top\ :$& $(\mathbf{N} \cup \{\top\})$\\\\
      \end{tabular}
    }  
    
    If $A$ is any set then $\langle \mathbf{P}(A), \subseteq \rangle$ is a CPO
    \ipar{
      $X \subseteq \mathbf{P}(A)$,\;\; $\lub X = \bigcup X$\nl
    }
    
    If $A$ is any set then $\langle A, \{(x,y)\ |\ x = y\}\rangle$ is a CPO (but not {\it pointed})\nl
    \ipar{
      but, $\langle A\cup\{\bot\}, \{(x,y)\ |\ (x = y) \lor (x = \bot)\}\rangle$ is\nl 
    }\nl
  \myhline
  
  \Def {\bf Products of Posets}
  \smallskip
  
  \ipar{
    $(D, \po_D) \times (E,\po_E) = (D\times E, \po_{D\times E})$\nl
    \phantom{=}where\nl 
    $(d,e) \po_{D\times E} (d',e')$\ \ iff\ \ $(d \po_D) \land (e \po_E e')$\nl
  }

  If $P \subseteq D\times E$ is directed then $P$ has a \LUB\nl

  \Claim Let P be directed, $P_1 = \{x\ |\ \exists y. (x,y) \in P\}$ and 
  $P_2 = \{y\ |\ \exists y. (x,y) \in P\}$,\nl
  \ipar{then $P_1\ \&\ P_2$ are directed}\nl

  \Pf if $\{x_1,...,x_n\} \in P_1$ and $\{y_1,...,y_n\} \in P_2$ such that $\{(x_1,y_1),...,(x_n,y_n)\} \subseteq P$ then\nl
  \ipar{
    by the definition of $\po_{P_1\times P_2}$, since $P$ is directed so are $P_1$ and $P_2$\nl
  }\nl
  
  {\bf Partial Functions}\nl

  \ipar{
    If $S$ and $T$ are sets then $S \pfunc T$ defines the set of {\bf partial-functions} from $S$ to $T$\nl
    \ipar{
      $f \po g$ iff $\forall x\in S$, if $f(x)$ is defined then so is $g(x)$, and $f(x) = g(x)$\nl
    }

    Alternatively:\nl
    \ipar{
      $graph(f) = \{(x,y)\ |\ x \in S\ \land\ y = f(x)\}$, then $f \po g$ iff $graph(f) \subseteq graph(f)$\nl
    }

    $X \subseteq [S \pfunc T]$ is directed iff for any finite $F \subseteq X$, $F$ has a UB in $X$\nl
  }
  
  Let $X \subseteq S \pfunc T$, $F \subset X$ with $F$ finite.\nl
  Let $f \in F = \{(x_1,f(x_1)),...,(x_n,f(x_n))\}$\nl

  We want $g:S \ra T$ such that $g(x) = f(x)$\; if\;\; $\exists f \in X$ such that $f(x)$ is defined\nl

  \Lemma{I}if $f_1, f_2 \in X$ and $f_1(x)\ \&\ f_2(x)$ are defined, then $f_1(x) = f_2(x)$\nl

  \Pf $\{f_1, f_2\}$ is a finite subset of $X$, therefore it has an UB in $X$,\nl
  \ipar{
    i.e. $\exists f_3$ such that $f_1 \po f_3$ and $f_2 \po f_3$.\;\;
    So $f_1(x) = f_3(x)$ and $f_2(x) = f_3(x)$\nl
  }

  This all means that:\nl

  \ipar{
    $S \pfunc T$ is a CPO\nl
  }
  
  \pagebreak
  
  \Def Let $f: D \ra E$ where $D \equiv (D,\po_D)$ and $E \equiv (E, \po_E)$
  \ipar{
    The function $f$ is {\bf monotone} iff $\forall d,d'$, if $d\po_D d'$ then $f(d) \po_E f(d')$\nl
  }

  \Lemma{(Exchange)}\nl
  \ipar{
    Let $D\ \&\ D'$ be CPOs, $P \subseteq D\ \&\ Q \subseteq D'$ be 
    directed, and $D''$ be any {\it poset}.\nl
    Let $f:D \times D \ra D''$ be monotone, then:
      $$\lub_{x \in P} \lub_{y \in Q} f(x,y) = \lub_{y \in Q} \lub_{x \in P} f(x,y)$$
  }


  \Pf Must show that: 
  $$\lub_{x \in P} \lub_{y \in Q} f(x,y) \po \lub_{y \in Q} \lub_{x \in P} f(x,y)\text{\;\; and \;}
  \lub_{y \in Q} \lub_{x \in P} f(x,y) \po \lub_{x \in P} \lub_{y \in Q} f(x,y)$$
  \nl\nl

  First, $\lub_{x \in P}$ is a \LUB, so it suffices to show that
  $$\lub_{y \in Q} \lub_{x \in P} f(x,y)\text{\;\; is an \upb for \;} \{\lub_{y\in Q}f(x,y)\ |\ x \in P\}$$
  So it remains to show that for any $x \in P$
  $$\lub_{y \in Q} f(x,y) \po \lub_{y \in Q} \lub_{x \in P} f(x,y)$$
  
  From there it remains to show that for any $y \in Q$
  $$f(x,y) \po \lub_{y \in Q} \lub_{x \in P} f(x,y)$$
  which is obvious since $f$ is {\it monotone}

  Options:\nl
  \ipar{
    \begin{tabular}[h]{l}
      (1) ... if these \LUBS exist ...\\
      (2) ... let $D''$ be a CPO, then these \LUBS exist ...
    \end{tabular}
  }\nl
   
  \myhline
  
  \Lemma{(Diagonal)}\nl
  \ipar{
    Let $D\ \&\ D'$ be CPOs, $P \subseteq D$ be directed, and $f:D \times D \ra D'$ be monotone\nl
    then:
    $$\lub_{x \in P} \lub_{y \in P} f(x,y) = \lub_{x \in P} f(x,x)$$
  }

  \Pf Homework Excercize $\#$5\nl
  
  There are more notes here from the discussion the day after...\nl

  \myhline\nl
  
  \Def a function $f: D \ra E$ where $D\ \&\ E$ are {\it pointed-CPO\/}s is {\bf strict} iff it is {\it bottom-preserving}.\nl

  \Def a function $f: D \ra E$ where $D\ \&\ E$ are {\it CPO\/}s is {\bf continuous} iff\nl
  \ipar{$\forall X \subseteq D$ where $X$ is directed, $f(\lub X) = \lub_{x\in X} f(x)$.\nl}

  This leads to the following properties:
  \ipar{
    (1) If $f$ is {\it continuous}, then $f$ is {\it monotone} (continuity $\impl$ monotonicity)
    \ipar{
      Let $X = \{a,b\}$ where $a \po b$. Then $X$ is {\it directed}. \nl
      Therefore $f(\lub X) = \lub \{f(x)\ |\ x \in X \}$, So\nl
      \ipar{$f(b) = \lub\{f(a),f(b)\}$, therefore $f(a) \po f(b)$}
    }
    (2) If $f$ is {\it monotone} and $D$ is {\it finite}, then $f$ is {\it continuous}\nl
    (3) If $f$ is {\it monotone} and $D$ has no {\it infinite-increasing-chains}, then $f$ is {\it continuous}\nl
    (4) $f$ is {\it monotone} $\not\impl$ $f$ is {\it continuous}\nl
    \ipar{
      Example:
      \ipar{
        $f: \omega^\top \ra \mathbf{O}$ with $f(\top) = \top$ and $f(n) = \bot$
      }
      $$\lub_{x \in X} f(x) = \bot \text{\;\; and\;\; } f(\lub_{x \in X} x) = \top$$
      \ipar{
        $f$ is not {\it continuous} since \; $\lub f(x) \ne  f(\lub x)$
      }
    }
  }\nl

  \Lemma{\!\!} If $f:D\ra E$ is continuous and $X \subseteq D$ is directed, then 
  $$\lub_{x \in X} f(x) \po f(\lub_{x \in X}x)$$
  
  \Pf For any $x_0 \in X$, $x_0 \po \lub X$, since $f$ is {\it monotone}, $f(x_0) \po \lub f(x)$
  \ipar{
    This is true for all $x_0 \in X$, so\ \ $\lub f(x)$ is an UB for $\{f(x)\ |\ x \in X\}$ and is {\it least}\nl\nl
  }
  
  \Claim If $f:D \ra E$ and $g:E \ra F$ are {\it continuous} then $(g \compose f):D \ra F$ is {\it continuous}\nl
  
  \Pf Must show that: 
  $$(g \compose f)(\lub_{x \in X} x) \po \lub_{x \in X} (g \compose f)(x)$$
  
  \ipar{
    Since $X$ is directed, so is $\{ f(x)\ |\ x\in X\}$ by the above Lemma.\nl
    \renewcommand\arraystretch{1.3}
    \phantom{===}$\begin{array}[h]{rll}
      g(f(\lub X))\;\; =& g(\ \lub\{\ f(x)\ |\ x\in X\})\!\!\!& \text{: by continuity of } f\\
     =& \lub\{\ g(f(x))\ |\ x\in X\}& \text{: by continuity of } g\\
     =& \lub (g \compose f)(x)\\
    \end{array}$\nl\nl
  }

  \pagebreak
  
  \Def $[D \ra E]$ is the set of all {\it continuous} functions from $D \ra E$ such that\nl
  $$f \po_{D\ra E} g \text{\; iff\; }\forall d\in D.\ f(d) \po_E g(d)$$

  

  For some $S$ and $T$\nl

  \ipar{
    $S \pfunc T$ is a {\it partial-function-order}\nl
    $S \ra T_\bot$ is a one to one correspondence by replacing {\it undefined} by $\bot$\nl
  }
  
  \hi Let $\Fenv:(S \ra T_\bot) \ra (S \pfunc T)$ be a function which converts a (total?) function from $S \ra T_\bot$ to the corresponding partial function, such that $\Fenv(f) = g$ where:\nl

  \ipar{\ipar{
    $g(x)$ is undefined if $f(x) = \bot$\nl
    $g(x) = f(x)$ otherwise\nl
  }}
  
  
  \Claim $f \po_{S\ra T_\bot} g$ iff $\Fenv(f) \po \Fenv(g)$\nl
  
  \Pf $\forall s \in S.\ (f(s) \po_{T_\bot} g(s)) \iff f(s) = g(s) \lor f(s) = \bot$\nl
  \ipar{
    So, either $\Fenv(f(s)) = g(s)$ or $\Fenv(f(s))$ is undefined\nl
  }\nl

  \Prop $[D \ra E]$ is a CPO\nl
  \ipar{
    Let $P \subseteq [D \ra E]$ be {\it directed}\nl
    Define $g:D\ra E$ such that $g(x) = \lub\{\ f(x)\ |\ f\in P\}$\nl
  }
  
  \Claim $g = \lub P$\nl
  
  \Pf We must show that: 
  \ipar{
    (1) $g$ is {\it continuous},\nl
    (2) $\forall f\in P.\ f \po g$, and\nl
    (3) $\forall f'\in ub(P).\ f' \po g$\nl
  }


  \myhline
  ?? I'm not sure where this section fits, my notes might be out of order...\nl

  \Claim If $P$ is {\it directed} then $Q = \{\ f(d)\ |\ f \in P\}$ is {\it directed}\nl

  \Pf Let $f_1, f_2 \in P$ with $f_1(d), f_2(d) \in Q$
  \ipar{
    If $f_1, f_2 \in P$ then that share an UB, say $f_3 \in P$ therefore $f_1(d)$ and $f_2(d)$ have an UB, $f_3(d) \in Q$.\nl

    So, $Q$ is {\it directed} and $g$ (from above?) is defined.\nl
  }\nl

  Let $Q \subseteq D$ be {\it directed}. We want to show that:
  $$g(\lub_{x\in Q} x) = \lub_{x\in Q} g(x)$$
  
  So:
  \begin{equation*}\begin{split}
    g(\lub_{x\in Q} x) &= \lub_{f\in P}\bigl(f(\lub_{x\in Q}x)\bigr) 
    \text{\;\;\;\; by definition of } g\\
    &= \lub_{f\in P}\bigl(\lub_{x\in Q}f(x)\bigr) \text{\;\;\; since } f \text{ is continuous}\\
    &= \lub_{x\in Q}\bigl(\lub_{f\in P}f(x)\bigr) \text{\;\;\; by the Exchange lemma}
  \end{split}\end{equation*}
  \bigskip

  \pagebreak
  {\bf Reminder}:\nl

  \ipar{
    Continuous $\equiv f(\lub X) = \lub_{x\in X} f(x)$\nl
    \ipar{
      - $\l x.x$ is {\it continuous}\nl
      - $D \ra E$, $\{(d,e_0)\ |\ d \in D \}$ is {\it continuous}\nl
      - $E \ra [D \ra E]$ for any $D, E$ is {\it continuous}\nl
    }
  }
  
  \Def $K_{d,e} = \l e.\l d.e$\nl
  
  \ipar{
    If $X \subseteq E$ is {\it directed} then:
    \begin{equation*}\begin{split}
        K(\lub X) &= \lub_{e\in X} K(e) = \lub_{e\in X}(\l d.e)\\
        \lub_{e \in X} K(e)(d) &= \lub_{e\in X}(e) = \lub X\\
        \lub_{e \in X} \l e.\l d.e &= \lub_{e\in X}(e) = \lub X\\
    \end{split}\end{equation*}
  }


  \Def $S(f)(g)(x) = (f(x))(g(x))$
  \ipar{
    $x:D$\nl
    $g:D \ra E$\nl
    $f:D \ra [E \ra F]$\nl
    $S:[[D \ra [E \ra F]] \ra [D \ra E] \ra D] \ra F$\nl
  }\nl

  \Claim $S$ is {\it continuous}\nl
  
  \Pf Homework Excercize $\#$6\nl

  \ipar{
    Must show that if $f\ \&\ g$ are {\it continuous} then $F$ is ({\it continuous\ }?)\nl
    \phantom{===}- Requires three results...\nl
  }
   
  $S: [[[D \impl [D \impl F]] \impl [D \impl E] \impl D] \impl F]$\nl
  $K: [D \impl [D \impl E]]$\nl

  Application:
  \smallskip

  \ipar{
    $\begin{array}[h]{c}
      D \impl E\phantom{=}D\\\hline
      E
    \end{array}$
  }\nl

  These are complete for propositional logic of {\it pure-implication}\nl
  \myhline
  
  \Def Terms
  \ipar{
    $t ::= x\ |\ K\ |\ S\ |\ (t_1\ t_2)$\nl
    $S = \l f.\l g.\l x.((f\ x)(g\ x))$\nl
    $K = \l x.\l y.x$\nl
  }
  
  \newcommand\lcomb{\lceil}
  \newcommand\rcomb{\rceil}
  
  \Claim Any lambda expression is eqivalent to some combinatory term $\lceil e\rceil $\nl
  
  \ipar{
    (1) $\lcomb x\rcomb = x$\nl
    (2) $\lcomb e_1\ e_2\rcomb = (\lcomb e_1\rcomb\ \lcomb e_2\rcomb)$\nl
    (3) $\lcomb \l x.e\rcomb = [x](\lcomb e\rcomb)$\nl
    where $[x]$ is an operator on combinatory terms: ({\it Curry} bracket abstraction)\nl
    \ipar{
      $[x]x = ((S\ K)\ K )\ x$\nl
      $[x]t = (K\ t)$\nl
      $[x](t_1\ t_2) = S([x]t_1)([x]t_2) = \l x.(([x]t_1)([x]t_1)) = \l x.(t_1\ t_2)$\nl
    }
  }

  Conclusion... continuous functions are closed under composition
  
  
\end{document}
