my forest
more dt
+198
-18
+4
trees/dm-000D.tree
+4
trees/dm-000D.tree
+4
trees/dm-000E.tree
+4
trees/dm-000E.tree
+4
trees/dm-000F.tree
+4
trees/dm-000F.tree
+7
-7
trees/dt-0004.tree
+7
-7
trees/dt-0004.tree
···
28
28
and #{\llbracket\cdot\rrbracket_\mathcal{B} : \mathcal{B} \rightarrow \mathbf{B}}:
29
29
##{
30
30
\begin{array}{lcl}
31
-
\llbracket \mathsf{false} \rrbracket_\mathcal{B}\ \sigma & = & F \\
32
-
\llbracket \mathsf{true} \rrbracket_\mathcal{B}\ \sigma & = & T \\
33
-
\llbracket \neg b \rrbracket_\mathcal{B}\ \sigma & = & \begin{cases}F & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = T \\
34
-
T & \text{otherwise}
31
+
\llbracket \mathsf{false} \rrbracket_\mathcal{B}\ \sigma & = & \False \\
32
+
\llbracket \mathsf{true} \rrbracket_\mathcal{B}\ \sigma & = & \True \\
33
+
\llbracket \neg b \rrbracket_\mathcal{B}\ \sigma & = & \begin{cases}\False & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = \True \\
34
+
\True & \text{otherwise}
35
35
\end{cases}
36
36
\\[1.1em]
37
-
\llbracket e_1 = e_2 \rrbracket_\mathcal{B}\ \sigma & = & \begin{cases}T & \text{if}\ \llbracket e_1 \rrbracket_\mathcal{E}\ \sigma = \llbracket e_2 \rrbracket_\mathcal{E}\ \sigma \\
38
-
F & \text{otherwise}
37
+
\llbracket e_1 = e_2 \rrbracket_\mathcal{B}\ \sigma & = & \begin{cases}\True & \text{if}\ \llbracket e_1 \rrbracket_\mathcal{E}\ \sigma = \llbracket e_2 \rrbracket_\mathcal{E}\ \sigma \\
38
+
\False & \text{otherwise}
39
39
\end{cases}
40
40
\end{array}
41
41
}
···
45
45
\llbracket \mathsf{skip} \rrbracket_\mathcal{C}\ \sigma & = & \sigma \\
46
46
\llbracket x := e \rrbracket_\mathcal{C}\ \sigma & = & \sigma\left(x \mapsto \llbracket e \rrbracket_\mathcal{E}\right) \\
47
47
\llbracket c_1 ; c_2 \rrbracket_\mathcal{C}\ \sigma & = & \llbracket c_2 \rrbracket_\mathcal{C}\ \left(\llbracket c_1 \rrbracket_\mathcal{C}\ \sigma\right) \\[0.3em]
48
-
\llbracket \textsf{if}\ b\ \textsf{then}\ c_1\ \textsf{else}\ c_2 \rrbracket_\mathcal{C}\ \sigma & = & \begin{cases}\llbracket c_1 \rrbracket_\mathcal{C}\ \sigma & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = T \\
48
+
\llbracket \textsf{if}\ b\ \textsf{then}\ c_1\ \textsf{else}\ c_2 \rrbracket_\mathcal{C}\ \sigma & = & \begin{cases}\llbracket c_1 \rrbracket_\mathcal{C}\ \sigma & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = \True \\
49
49
\llbracket c_2 \rrbracket_\mathcal{C}\ \sigma & \text{otherwise}
50
50
\end{cases}
51
51
\end{array}
+1
-1
trees/dt-0005.tree
+1
-1
trees/dt-0005.tree
+1
-1
trees/dt-0006.tree
+1
-1
trees/dt-0006.tree
···
8
8
}
9
9
The intuitive way to assign a semantics would be to use a \em{recursive function}:
10
10
##{
11
-
\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ \sigma\; = \; \begin{cases} \llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ (\llbracket c \rrbracket_\mathcal{C}\ \sigma) & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = T \\
11
+
\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ \sigma\; = \; \begin{cases} \llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ (\llbracket c \rrbracket_\mathcal{C}\ \sigma) & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = \True \\
12
12
\sigma & \text{otherwise}
13
13
\end{cases}
14
14
}
+2
-2
trees/dt-000H.tree
+2
-2
trees/dt-000H.tree
···
1
1
\import{dt-macros}
2
-
\title{Monotonic Functions}
2
+
\title{Monotonic functions}
3
3
\author{liamoc}
4
4
\p{If we model our semantic domains for values with [pointed poset](dt-000G)s, then programs are modelled by functions between such [poset](dm-0004)s. But, not all functions are suitable:}
5
5
\transclude{dt-000I}
6
6
\p{It stands to reason that the amount of information we get out of our functions should grow as we increase the amount of information we put into them.
7
-
Such functions are called \em{monotonic} with respect to our information ordering.}
7
+
Such functions are called \em{monotonic} with respect to our [information ordering](dt-000B).}
8
8
\transclude{dt-000J}
9
9
\transclude{dt-000K}
10
10
\scope{
+8
trees/dt-000N.tree
+8
trees/dt-000N.tree
···
2
2
\taxon{Exercise}
3
3
\author{liamoc}
4
4
\p{Consider the functions #{\mathbb{B}_\bot \rightarrow \mathbb{B}_\bot}. Which ones are [monotonic](dt-000J)? There are a total of 27 such functions but only three significant classes.}
5
+
\scope{
6
+
\put\transclude/toc{false}
7
+
\put\transclude/numbered{false}
8
+
\put\transclude/expanded{false}
9
+
\subtree{
10
+
\taxon{Solution}
11
+
\p{The three classes are the nine [strict](dt-000K) functions (which map #{\bot} to #{\bot}), which are all [monotonic](dt-000J), the two non-strict constant functions (which ignore their input and return #{\True} and #{\False} respectively), which are also monotonic, and the 16 non-monotonic functions.}
12
+
}}
+19
trees/dt-000O.tree
+19
trees/dt-000O.tree
···
45
45
}
46
46
\ol{
47
47
\li{ Write down the monotonic functions #{\mathbf{K}_3 \rightarrow \mathbf{K}_3}.}
48
+
\scope{
49
+
\put\transclude/toc{false}
50
+
\put\transclude/numbered{false}
51
+
\put\transclude/expanded{false}
52
+
\subtree{
53
+
\taxon{Solution}
54
+
\p{When drawn as a diagram like the above, the monotonic functions are all those whose lines do not cross.}
55
+
}}
48
56
\li{ Write a simple recursive program to calculate the number of monotonic functions #{\mathbf{K}_n \rightarrow \mathbf{K}_m}.}
57
+
\scope{
58
+
\put\transclude/toc{false}
59
+
\put\transclude/numbered{false}
60
+
\put\transclude/expanded{false}
61
+
\subtree{
62
+
\taxon{Solution}
63
+
\p{In Haskell:}
64
+
\pre{monotonics :: Int -> Int -> Int
65
+
monotonics n 1 = 1
66
+
monotonics n m = sum [monotonics (n-x) (m-1) | x <- [0..n]]}
67
+
}}
49
68
}
+11
trees/dt-000P.tree
+11
trees/dt-000P.tree
···
6
6
\li{ #{\llbracket \mathsf{proc}\ c \rrbracket_\mathcal{E}\ \sigma\ =\ ?}}
7
7
\li{ #{\llbracket x \rrbracket_\mathcal{C}\ \sigma\ =\ ?}}
8
8
}
9
+
\scope{
10
+
\put\transclude/toc{false}
11
+
\put\transclude/numbered{false}
12
+
\put\transclude/expanded{false}
13
+
\subtree{
14
+
\taxon{Solution}
15
+
\ol{
16
+
\li{ #{\llbracket \mathsf{proc}\ c \rrbracket_\mathcal{E}\ \sigma\ =\ \llbracket c \rrbracket_\cal{C}}}
17
+
\li{ #{\llbracket x \rrbracket_\mathcal{C}\ \sigma\ =\ \sigma(x)(\sigma)}}
18
+
}
9
19
}
20
+
}}
+18
-1
trees/dt-000Q.tree
+18
-1
trees/dt-000Q.tree
···
2
2
\taxon{Exercise}
3
3
\author{liamoc}
4
4
\ol{
5
-
\li{Give an example of a [poset](dm-0004) #{A} and a [monotonic](dt-000J) function #{f : A \rightarrow A} such that #{f} \em{doesn't} have a [fixed point](dt-000S).}
5
+
\li{Give an example of a [poset](dm-0004) #{A} and a [monotonic](dt-000J) function #{f : A \rightarrow A} such that #{f} \em{doesn't} have a [fixed point](dt-000S).
6
+
\scope{
7
+
\put\transclude/toc{false}
8
+
\put\transclude/numbered{false}
9
+
\put\transclude/expanded{false}
10
+
\subtree{
11
+
\taxon{Solution}
12
+
\p{In the poset #{(\mathbb{N},\leq)}, the function #{f(x) = x + 1} has no fixed points.}
13
+
}}
14
+
}
6
15
\li{Give an example of a [poset](dm-0004) #{A} and a [monotonic](dt-000J) function #{f : A \rightarrow A} such that #{f} has \em{multiple} [fixed point](dt-000S)s.}
16
+
\scope{
17
+
\put\transclude/toc{false}
18
+
\put\transclude/numbered{false}
19
+
\put\transclude/expanded{false}
20
+
\subtree{
21
+
\taxon{Solution}
22
+
\p{In the poset #{(\mathbb{N},\leq)}, the function #{f(x) = x} has infinitely many fixed points.}
23
+
}}
7
24
}
+2
-2
trees/dt-000R.tree
+2
-2
trees/dt-000R.tree
···
5
5
Consider our recursive \syn{while} loop semantics from \ref{dt-0006}:
6
6
7
7
##{
8
-
\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ \sigma\; = \; \begin{cases} \llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ (\llbracket c \rrbracket_\mathcal{C}\ \sigma) & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = T \\
8
+
\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ \sigma\; = \; \begin{cases} \llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ (\llbracket c \rrbracket_\mathcal{C}\ \sigma) & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = \True \\
9
9
\sigma & \text{otherwise}
10
10
\end{cases}
11
11
}
···
13
13
##{
14
14
\begin{array}{l}
15
15
\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C} = f(\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}) \\[0.5em]
16
-
\qquad \text{where}\; f(X)\ \sigma\; \triangleq \; \begin{cases} X\ (\llbracket c \rrbracket_\mathcal{C}\ \sigma) & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = T \\
16
+
\qquad \text{where}\; f(X)\ \sigma\; \triangleq \; \begin{cases} X\ (\llbracket c \rrbracket_\mathcal{C}\ \sigma) & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = \True \\
17
17
\sigma & \text{otherwise}
18
18
\end{cases}
19
19
\end{array}
+1
trees/dt-000T.tree
+1
trees/dt-000T.tree
+3
-2
trees/dt-000U.tree
+3
-2
trees/dt-000U.tree
+2
-1
trees/dt-000Z.tree
+2
-1
trees/dt-000Z.tree
+1
-1
trees/dt-0013.tree
+1
-1
trees/dt-0013.tree
+3
trees/dt-0015.tree
+3
trees/dt-0015.tree
+9
trees/dt-0016.tree
+9
trees/dt-0016.tree
+11
trees/dt-0017.tree
+11
trees/dt-0017.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\title{Least upper bound}
4
+
\author{liamoc}
5
+
\p{Let #{X \subseteq Y} be a subset of a [poset](dm-0004) #{Y}. An element #{y \in Y} is a \em{least upper bound} (or \em{lub}) for #{X} iff:
6
+
\ol{
7
+
\li{ It is an [upper bound](dm-000C): #{\forall x \in X.\ x \sqsubseteq y}}
8
+
\li{ It is less than any other [upper bound](dm-000C): #{\forall y' \in Y.\ (\forall x \in X. x \sqsubseteq y') \Rightarrow y \sqsubseteq y'}}
9
+
}
10
+
It follows that lubs are unique if they exist. We write the lub of a set #{X} as #{\bigsqcup X}, and usually write #{x \sqcup y} as a shorthand for #{\bigsqcup \Set{x,y}}.
11
+
}
+7
trees/dt-0018.tree
+7
trees/dt-0018.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Corollary}
3
+
\title{Properties of #{\sqcup}}
4
+
\author{liamoc}
5
+
\p{
6
+
When [lubs](dt-0017) exist, the binary #{\sqcup} operator is [idempotent](dm-000D), [commutative](dm-000E), and [associative](dm-000F). Also, we have that #{x \sqsubseteq y} iff #{x \sqcup y = y}.
7
+
}
+6
trees/dt-0019.tree
+6
trees/dt-0019.tree
···
1
+
\taxon{Theorem}
2
+
\title{Pointedness via lubs}
3
+
\author{liamoc}
4
+
\p{
5
+
A [poset](dm-0004) #{Y} is [pointed](dt-000G) iff #{\bigsqcup \emptyset} exists, as the [lub](dt-0017) of an empty set is just the [bottom element](dt-000A) in the [poset](dm-0004), i.e. #{\bigsqcup \emptyset = \bot}.
6
+
}
+2
trees/dt-001A.tree
+2
trees/dt-001A.tree
···
1
+
\title{Information intuition}
2
+
\p{When the [poset](dm-0004) #{Y} from \ref{dt-0017} is ordered by our [information ordering](dt-000B), the intuition of the [lub](dt-0017) #{\bigsqcup X} is that it combines all of the information content of all the elements of #{X} but it does \em{not} add any additional information (hence \em{least}).}
+8
trees/dt-001B.tree
+8
trees/dt-001B.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Example}
3
+
\title{[Lubs](dt-0017) in [the domain #{\bools_\bot \times \bools_\bot}](dt-000F)}
4
+
\ul{
5
+
\li{ #{(\bot, \False) \sqcup (\True,\bot) = (\True,\False)} }
6
+
\li{ #{(\bot, \False) \sqcup (\bot,\bot) = (\bot,\False)} }
7
+
\li{ #{(\bot, \False) \sqcup (\True, \True)} does not exist.}
8
+
}
+11
trees/dt-001C.tree
+11
trees/dt-001C.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Exercise}
3
+
\p{ What is the [lub](dt-0017) operator on subsets #{X \subseteq \nat} of the [poset](dm-0004) #{(\nat,\leq)}?}
4
+
\scope{
5
+
\put\transclude/toc{false}
6
+
\put\transclude/numbered{false}
7
+
\put\transclude/expanded{false}
8
+
\subtree{
9
+
\taxon{Solution}
10
+
\p{The [lub](dt-0017) operator is \em{maximum}.}
11
+
}}
+9
trees/dt-001D.tree
+9
trees/dt-001D.tree
···
1
+
\taxon{Definition}
2
+
\author{liamoc}
3
+
\title{Complete partial order}
4
+
\p{A \em{complete partial order} or \em{cpo} (more specifically a \em{directed complete partial order} or \em{dcpo}) is a [poset](dm-0004) where [lubs](dt-0017) exist for the empty set and for all [directed](dt-0010) subsets. That is, a \em{cpo} is a [poset](dm-0004) #{A} such that:
5
+
\ol{
6
+
\li{#{A} has a [bottom element](dt-000A) #{\bot \in A}, that is the [lub of the empty set](dt-0019), and}
7
+
\li{#{\bigsqcup X} exists for all [directed](dt-0010) #{X \subseteq A}.}
8
+
}
9
+
}
+5
trees/dt-001E.tree
+5
trees/dt-001E.tree
+6
trees/dt-001F.tree
+6
trees/dt-001F.tree
···
1
+
\taxon{Aside}
2
+
\title{Other kinds of completeness}
3
+
\author{liamoc}
4
+
\p{In \ref{dt-001D} we defined cpos in terms of \em{directed completeness}. We may consider \em{chain completeness} instead, where, rather than require [lubs](dt-0017) for every [directed](dt-0010) subset of our [poset](dm-0004) #{A}, we require [lubs](dt-0017) for every [chain](dt-000V) #{X \subseteq A}. We know from \ref{dt-0012} that all [chains](dt-000V) are [directed](dt-0010), so every directed complete cpo is also chain complete. It is also known that every chain complete cpo is also directed complete, so the notions are \strong{equivalent}, although the proof is apparently non-trivial and buried in the literature.}
5
+
\p{If we weaken our completeness requirement to require [lubs](dt-0017) only for the countable [#{\omega}-chains](dt-000W) and not necessarily all chains, we get what is called an \em{#{\omega}-cpo}. All [#{\omega}-chains](dt-000W) are [chains](dt-000V) and are therefore [directed](dt-0010), but not all [chains](dt-000V) are [#{\omega}-chains](dt-000W).}
6
+
\p{Working with just #{\omega}-cpos is common in [denotational semantics](dt-0001) practice, but working with [directed](dt-0010) completeness simplifies some of the properties we will discuss later.}
+30
trees/dt-001G.tree
+30
trees/dt-001G.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\p{For each of the following [posets](dm-0004), determine if it is a [cpo](dt-001D) or not. If it is, describe the [lubs](dt-0017). If it is not, give a [directed](dt-0010) set which has no [lub](dt-0017).}
5
+
\ol{
6
+
\li{ A finite [pointed poset](dt-000G) }
7
+
\li{ #{(\cal{P}(S), \subseteq)} for some set #{S}}
8
+
\li{ #{(\nat,\leq)}}
9
+
\li{ #{(\nat \cup \Set{\infty}, \leq)}}
10
+
\li{ #{ ([0,1] \subseteq \mathbb{R}, \leq)}}
11
+
\li{ #{ (\mathbb{Q}, \leq)}}
12
+
\li{ A [flat domain](dt-0008) #{S_\bot} for some set #{S}.}
13
+
}
14
+
\scope{
15
+
\put\transclude/toc{false}
16
+
\put\transclude/numbered{false}
17
+
\put\transclude/expanded{false}
18
+
\subtree{
19
+
\taxon{Solution}
20
+
\ol{
21
+
\li{ A finite [pointed poset](dt-000G) is a [cpo](dt-001D), as all [directed](dt-0010) subsets will be finite and therefore have a [lub](dt-0017). }
22
+
\li{ #{(\cal{P}(S), \subseteq)} is a [cpo](dt-001D) as the [lub](dt-0017) is just the union. }
23
+
\li{ #{(\nat,\leq)} is \em{not} a [cpo](dt-001D), as the [#{\omega}-chain](dt-000W) #{1 \leq 2 \leq 3 \leq \cdots} has no [lub](dt-0017).}
24
+
\li{ #{(\nat \cup \Set{\infty}, \leq)} is a [cpo](dt-001D), as #{\infty} is the [lub](dt-0017) of any non-repeating [chain](dt-000V). }
25
+
\li{ #{ ([0,1] \subseteq \mathbb{R}, \leq)} is a [cpo](dt-001D) with maximum as the [lub](dt-0017), but the open range (excluding 1) is not.}
26
+
\li{ #{ (\mathbb{Q}, \leq)} is \em{not} a [cpo](dt-001D), and not just because it lacks a [lub](dt-0017) for #{\mathbb{Q}} itself, but also it doesn't contain #{\sqrt{2}}, which can be expressed as the [lub](dt-0017) of an infinite sequence of rational approximations. }
27
+
\li{ A [flat domain](dt-0008) #{S_\bot} for some set #{S} is a [cpo](dt-001D), as the largest [chains](dt-000V) have two elements, and we always pick the non-#{\bot} one as the [lub](dt-0017). }
28
+
}
29
+
}
30
+
}