my forest
miscellaneous stuff
+57
-8
+3
-1
trees/dt-001G.tree
+3
-1
trees/dt-001G.tree
···
8
8
\li{ #{(\nat,\leq)}}
9
9
\li{ #{(\nat \cup \Set{\infty}, \leq)}}
10
10
\li{ #{ ([0,1] \subseteq \mathbb{R}, \leq)}}
11
+
\li{ #{ (\op-cl-int{0}{1} \subseteq \mathbb{R}, \leq)}}
11
12
\li{ #{ (\mathbb{Q}, \leq)}}
12
13
\li{ A [flat domain](dt-0008) #{S_\bot} for some set #{S}.}
13
14
}
···
22
23
\li{ #{(\cal{P}(S), \subseteq)} is a [cpo](dt-001D) as the [lub](dt-0017) is just the union. }
23
24
\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
25
\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{ #{ ([0,1] \subseteq \mathbb{R}, \leq)} is a [cpo](dt-001D) with maximum as the [lub](dt-0017).}
27
+
\li{#{ (\op-cl-int{0}{1} \subseteq \mathbb{R}, \leq)} is \em{not} a [cpo](dt-001D), as the set #{\Set{0.9,0.99,0.999,\dots}} has a [lub](dt-0017) of #{1 \notin \op-cl-int{0}{1}}.}
26
28
\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
29
\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
30
}
+25
trees/dt-001Y.tree
+25
trees/dt-001Y.tree
···
1
+
\taxon{Lecture Notes}
2
+
\title{Domain theory}
3
+
\author{liamoc}
4
+
\p{These lecture notes are based on the material I used to teach the [[typesig-dt]] course at the [[uoe]] in 2024.}
5
+
\transclude{dt-0005}
6
+
\subtree{
7
+
\taxon{Lecture}
8
+
\title{Constructions on cpos and PCF}
9
+
\p{todo}
10
+
}
11
+
\subtree{
12
+
\taxon{Lecture}
13
+
\title{Scott Domains}
14
+
\p{todo}
15
+
}
16
+
\subtree{
17
+
\taxon{Lecture}
18
+
\title{Recursively Defined Domains}
19
+
\p{todo}
20
+
}
21
+
\subtree{
22
+
\taxon{Lecture}
23
+
\title{Non-determinism}
24
+
\p{todo}
25
+
}
+4
-1
trees/dt-macros.tree
+4
-1
trees/dt-macros.tree
···
8
8
\def\False{#{\mathit{F}}}
9
9
\def\Set[body]{#{\{\body\}}}
10
10
\def\fixop{#{\textbf{fix}}}
11
-
\def\acr[distance]{\\[\distance]}
11
+
\def\acr[distance]{\\[\distance]}
12
+
\def\lsquare{\startverb[\stopverb}
13
+
\def\rparen{\startverb)\stopverb}
14
+
\def\op-cl-int[x][y]{\lsquare\x,\y\rparen}
+4
trees/index.tree
+4
trees/index.tree
+1
-1
trees/loc-0009.tree
+1
-1
trees/loc-0009.tree
···
2
2
\author{liamoc}
3
3
\p{I am generally available via email, at \code{me@} this domain. I may also be found on Discord (\code{liamoc}), various Zulips (SPLS, Lean, Agda), the [cogent-club slack](https://cogent-club.slack.com/), [bluesky](https://bsky.app/profile/liamoc.net), [the types.pl mastodon instance](https://types.pl/@liamoc), and inexplicably still [twitter](https://twitter.com/kamatsu8). My office is Room N213 in the Skaidrite Darius Building (CSIT) 108 on the [ANU](anu) Campus. The office door is open to the public so feel free to pop over if you want to visit me. To ensure my availability, it may be wise to first contact me via other means to make an appointment.}
4
4
\p{If you are a student or a colleague, please contact me via my [ANU](anu) email (\code{liam.oconnor} at \code{anu.edu.au}), or on the appropriate course forum (e.g. Ed).}
5
-
\p{If you are in posession of my telephone number, please avoid calling unless absolutely necessary.}
5
+
\p{If you are in possession of my telephone number, please avoid calling unless absolutely necessary.}
+4
-3
trees/loc-000E.tree
+4
-3
trees/loc-000E.tree
···
1
-
\date{2025-03-28}
2
-
\tag{news}
3
-
\title{Testing!}
1
+
\import{table-macros}
2
+
\author{liamoc}
3
+
\title{About this website}
4
+
\p{This website is a "forest" created using the [Forester tool](https://www.forester-notes.org), a system of evergreen hypertext notes developed by, among others, [[jonsterling]] and [[kentookura]]. To search my forest, press \kbd{Ctrl}+\kbd{K}.}
+1
-1
trees/news.tree
+1
-1
trees/news.tree
···
36
36
}
37
37
\tr{
38
38
\th{ 24.09.09 }
39
-
\td{Our student [[rayhana]] has published her first paper, [[amjad-vanglabbeek.oconnor-24]] at [EXPRESS/SOS](expresssos24). }
39
+
\td{Our student [[rayhana]] has published her first paper, [[amjad-vanglabbeek-oconnor-2024]] at [EXPRESS/SOS](expresssos24). }
40
40
}
41
41
\tr{
42
42
\th{ 24.07.30 }
+10
trees/people/jonsterling.tree
+10
trees/people/jonsterling.tree
+3
trees/people/kentookura.tree
+3
trees/people/kentookura.tree
+1
-1
trees/people/liamoc.tree
+1
-1
trees/people/liamoc.tree
···
10
10
\p{Lately, my research has been focused on [property-based testing](loc-000A), [semantics](loc-000C) and [temporal logic](loc-000B), but I have very broad research interests. See my [personal bibliography](loc-0001) for a full list of my work.}
11
11
\p{Previously, I lectured courses at [[unsw]], where I did my PhD with [[gckeller]] and the Trustworthy Systems Team lead by [[heiser]], focusing on the [[cogent]] project.}
12
12
13
-
\p{More details about me can be found on my [curriculum vitæ](loc-0004).}
13
+
\p{Full details about me can be found on my [curriculum vitæ](loc-0004), which includes a [list of students](loc-0002). My contact details can be found [here](loc-0009).}