diff --git a/theme b/theme index 1d24633..6bb3ba3 160000 --- a/theme +++ b/theme @@ -1 +1 @@ -Subproject commit 1d24633e5592cb0f85f04a7c9d90f004c980aeec +Subproject commit 6bb3ba3c8fe59ec3700bcce34b234e84da65a9fb diff --git a/trees/dt-001G.tree b/trees/dt-001G.tree index 1b702ca..eedeabe 100644 --- a/trees/dt-001G.tree +++ b/trees/dt-001G.tree @@ -8,6 +8,7 @@ \li{ #{(\nat,\leq)}} \li{ #{(\nat \cup \Set{\infty}, \leq)}} \li{ #{ ([0,1] \subseteq \mathbb{R}, \leq)}} + \li{ #{ (\op-cl-int{0}{1} \subseteq \mathbb{R}, \leq)}} \li{ #{ (\mathbb{Q}, \leq)}} \li{ A [flat domain](dt-0008) #{S_\bot} for some set #{S}.} } @@ -22,7 +23,8 @@ \li{ #{(\cal{P}(S), \subseteq)} is a [cpo](dt-001D) as the [lub](dt-0017) is just the union. } \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).} \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). } -\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.} +\li{ #{ ([0,1] \subseteq \mathbb{R}, \leq)} is a [cpo](dt-001D) with maximum as the [lub](dt-0017).} +\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}}.} \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. } \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). } } diff --git a/trees/dt-001Y.tree b/trees/dt-001Y.tree new file mode 100644 index 0000000..8b5520d --- /dev/null +++ b/trees/dt-001Y.tree @@ -0,0 +1,25 @@ +\taxon{Lecture Notes} +\title{Domain theory} +\author{liamoc} +\p{These lecture notes are based on the material I used to teach the [[typesig-dt]] course at the [[uoe]] in 2024.} +\transclude{dt-0005} +\subtree{ +\taxon{Lecture} +\title{Constructions on cpos and PCF} +\p{todo} +} +\subtree{ +\taxon{Lecture} +\title{Scott Domains} +\p{todo} +} +\subtree{ +\taxon{Lecture} +\title{Recursively Defined Domains} +\p{todo} +} +\subtree{ +\taxon{Lecture} +\title{Non-determinism} +\p{todo} +} \ No newline at end of file diff --git a/trees/dt-macros.tree b/trees/dt-macros.tree index 7e4045e..217c68c 100644 --- a/trees/dt-macros.tree +++ b/trees/dt-macros.tree @@ -8,4 +8,7 @@ \def\False{#{\mathit{F}}} \def\Set[body]{#{\{\body\}}} \def\fixop{#{\textbf{fix}}} -\def\acr[distance]{\\[\distance]} \ No newline at end of file +\def\acr[distance]{\\[\distance]} +\def\lsquare{\startverb[\stopverb} +\def\rparen{\startverb)\stopverb} +\def\op-cl-int[x][y]{\lsquare\x,\y\rparen} \ No newline at end of file diff --git a/trees/index.tree b/trees/index.tree index f6e1d16..26b6dd4 100644 --- a/trees/index.tree +++ b/trees/index.tree @@ -6,5 +6,9 @@ \put\transclude/heading{false} \transclude{liamoc} \put\transclude/heading{true} +\transclude{loc-000E} +\subtree{\title{Lecture notes} +\p{[[dt-001Y]]} +} \transclude{news} } diff --git a/trees/loc-0009.tree b/trees/loc-0009.tree index e280409..eab2ac4 100644 --- a/trees/loc-0009.tree +++ b/trees/loc-0009.tree @@ -2,4 +2,4 @@ \author{liamoc} \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.} \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).} -\p{If you are in posession of my telephone number, please avoid calling unless absolutely necessary.} +\p{If you are in possession of my telephone number, please avoid calling unless absolutely necessary.} diff --git a/trees/loc-000E.tree b/trees/loc-000E.tree index 12077e0..5e45d22 100644 --- a/trees/loc-000E.tree +++ b/trees/loc-000E.tree @@ -1,3 +1,4 @@ -\date{2025-03-28} -\tag{news} -\title{Testing!} +\import{table-macros} +\author{liamoc} +\title{About this website} +\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}.} \ No newline at end of file diff --git a/trees/news.tree b/trees/news.tree index 566d002..96c3f48 100644 --- a/trees/news.tree +++ b/trees/news.tree @@ -36,7 +36,7 @@ } \tr{ \th{ 24.09.09 } - \td{Our student [[rayhana]] has published her first paper, [[amjad-vanglabbeek.oconnor-24]] at [EXPRESS/SOS](expresssos24). } + \td{Our student [[rayhana]] has published her first paper, [[amjad-vanglabbeek-oconnor-2024]] at [EXPRESS/SOS](expresssos24). } } \tr{ \th{ 24.07.30 } diff --git a/trees/people/jonsterling.tree b/trees/people/jonsterling.tree new file mode 100644 index 0000000..9d2d158 --- /dev/null +++ b/trees/people/jonsterling.tree @@ -0,0 +1,10 @@ +\title{Jon Sterling} +\taxon{Person} +\meta{external}{https://www.jonmsterling.com/} +\meta{institution}{[[cam]]} +\meta{orcid}{0000-0002-0585-5564} +\meta{position}{Associate Professor} + + + + diff --git a/trees/people/kentookura.tree b/trees/people/kentookura.tree new file mode 100644 index 0000000..d7b0b1b --- /dev/null +++ b/trees/people/kentookura.tree @@ -0,0 +1,3 @@ +\title{Kento Okura} +\taxon{Person} +\external{https://github.com/kentookura} \ No newline at end of file diff --git a/trees/people/liamoc.tree b/trees/people/liamoc.tree index 4d9221e..9268372 100644 --- a/trees/people/liamoc.tree +++ b/trees/people/liamoc.tree @@ -10,4 +10,4 @@ \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.} \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.} -\p{More details about me can be found on my [curriculum vitæ](loc-0004).} +\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).} diff --git a/trees/table-macros.tree b/trees/table-macros.tree index ea31568..1b890b0 100644 --- a/trees/table-macros.tree +++ b/trees/table-macros.tree @@ -19,3 +19,4 @@ \def\hr{ \{} } +\def\kbd[body]{\{\body}} \ No newline at end of file