my forest
fix #1; also add latest church music corner, fix some dt typos
+25
-4
+1
-1
trees/dt/dt-004D.tree
+1
-1
trees/dt/dt-004D.tree
···
6
6
\p{Scott's original solution to this lack of closure was to use a \em{complete lattice} instead of [cpos](dt-001D), i.e. requiring [lubs](dt-0017) for all subsets, not just [directed](dt-0010) ones. This solves the problem with #{\contto} but introduces new problems:
7
7
\ol{
8
8
\li{ Complete lattices need a \em{top} element #{\top}, but adding a fictitious top (representing inconsistent information) to [cpos](dt-001D) like #{\mathbb{B}_\bot} is strange.}
9
-
\li{ Extending the functions that capture our primitive semantic operationsto complete lattices can spoil nice algebraic properties. Consider these two possible implementations of #{\mathsf{ite}}, the function for the semantics of an #{\syn{if}} expression:
9
+
\li{ Extending the functions that capture our primitive semantic operations to complete lattices can spoil nice algebraic properties. Consider these two possible implementations of #{\mathsf{ite}}, the function for the semantics of an #{\syn{if}} expression:
10
10
##{
11
11
\mathsf{ite}(\top,x,y) = x \sqcup y\quad\quad\quad \quad\quad \mathsf{ite}(\top,x,y) = \top
12
12
}
+2
-2
trees/dt/dt-0067.tree
+2
-2
trees/dt/dt-0067.tree
···
6
6
X \preceq_P Y\quad \text{iff}\quad X \preceq_H Y \land X \preceq_S Y
7
7
}
8
8
This ordering is also called the \em{Egli-Milner} ordering. On a [flat domain](dt-0008), it simplifies to:
9
-
#{A\sqsubseteq B\quad\text{iff}\quad A = B \lor (\bot \in A \land (A \setminus \{\bot\})\subseteq B)}
10
-
Note that this \em{is} antisymmetric in the case of a [flat domain](dt-0008), and the [lub](dt-0017) of a [chain](dt-000V) of sets can be found by taking the union of all elements of the chain if all elements contain #{\bot} If not, then the element without #{\bot} will be the [least upper bound](dt-0017).}
9
+
##{A\sqsubseteq B\quad\text{iff}\quad A = B \lor (\bot \in A \land (A \setminus \{\bot\})\subseteq B)}
10
+
Note that this \em{is} [antisymmetric](dm-0003) in the case of a [flat domain](dt-0008), and the [lub](dt-0017) of a [chain](dt-000V) of sets can be found by taking the union of all elements of the chain if all elements contain #{\bot} If not, then the element without #{\bot} will be the [least upper bound](dt-0017).}
11
11
\p{
12
12
The failures of [antisymmetry](dm-0003) can only be observed in domains of height higher than one. Consider a set #{\Set{x,y}} containing two elements. According to the induced equivalence from this [preorder](dm-000V) #{\approx_P}, this set would be considered equal to the set that contains those two elements \em{plus} any elements that lie between them on the [information ordering](dt-000B): ##{\Set{x,y} \approx_P \Set{ z \mid x \sqsubseteq z \sqsubseteq y }}
13
13
The \em{Plotkin powerdomain} is sometimes called the \em{convex powerdomain}, due to the similarity of this to the geometric definition of convexity. Thus, we use the [ideal completion](dt-0046) trick (as with the [Hoare](dt-0061) and [Smyth](dt-0064) constructions) here to arrive at a definition of powerdomain that distinguishes between all three programs outlined in \ref{dt-0063}.}
+21
trees/loc-000Q.tree
+21
trees/loc-000Q.tree
···
1
+
\import{table-macros}
2
+
\def\percent{\startverb%\stopverb
3
+
}
4
+
\parent{loc-000P}
5
+
\title{4th Sunday after Easter 2025}
6
+
\tag{cmc}
7
+
\date{2025-05-18}
8
+
\author{liamoc}
9
+
\quote{
10
+
Cantáte Dómino cánticum novum, allelúia: quia mirabília fecit Dóminus, allelúia: ante conspéctum géntium revelávit iustítiam suam, allelúia, allelúia.
11
+
}
12
+
\p{This week our choir at [All Saints Ainslie](https://allsaintsainslie.org.au) were without a director, so I filled in as needed. We sang Samuel Wesley's [Lead me, Lord](https://www.youtube.com/watch?v=_cmZTdkjBTY) from his larger work, \em{Praise the Lord, My Soul}.}
13
+
\quote{
14
+
\poem{
15
+
\line{Lead me, Lord. Lead me in thy righteousness,}
16
+
\line{Make thy way plain before my face.}
17
+
\line{For it is thou, Lord; thou, Lord only,}
18
+
\line{That makest me dwell in safety.}
19
+
}
20
+
}
21
+
\p{I also attended Evensong at [St. Paul's Manuka](https://www.stpaulsmanuka.org.au/). Sadly the normal choir wasn't in today, but it was still a restorative service. They used Common Worship, so it was missing some of the collects I like, but they interestingly included a \em{responsórium breve}. The building isn't my favoured sandstone but it's a rather nice brick church. Afterwards I briefly popped into the nearby Catholic [St. Christopher's Cathedral](https://saintchristopher.org.au/) for evening Mass. The building is a little bit less pleasant than its Anglican neighbour, but the service was very well attended. The music was entirely forgettable hymn standards. }