https://liamoc.net/forest/dt-001Y/index.xml
Liam O'Connor
https://liamoc.net/forest/dt-001Y/
dt-001Y
/forest/dt-001Y/
Domain theory
Lecture Notes
These lecture notes are based on the material I used to teach the Domain Theory (TypeSIG) course at the University of Edinburgh in 2024.
Liam O'Connorhttps://liamoc.net/forest/dt-0005/dt-0005/forest/dt-0005/Semantics and recursionLectureThis lecture is based on material from Graham Hutton, Dana Scott, Joseph Stoy, Carl Gunter, and Glynn Winskel.Liam O'Connorhttps://liamoc.net/forest/dt-0003/dt-0003/forest/dt-0003/Denotational semanticsIn this course we are concerned with programming languages, which, as with natural languages, consist of a syntax and semantics.
The syntax of a language is, for our purposes, merely an inductively-defined tree structure (i.e. abstract syntax).Liam O'Connorhttps://liamoc.net/forest/dt-0000/dt-0000/forest/dt-0000/The Language (without loops)DefinitionUsing notation similar to Backus-Naur Form (BNF):
In the language above, there are three syntactic classes: , , and .Liam O'Connorhttps://liamoc.net/forest/dt-0001/dt-0001/forest/dt-0001/Denotational semanticsDefinitionA denotational semantics consists of, for each syntactic class in a language:
A semantic domain which can be any set of mathematical objects (although, as we will see later, it is helpful if it obeys certain properties).
A valuation function . We require that this function be a homomorphism, that is that it is compositional. This means that the valuation (or denotation) of an expression should be made from the denotation of its components. In other words, for each syntactic constructor , we should have a mathematical operation such that the denotation of can be defined as: Liam O'Connorhttps://liamoc.net/forest/dt-0002/dt-0002/forest/dt-0002/RemarkThe choices of semantic domain and valuation function are, essentially, arbitrary: we choose objects that reflect those aspects of our programs that we are interested in. For most of the simple languages we will examine, we are only concerned with the results of the computation, which is a semantics suitable for reasoning about program behaviour and correctness. However, there also exist denotational cost models that compositionally assign a measure of program performance to syntax. This measure is just another kind of denotational semantics.Liam O'Connorhttps://liamoc.net/forest/dt-0004/dt-0004/forest/dt-0004/Denotational semantics for the language (without loops)Examp
leWe shall first select a semantic domain for each syntactic class:
Here, represents the set of states, which contains the values assigned to all variables:
Now, we define our valuation functions,
:
and :
and :
Liam O'Connorhttps://liamoc.net/forest/dt-000L/dt-000L/forest/dt-000L/RecursionSo far, our semantic domains have just been (functions of) sets. While these have the advantage of being mathematically simple and intuitive, two language features make these sets insufficient for our purposes:
Recursively defined programs, for dealing with recursion and loops, and
Recursively defined semantic domains, for dealing with higher-order programs.Liam O'Connorhttps://liamoc.net/forest/dt-0006/dt-0006/forest/dt-0006/Recursively defined programsSuppose we extended the language with a while loop construct:
The intuitive way to assign a semantics would be to use a recursive function:
However, such an equation is not a good definition. If we consider the trivial infinite loop program , and compute its semantics, we end up with:
This equation is satisfied by any function ,
so it doesn't tell us which function corresponds to the program .More generally, allowing our functions to be (generally) recursive causes these issues. The loop program gives rise to the recursive equation , which has an infinite number of solutions.If we add recursion to our programming language, we could have programs that give rise to more complex recursive equations like . By contrast to , has no solutions (assuming operates on integers).
Liam O'ConnorUpshotWe need an explicit notion of "non-termination" on the semantics level, to properly deal with general recursion (or iteration).
Liam O'Connorhttps://liamoc.net/forest/dt-0007/dt-0007/forest/dt-0007/Recursively defined semantic domainsSuppose we extend our notion of expressions in the language with parameterless higher-order procedures:
Liam O'ConnorUsing higher-order proceduresExampleWe can store procedures in variables, so the program:
has the same effects on the variable as the program:
For our denotational semantics, our domains now take this form ( parts are new vs. Example ), where denotes disjoint union:
Liam O'Connorhttps://liamoc.net/forest/dt-000P/dt-000P/forest/dt-000P/ExerciseGive a semantics to the construct:
Liam O'ConnorSolution
Unfolding the definition of , we end up with a recursive equation for the definition of :
Such equations have no set-theoretic solution, even if we weaken equality to mere set isomorphism (here notated ).Liam O'ConnorA simpler equation with no solutionExampleConsider the recursive equation . Cantor's theorem says that there is no set such that (where is the power set of ), and seeing as it follows that has no solution.Any kind of higher-order construct leads to such recursive domain equations.
Liam O'ConnorUpshot There are no (nontrivial) set-theoretic solutions to the recursive domain equations that arise from higher-order language constructs.
We will return to this problem later on! For now, let's focus on representing non-termination.Liam O'Connorhttps://liamoc.net/forest/dt-0009/dt-0009/forest/dt-0009/Flat domains and information orderingLiam O'Connorhttps://liamoc.net/forest/dt-000A/dt-000A/for
est/dt-000A/The bottom valueFollowing Scott, we introduce a special bottom value to our semantic domains.
Liam O'Connorhttps://liamoc.net/forest/dt-0008/dt-0008/forest/dt-0008/Flat domainDefinitionGiven a set , the flat domain (or lifted set) is just the set (where ).Liam O'Connorhttps://liamoc.net/forest/dt-000B/dt-000B/forest/dt-000B/Information orderingDefinitionAn information ordering is a partial order on denotations, written . This indicates that is approximated by, or carries more information than
, or is more well-defined than .
Naturally, the bottom value, being totally uninformative, is always the least element in this ordering.Liam O'Connorhttps://liamoc.net/forest/dt-000C/dt-000C/forest/dt-000C/Information ordering for flat domainsExampleConsider a flat domain . There is a natural information ordering on :Formally, we say iff .
Liam O'ConnorWarningDon't confuse the information ordering on numbers, i.e. on , with the numerical ordering on . We know , but and are not comparable
in our flat information ordering.
Liam O'Connorhttps://liamoc.net/forest/dt-000D/dt-000D/forest/dt-000D/Combining domainsSome of our semantics may depend on the combination of multiple domains, i.e. semantic functions of multiple arguments. As an example, the semantics of an
statement combines the semantics of the condition and the semantics of each of the two branches. In such scenarios, our domains are no longer flat -- we must generalise to pointed posets.Liam O'Connorhttps://liamoc.net/forest/dt-000G/dt-000G/forest/dt-000G/Pointed posetDefinitionA pointed poset is a partially ordered set with a bottom value.Liam O'Connorhttps://liamoc.net/forest/dt-000E/dt-000E/forest/dt-000E/Product of two pointed posetsConstructionGiven two pointed posets and , the product poset is ordered as follows:
Intuitively, this says that "the information content of a pair of values is increased by increasing the information of either or both of its component values".This product poset is also pointed, with bottom value being .Liam O'Connorhttps://liamoc.net/forest/dt-000F/dt-000F/forest/dt-000F/The domain ExampleAs can be seen above, the domain is not flat, but it is still a pointed poset.Liam O'Connorhttps://liamoc.net/forest/dt-000H/dt-000H/forest/dt-000H/Monotonic functionsIf we model our semantic domains for values with pointed posets, then programs are modelled by functions between such posets. But, not all functions are suitable:Liam O'Connorhttps://liamoc.net/forest/dt-000I/dt-000I/forest/dt-000I/The halting queryExampleThe function seems to let us solve the halting problem, assuming represents non-termination:
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.
Such functions are called monotonic with respect to our information ordering.Liam O'Connorhttps://liamoc.net/forest/dt-000J/dt-000J/forest/dt-000J/MonotonicityDefinitionA function between posets and is monotone (or monotonic) if, for all :
Liam O'Connorhttps://liamoc.net/forest/dt-000K/dt-000K/forest/dt-000K/StrictnessDefinitionA function on pointed posets and is strict if it preserves the bottom va
lue, i.e. .
Liam O'ConnorThesisComputable functions are monotonic (observe that is not).
Liam O'Connorhttps://liamoc.net/forest/dt-000N/dt-000N/forest/dt-000N/ExerciseConsider the functions . Which ones are monotonic? There are a total of 27 such functions but only three significant classes.
Liam O'ConnorSolutionThe three classes are the nine strict functions (which map to ), which are all monotonic, the two non-strict constant functions (which ignore their input and return and respectively), which are also monotonic, and the 16 non-monotonic functions.Liam O'Connorhttps://liamoc.net/forest/dt-000O/dt-000O/forest/dt-000O/ExerciseLet denote the chain of values where implies . There is one monotonic function :,thick] (a) edge[bend left] (b);
\end {tikzpicture}]]>And there are three monotonic functions :,thick] (a) edge (b);
\draw [thick] (b) edge (b1);
\draw [thick] (a) edge (a1);
\draw [->,thick] (a1) edge (b1);
\end {tikzpicture}$\quad $
\begin {tikzpicture}
\node (a) at (0,0) {$\bullet $};
\node (b) at (1,0) {$\bullet $};
\node (a1) at (0,1) {$\bullet $};
\node (b1) at (1,1) {$\bullet $};
\draw [thick] (b) edge (b1);
\draw [->,thick] (a) edge (b);
\draw [thick] (a) edge (a1);
\draw [->,thick] (a1) edge (b);
\end {tikzpicture}$\quad $
\begin {tikzpicture}
\node (a) at (0,0) {$\bullet $};
\node (b) at (1,0) {$\bullet $};
\node (a1) at (0,1) {$\bullet $};
\node (b1) at (1,1) {$\bullet $};
\draw [->,thick] (a) edge (b1);
\draw [thick] (a) edge (a1);
\draw [thick] (b) edge (b1);
\draw [->,thick] (a1) edge (b1);
\end {tikzpicture}
]]>Write down the monotonic functions .
Liam O'ConnorSolutionWhen drawn as a diagram like the above, the monotonic functions are all those whose lines do not cross.
Write a simple recursive program to calculate the number of monotonic functions .
Liam O'ConnorSolutionIn Haskell:monotonics :: Int -> Int -> Int
monotonics n 1 = 1
monotonics n m = sum [monotonics (n-x) (m-1) | x <- [0..n]]Liam O'Connorhttps://liamoc.net/forest/dt-000U/dt-000U/forest/dt-000U/Fixed pointsLiam O'Connorhttps://liamoc.net/forest/dt-000R/dt-000R/forest/dt-000R/From recursion to fixed pointsConsider our recursive loop semantics from SS :
How do we ensure that solutions exist for such recursive equations? And, if multiple solutions exist, how do we decide which one to pick? To address these questions, let's factor out everything in our definition except the recursion into a separate (higher-order) function:
Looking at it this way, we can see that any solution to this equation must be an element of our semantic domain such that . In other words, the problem of finding solutions to our recursive equations can be cast as the problem of finding a fixed point for non-recursive higher-order functions.Liam O'Connorhttps://liamoc.net/forest/dt-000S/dt-000S/forest/dt-000S/Fixed pointDefinitionA value is a fixed point of a function if .Liam O'Connorhttps://liamoc.net/forest/dt-000T/dt-000T/forest/dt-000T/Monotonicity is insufficientLiam O'Co
nnorhttps://liamoc.net/forest/dt-000Q/dt-000Q/forest/dt-000Q/ExerciseGive an example of a poset and a monotonic function such that doesn't have a fixed point.
Liam O'ConnorSolutionIn the poset , the function has no fixed points.
Give an example of a poset and a monotonic function such that has multiple fixed points.
Liam O'ConnorSolutionIn the poset , the function has infinitely many fixed points.
Liam O'ConnorProblemNot all monotonic functions on posets have fixed points, and some have multiple fixed points!So, requiring our functions to be monotonic is insufficient to guarantee that a single "best" solution exists.Liam O'Connorhttps://liamoc.net/forest/dt-000Y/dt-000Y/forest/dt-000Y/Chains and UnfoldingIntuitively, recursive programs are executed by "unfolding" as much as necessary to get a result. We would like to characterise our domains to ensure that solutions always exist, and to allow us to pick the solutions that are "minimal" in the sense that they rely on a minimal amount of unfolding.After converting a recursive program into a n
on-recursive monotonic higher order function , the fixed point we desire would intuitively be the limit of the ascending Kleene chain of , i.e. :https://liamoc.net/forest/dt-000X/dt-000X/forest/dt-000X/Ascending Kleene chain<
fr:taxon>Example Given a pointed poset and a monotonic function , the ascending Kleene chain is the -chain:
Because is the bottom element, we know that . Each subsequent step in the chain exists because of monotonicity.Each successive element of this chain is another "unfolding" of the recursion.Liam O'Connor<
/fr:author>https://liamoc.net/forest/dt-000V/dt-000V/forest/dt-000V/ChainDefinition A chain in a poset is a totally ordered subset of . That is, a subset is a chain iff:
Liam O'Connorhttps://liamoc.net/forest/dt-000W/dt-000W/forest/dt-000W/-chainDefinition An -chain is a chain that is countable. In other words, it is a sequence of elements such that:
Liam O'Connorhttps://liamoc.net/forest/dt-000Z/dt-000Z/forest/dt-000Z/From chains to directed setsWhile -chains are technically sufficient for denotational semantics, for our purposes it is a little more convenient to think in terms of directed sets rather than chains.Liam O'Connorhttps://liamoc.net/forest/dt-0010/dt-0010/forest/dt-0010/Directed setDefinitionFormally, a non-empty subset of a poset is directed iff:
The above is an upper bound of and . Hence, a non-empty set is directed iff every pair of values has an upper bound in the set.Intuitively, directed sets are "going somewhere" -- given two elements we can always find a "greater" one in the set.https://liamoc.net/forest/dt-0011/dt-0011/forest/dt-0011/Power sets are directedExampleThe power set of any set is directed under .Below: :Liam O'Connorhttps://liamoc.net/forest/dt-0012/dt-0012/forest/dt-0012/Chain - DirectedTheoremAll non-empty chains are directed.
Liam O'ConnorProofLet be a chain. Then, given two elements we know from totality that either or . If , then is the upper bound, otherwise is the upper bound.
https://liamoc.net/forest/dt-0013/dt-0013/forest/dt-0013/Consistent subsetDefinition A subset of a poset is consistent iff
Such an is called an upper bound of .
,thick] (foo) edge[bend right] (1.2,0);
\node (a) at (4.2,0) {$\bullet $};
\node (b) at (5.8,0) {$\bullet $};
\node (x) at (4.2,1) {$\bullet $};
\node (y) at (5.8,1) {$\bullet $};
\node (c) at (5,-1) {$\bullet $};
\draw [thick] (c) -- (a) (c) -- (b) (a) -- (x) (a) -- (y) (b) -- (x) (b) -- (y);
\draw [dashed, rounded corners=0.4cm] (3.8,-0.4) rectangle (6.2,0.4);
\node (foo) at (7,-1.2) {a \emph {consistent} set};
\draw [->,thick] (foo) edge[bend right] (6.2,0);
\node (foo) at (2,1) {upper bound};
\draw [->,thick] (foo) edge[bend left] (x);
\draw [->,thick] (foo) edge[bend left] (y);
\end {tikzpicture}
]]>Liam O'Connorhttps://liamoc.net/forest/dt-0014/dt-0014/forest/dt-0014/Alternative characterisation of directednessTheoremA subset of a poset is directed iff every finite subset of has an upper bound in .
Liam O'ConnorProof=: Every pair of elements has an upper bound simply by taking the upper bound of the set
=: Given a finite set , we can show it has an upper bound by an inductive process, first taking the upper bound of and , and then taking the upper bound of that an and so on until we have an upper bound for
the whole set. This induction works because the set is finite.
Liam O'Connorhttps://liamoc.net/forest/dt-0015/dt-0015/forest/dt-0015/CorollaryFrom Theorem we can see that a finite set is directed iff it has a top element , i.e. .Liam O'Connorhttps://liamoc.net/forest/dt-0016/dt-0016/forest/dt-0016/Least upper boundsLiam O'Connorhttps://liamoc.net/forest/dt-0017/dt-0017/forest/dt-0017/Least upper boundDefinitionLet be a subset of a poset . An element is a least upper bound (or lub) for iff:
It is an upper bound:
It is less than any other upper bound:
It follows that lubs are unique if they exist. We write the lub of a set as , and usually write as a shorthand for .Liam O'Connorhttps://liamoc.net/forest/dt-0018/dt-0018/forest/dt-0018/Properties of CorollaryWhen lubs exist, the binary operator is idempotent, commutative, and associative. Also, we have that iff .L
iam O'Connorhttps://liamoc.net/forest/dt-0019/dt-0019/forest/dt-0019/Pointedness via lubsTheoremA poset is pointed iff exists, as the lub of an empty set is just the bottom element in the poset, i.e. .https://liamoc.net/forest/dt-001A/dt-001A/forest/dt-001A/Information intuitionWhen the poset from Definition is ordered by our information ordering, the intuition of the lub is that it combines all of the information content of all the elements of but it does not add any additional information (hence least).https://liamoc.net/forest/dt-001B/dt-001B/forest/dt-001B/Lubs in the domain Example
does not exist.https://liamoc.net/forest/dt-001C/dt-001C/forest/dt-001C/ExerciseWhat is the lub operator on subsets of the poset ?
SolutionThe lub operator is maximum.Liam O'Connorhttps://liamoc.net/forest/dt-001E/dt-001E/forest/dt-001E/Complete partial ordersLiam O'Connorhttps://liamoc.net/forest/dt-001D/dt-001D/forest/dt-001D/Complete partial orderDefinitionA complete partial order or cpo (more specifically a directed complete partial order or dcpo) is a poset where lubs exist for the empty set and for all directed subsets. That is, a cpo is a poset such that:
has a bottom element , that is the lub of the empty set, and
exists for all directed .Liam O'Connorhttps://liamoc.net/forest/dt-001F/dt-001F/forest/dt-001F/Other kinds of completenessAsideIn Definit
ion we defined cpos in terms of directed completeness. We may consider chain completeness instead, where, rather than require lubs for every directed subset of our poset , we require lubs for every chain . We know from Theorem that all chains are directed, 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 equivalent, although the proof is non-trivial, relying on transfinite induction (see these lecture notes for details).If we weaken our completeness requirement to require lubs only for the countable -chains and not necessarily all chains, we get what is called an -cpo. All -chains are chains and are therefore directed, but not all chains are -chains.Working with just -cpos is common in denotational semantics practice, but working with directed completeness simplifies some of the properties we will discuss later.Liam O'Connorhttps://liamoc.net/forest/dt-001G/dt-001G/forest/dt-001G/ExerciseFor each of the following posets, determine if it is a cpo or not. If it is, describe the lubs. If it is not, give a directed set which has no lub.A finite pointed poset
for some set
A flat domain for some set .
Liam O'ConnorSolutionA finite pointed poset is a cpo, as all directed subsets will be finite and therefore have a lub.
is a cpo as the lub is just the union.
is not a cpo, as the -chain has no lub.
is a cpo, as is the lub of any non-repeating chain.
is a cpo with maximum as the lub.
is not a cpo, as the set has a lub of .
is not a cpo, and not just because it lacks a lub for itself, but also it doesn't contain , which can be expressed as the lub of an infinite sequence of rational approximations.
A flat domain for some set is a cpo, as the largest chains have two elements, and we always pick the non- one as the lub.
https://liamoc.net/forest/dt-001H/dt-001H/forest/dt-001H/Lubs of chainsRemarkThe limit of the ascending Kleene chain of a monotonic function is the same as the least upper bound of the set (where is the -fold self-composition of the function ). If we require that our semantic domain is a cpo, we know that this limit exists.
ThesisOur semantic domains are cpos, ensuring the presence of these limits.Liam O'Connorhttps://liamoc.net/forest/dt-001X/dt-001X/forest/dt-001X/ExerciseShow that if and are posets and is directed (by the ordering in Construction ), then the subsets and (defined below) are also directed.
Liam O'ConnorSolutionGiven two elements , we know that there exists such that and . Because is directed, we can conclude that there exists an upper bound where and . As , is an upper bound in for both and and thus is directed. The proof for is analogous.
Give an example of a set such that and are directed, but is not.
Liam O'ConnorSolution is not directed as the two elements are not comparable, but which is directed as .
Show that if and are cpos and is directed, then
Note: Together with this shows that the Cartesian product of two cpos is itself a cpo.
Liam O'ConnorSolutionLet . Because of the ordering in Construction , is certainly a upper bound of the directed set . To show it is the least upper bound, assume for the sake of contradiction that is not the least upper bound of . Then, there must be a such that . But then, would be a lesser upper bound for than , which is supposed to be the lub. Thus there is a contradiction, and must be the lub of .Liam O'Connorhttps://liamoc.net/forest/dt-001I/dt-001I/fore
st/dt-001I/Continuity and Fixed PointsBy choosing a cpo for our semantic domain, we can ensure that the Kleene chain has a limit. However, it is not guaranteed that the limit we find will be a fixed point to our monotonic function .Liam O'Connorhttps://liamoc.net/forest/dt-001K/dt-001K/forest/dt-001K/Monotonicity is insufficientProblemConsider this monotonic function defined over a cpo :
Note this function is not continuous at 0. Starting from our element , we can see that the limit of the ascending Kleene chain is :
But ! -- the lub of the Kleene chain is not a fixed point!To address this problem, we shall strengthen our requirement on functions from mere monotonicity to continuity.Liam O'Connorhttps://liamoc.net/forest/dt-001J/dt-001J/forest/dt-001J/ContinuityDefinitionA function on cpos and is continuous iff for all directed ,
exists, and
, i.e., preserves lubs.
The intuition behind continuity is that "nothing is suddenly invented at infinity": our function will behave analogously at the limit as it does for each element in our chain.Liam O'Connorhttps://liamoc.net/forest/dt-001L/dt-001L/forest/dt-001L/Continuity implies monotonicityTheoremAll continuous functions are monotonic.
Liam O'ConnorProofConsider two elements of a cpo where . Then is directed with a lub of . By the second condition in Definition , we get which is equivalent to .Liam O'Connorhttps://liamoc.net/forest/dt-001M/dt-001M/forest/dt-001M/Monotonic but not continuousExampleConsider this function from , defined by:
This function is monotonic, but, taking (which is a directed subset of the cpo ), then , but . Thus, this function is not continuous.Liam O'Connorhttps://liamoc.net/forest/dt-001N/dt-001N/forest/dt-001N/ExerciseShow that if a function on cpos is monotonic, then exists for any directed (i.e.the first condition for continuity in Definition ).Hint: It suffices to show that is directed.
Liam O'ConnorSolutionBecause is a cpo, it suffices to show that is directed. Let . Let be the values that maps to and respectively, i.e. and . Because is directed, an upper bound of and exists in . Call this upper bound .
Because and , we know that and by monotonicity of . Also, because . Therefore, because two arbitrary elements in have an upper bound within the set, the set is directed.Liam O'Connorhttps://liamoc.net/forest/dt-001O/dt-001O/forest/dt-001O/Alternative characterisation of continuityTheoremA function on cpo
s and is continuous iff:
is monotonic, and
, for all directed
Liam O'ConnorProofThe second condition here is identical to that of Definition . The monotonicity requirement is equivalent to the first condition of Definition , with one direction shown by Theorem , and the other shown by the solution of Exercise .
ThesisComputable functions are continuous functions on cpos.Liam O'Connorhttps://liamoc.net/forest/dt-001W/dt-001W/forest/dt-001W/ExerciseShow that if a function on cpos and is monotonic and is finite, then is continuous.Hint: Finite directed sets contain their lub
Liam O'ConnorSolutionBecause of Theorem , it suffices to show the second condition of continuity, as is monot
onic.Because is finite, any directed subset is also finite, and therefore . Because is monotone, for all .The solution to Exercise shows that is directed and therefore contains its upper bound . Because is monotone, must be (else it would contradict the above).Therefore , as required.https://liamoc.net/forest/dt-001P/dt-001P/forest/dt-001P/The Kleene fixed point theoremTheoremLet be a cpo and be a continuous function. Then the lub of the Kleene chain is the least fixed point of .
ProofWe apply continuity to show that it is a fixed point:
To see that it is the least fixed point: Let be a fixed point of . We know that by definition of . Taking of both sides, we get . We can continue this inductively and thus we know that, for all , . Because is, therefore, an upper bound of the ascending Kleene chain, it must also be at least as large as the lub of that chain.Liam O'Connorhttps://liamoc.net/forest/dt-001Q/dt-001Q/forest/dt-001Q/The operatorDefinitionLet denote the least fixed point of the continuous function , that is , guaranteed to exist by Theorem .Liam O'Connorhttps://liamoc.net/forest/dt-001S/dt-001S/forest/dt-001S/ExerciseWhat is where is the identity function on ?
Liam O'ConnorSolution
What is where is the constant function that always returns ?
Liam O'ConnorSolution
What is where
(where denotes Haskell-style lazy lists of )?
Liam O'ConnorSolution
Here would be the semantics of the recursive definition .Liam O'Connorhttps://liamoc.net/forest/dt-001R/dt-001R/forest/dt-001R/Semantics with fixed pointsLiam O'Connorhttps://liamoc.net/forest/dt-001V/dt-001V/forest/dt-001V/Semantics of loopsArmed with the operator, we can return to our semantics of loops from SS and SS , and at last define their semantics without relying on dubious recursive definitions:
Proof that is continuous is technically required but is omitted here.Liam O'Connorhttps://liamoc.net/forest/dt-001U/dt-001U/forest/dt-001U/Semantics of recursive functionsExampleConsider the function , given by:
Looking at the first few elements of our Kleene chain, we get:
Continuing on, we see that the th approximation to is the function that gives for all up to , and diverges () for all other arguments. Hence the limit is the factorial function on !Liam O'Connorhttps://liamoc.net/forest/dt-001T
/dt-001T/forest/dt-001T/ExerciseWrite down the first few approximations to , where the higher order function is given by:
What is ? What is ?
Liam O'ConnorSolutionThe approximations are . The limit is a function that, given a natural number , produces the infinite list of natural numbers starting from .
Repeat the same process, but this time for a new higher order function given by:
Liam O'ConnorSolutionThe th approximation returns if the input number
is non-negative, even and less than , otherwise it diverges (returns ). The limit returns for any non-negative even number, and diverges otherwise.
Liam O'Connorhttps://liamoc.net/forest/dt-001Z/dt-001Z/forest/dt-001Z/Constructions on cpos and PCFLectureThis lecture is based on material from Graham Hutton, John
Longley, Dana Scott, Joseph Stoy, Carl Gunter, and Glynn Winskel.Liam O'Connorhttps://liamoc.net/forest/dt-002K/dt-002K/forest/dt-002K/ProductsRecall Construction , which showed that the product of two pointed posets is itself a pointed poset.
In Exercise you may also have shown that is also a cpo if and are cpos, with this definition for lubs:
This definition can be made a little more comprehensible by defining it in terms of the two projection operators for pairs:Liam O'Connorhttps://liamoc.net/forest/dt-0020/dt-0020/forest/dt-0020/Projection operators for productsDefinitionDestruction of pairs is captured by the two projection operators, defined as follows:
Liam O'Connorhttps://liamoc.net/forest/dt-0021/dt-0021/forest/dt-0021/Product of cposConstructionGiven cpos and , the product is itself a cpo, ordered by
with bottom value being . Least upper bounds are found by taking the lubs of each component:Liam O'Connorhttps://liamoc.net/forest/dt-0022/dt-0022/forest/dt-0022/Continuity of projection operationsTheoremThe projection functions and are continuous.Liam O'Connorhttps://liamoc.net/forest/dt-0023/dt-0023/forest/dt-0023/The split functionDefinition
Construction of pairs is captured by the split function: If and , then split, written , is defined as:
Liam O'Connorhttps://liamoc.net/forest/dt-0024/dt-0024/forest/dt-0024/Continuity of splitTheoremFor continuous functions and , the split function is continuous.
Liam O'ConnorProofUsing the alternative characterisation of continuity:
is monotonic. Let . Then:
preserves lubs of directed sets. Let be directed. Then:
These building blocks can be used to make many functions on products (thereby ensuring continuity):Liam O'Connorhttps://liamoc.net/forest/dt-0025/dt-0025/forest/dt-0025/The functionDefinition
Liam O'Connorhttps://liamoc.net/forest/dt-0026/dt-0026/forest/dt-0026/Product of functionsDefinitionGiven and , we overload the operator for products to denote the combined function , given below:
Liam O'Connorhttps://liamoc.net/forest/dt-002G/dt-002G/forest/dt-002G/ExerciseExpress the function using just our primitive combinators for projection and split.
Liam O'ConnorSolution
Liam O'Connorhttps://liamoc.net/forest/dt-0027/dt-0027/forest/dt-0027/Pictorial PropertiesThe following properties of our projection and split functions follow from the pictorial reasoning we see on the right:
Liam O'Connorhttps://liamoc.net/forest/dt-0028/dt-0028/forest/dt-0028/ExerciseProve that the three properties in SS are equivalent to the universal property for products
Liam O'ConnorSolutionShowing in both directions:
The three properties follow from the universal property:
The first two properties follow from the universal property where is set to . The third property follows from the universal property where is set to and is set to .
The universal property follows from the universal property:
In the direction of the universal property follows from the third property, and the direction follows from the first two.
Liam O'Connorhttps://liamoc.net/forest/dt-0029/dt-0029/forest/dt-0029/Universal property for cpo productsDefinitionAs commuting diagram on th
e category :Liam O'Connorhttps://liamoc.net/forest/dt-002A/dt-002A/forest/dt-002A/Category theoryAsideLiam O'Connorhttps://liamoc.net/forest/dm-000G/dm-000G/forest/dm-000G/CategoryDefinitionA category consists of a collection of things (objects) and a collection of arrows between these things (morphisms). If there is a morphism and a morphism , we also have the composed morphism . This composition operator must be associative. Additionally each object has an identity morphism , such that for an arrow , .Liam O'Connorhttps://liamoc.net/forest/dm-000H/dm-000H/forest/dm-000H/The category Example The category is the category where the objects are (small) sets, the morphisms are functions between these sets, composition is function composition () and identity is just the identity function .Liam O'Connorhttps://liamoc.net/forest/dm-000I/dm-000I/forest/dm-000I/The category Example The category is the category where the objects are (small) sets, the morphisms are relations between these sets, composition is relational composition: and identity is the diagonal relation (equality).Liam O'Connorhttps://liamoc.net/forest/dt-002B/dt-002B/forest/dt-002B/The category Example The category is the category where the objects are
cpos, the morphisms are continuous functions between these cpos, composition is function composition () and identity is just the identity function .Liam O'Connorhttps:/
/liamoc.net/forest/dm-000J/dm-000J/forest/dm-000J/FunctorDefinitionA functor from a category to a category consists of an object mapping that maps objects of to objects of , and a morphism mapping that maps morphisms of to morphisms of such that:
For each in , we have a morphism in .
For each object in , the equation holds in .
For a pair of morphism in , the equation holds in .Liam O'Connorhttps://liamoc.net/forest/dm-000K/dm-000K/forest/dm-000K/The category Example The category is the category where the objects are themselves (small) categories, the morphisms are structure-preserving maps between these categories, i.e., functors.Liam O'Connorhttps://liamoc.net/forest/dm-000L/dm-000L/forest/dm-000L/Commutative diagramsWhen working in a category, we can state many theorems compactly using commutative diagrams, such as this diagram for products:
In these diagrams, the objects are vertices in the diagram, and the morphisms are the arrows in the diagram (we typically omit identity morphisms and morphisms that are just compositions of other morphisms). Looking at the above diagram, we can equate the two paths from to and the two paths from to , and produce the equations and . We adopt the convention that dotted lines indicate uniqueness, meaning that, from the diagram above, we can also infer the law: Liam O'Connorhttps://liamoc.net/forest/dt-002C/dt-002C/forest/dt-002C/Derived properties of cpo productsCorollaryThe universal property is called such because all the familiar properties of products follow from it - thinking in pictures helps to see how (Indeed, the universal property characterises products up to isomorphism):
These last two statements and show that is a bifunctor on the category , i.e., a functor .Liam O'Connorhttps://liamoc.net/forest/dt-002I/dt-002I/forest/dt-002I/ExerciseShow using the universal property that
Liam O'ConnorSolution
Instantiating the universal property where , , and :
Simplifying using the pictorial properties in SS (shown equivalent to the universal property in Exercise ):
By logical simplifications, we arrive at
as required.
Liam O'Connorhttps://liamoc.net/forest/dt-002D/dt-002D/forest/dt-002D/Isomorphisms for cpo productsLiam O'Connorhttps://liamoc.net/forest/dt-002E/dt-002E/forest/dt-002E/Cpo isomorphismDefinitionAn isomorphism between two cpos and is a bijection between and such that preserves the cpo structure, i.e., that and are continuous.We say two cpos and are isomorphic, written , iff an isomorphism exists between them.Liam O'Connorhttps://liamoc.net/forest/dt-002H/dt-002H/forest/dt-002H/Commutative monoid structure for cposTheoremCpos form a commutative monoid "up to isomorphism" under and (the cpo consisting of only one element ). That is, for all cpos and :
Liam O'ConnorProof
The isomorphisms required are the projection , the function from Exercise , and the swap function.
Liam O'Connorhttps://liamoc.net/forest/dt-002F/dt-002F/forest/dt-002F/The set of continuous functionsDefinitionLet denote just the continuous functions from cpo to cpo :
Liam O'Connorhttps://liamoc.net/forest/dt-002J/dt-002J/forest/dt-002J/TheoremThere is an isomorphism between pairs of continuous functions and continuous functions that output pairs:
Liam O'ConnorProof
Proof follows from the universal property after setting up the isomorphism with functions and .
Liam O'ConnorUpshot Because we have the functor on that satisfies the properties of products described above, the category therefore has binary products.
Liam O'Connorhttps://liamoc.net/forest/dt-002Z/dt-002Z/forest/dt-002Z/FunctionsPreviously, such as in Example , we already implicitly assumed that the set of continuous functions on cpos is itself a cpo. In this section, we will formalise this construction.Liam O'Connorhttps://liamoc.net/forest/dt-002L/dt-002L/forest/dt-002L/The cpo of functionsConstructionIf and
are cpos, the set of continuous functions is a cpo under the pointwise ordering:
The intuition of this ordering in terms of information is that we increase the information content of a function overall by increasing the information content of any (or many) argument values. To prove this, we must show:
has a least element. is the constant function that returns , i.e. .
exists for all directed . Our lub of a set of continuous functions is the function where:
We must show a number of properties of this lub . Specifically:
exists in .
Liam O'ConnorProofWe want to show that the set is directed. Take two values . Since is directed, there exists a function such that and . By applying the definition of for functions above, we have and . Thus is an upper bound of these two values , and thus is directed, and thus its lub exists since is a cpo.
is continuous.
Liam O'ConnorProofUsing the alternative characterisation of continuity
Monotonicity is similar to prove.
is an upper bound for .
Liam O'ConnorProof
Let . Then for any we have . Now, by 2a and lubs, we have , which by the definition of gives . Hence, by the definition of on functions, we can conclude .
is the least upper bound for .
Liam O'ConnorProof Let be an upper bound for . Then (using on functions) is an upper bound for for all . Now, by 2a and lubs, we have , i.e. , which, by the definition of on functions, allows us to conclude .Liam O'Connorhttps://liamoc.net/forest/dt-002M/dt-002M/forest/dt-002M/
The space Example] (b) edge[bend right] (tl)
(tl) edge[loop above] (tl)
(tr) edge[bend right=1.3em] (tl);
\end {tikzpicture}
}
&&
&&
&&
{\begin {tikzpicture}
\draw [rounded corners, thick, fill=white] (-0.8,-0.7) rectangle (0.8,1.39);
\node (tr) at (0.5,0.5) {$\bullet $};
\node (tl) at (-0.5,0.5) {$\bullet $};
\node (b) at (0,-0.5) {$\bullet $};
\draw [thick] (b) -- (tr) (b) -- (tl);
\draw [thick,draw=blue,->] (b) edge[bend right] (tr)
(tl) edge[bend left=1.3em] (tr)
(tr) edge[loop above] (tr);
\end {tikzpicture}
}
\\
{\begin {tikzpicture}
\draw [rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
\node (tr) at (0.5,0.5) {$\bullet $};
\node (tl) at (-0.5,0.5) {$\bullet $};
\node (b) at (0,-0.5) {$\bullet $};
\draw [thick] (b) -- (tr) (b) -- (tl);
\draw [thick,draw=blue,->] (b) edge[loop below] (b)
(tl) edge[loop below] (tl)
(tr) edge[bend right=1.3em] (tl);
\end {tikzpicture}
}\ar [u,ultra thick,-]
&&
{\begin {tikzpicture}
\draw [rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
\node (tr) at (0.5,0.5) {$\bullet $};
\node (tl) at (-0.5,0.5) {$\bullet $};
\node (b) at (0,-0.5) {$\bullet $};
\draw [thick] (b) -- (tr) (b) -- (tl);
\draw [thick,draw=blue] (b) edge[loop below,->] (b)
(tl) edge[loop below,->] (tl)
(tr) edge[loop below] (tr);
\end {tikzpicture}
}
&&
{\begin {tikzpicture}
\draw [rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
\node (tr) at (0.5,0.5) {$\bullet $};
\node (tl) at (-0.5,0.5) {$\bullet $};
\node (b) at (0,-0.5) {$\bullet $};
\draw [thick] (b) -- (tr) (b) -- (tl);
\draw [thick,draw=blue,->] (b) edge[loop below] (b)
(tr) edge[bend left=1.3em] (tl)
(tl) edge[bend left=1.3em] (tr);
\end {tikzpicture}
}
&&
{\begin {tikzpicture}
\draw [rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
\node (tr) at (0.5,0.5) {$\bullet $};
\node (tl) at (-0.5,0.5) {$\bullet $};
\node (b) at (0,-0.5) {$\bullet $};
\draw [thick] (b) -- (tr) (b) -- (tl);
\draw [thick,draw=blue,->] (b) edge[loop below] (b)
(tl) edge[bend left=1.3em] (tr)
(tr) edge[loop below] (tr);
\end {tikzpicture}
}\ar [u,ultra thick,-]
\\
{\begin {tikzpicture}
\draw [rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
\node (tr) at (0.5,0.5) {$\bullet $};
\node (tl) at (-0.5,0.5) {$\bullet $};
\node (b) at (0,-0.5) {$\bullet $};
\draw [thick] (b) -- (tr) (b) -- (tl);
\draw [thick,draw=blue,->] (b) edge[loop below] (b)
(tl) edge[loop right] (tl)
(tr) edge[bend left] (b);
\end {tikzpicture}
}\ar [u,ultra thick,-]\ar [urr,ultra thick,-]
&&
{\begin {tikzpicture}
\draw [rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
\node (tr) at (0.5,0.5) {$\bullet $};
\node (tl) at (-0.5,0.5) {$\bullet $};
\node (b) at (0,-0.5) {$\bullet $};
\draw [thick] (b) -- (tr) (b) -- (tl);
\draw [thick,draw=blue,->] (b) edge[loop below] (b)
(tl) edge[bend right] (b)
(tr) edge[bend right=1.3em] (tl);
\end {tikzpicture}
}\ar [ull,ultra thick,-]\ar [urr,ultra thick,-]
&&
{\begin {tikzpicture}
\draw [rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
\node (tr) at (0.5,0.5) {$\bullet $};
\node (tl) at (-0.5,0.5) {$\bullet $};
\node (b) at (0,-0.5) {$\bullet $};
\draw [thick] (b) -- (tr) (b) -- (tl);
\draw [thick,draw=blue,->] (b) edge[loop below] (b)
(tr) edge[bend left] (b)
(tl) edge[bend left=1.3em] (tr);
\end {tikzpicture}
}\ar [u,ultra thick,-]\ar [urr,ultra thick,-]
&&
{\begin {tikzpicture}
\draw [rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
\node (tr) at (0.5,0.5) {$\bullet $};
\node (tl) at (-0.5,0.5) {$\bullet $};
\node (b) at (0,-0.5) {$\bullet $};
\draw [thick] (b) -- (tr) (b) -- (tl);
\draw [thick,draw=blue,->] (b) edge[loop below] (b)
(tl) edge[bend right] (b)
(tr) edge[loop left] (tr);
\end {tikzpicture}
}\ar [u,ultra thick,-]\ar [ullll,ultra thick,-]
\\
&\qquad &&{\begin {tikzpicture}
\draw [rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
\node (tr) at (0.5,0.5) {$\bullet $};
\node (tl) at (-0.5,0.5) {$\bullet $};
\node (b) at (0,-0.5) {$\bullet $};
\draw [thick] (b) -- (tr) (b) -- (tl);
\draw [thick,draw=blue,->] (b) edge[loop below] (b)
(tl) edge[bend right] (b)
(tr) edge[bend left] (b);
\end {tikzpicture}
}\ar [ul, ultra thick,-] \ar [ur, ultra thick,-] \ar [ulll, ultra thick,-] \ar [urrr, ultra thick,-] &&\qquad
\end {tikzcd}
]]>
At each step "upwards" on this cpo, one arrow that ends in now points to a non- value (moving up the cpo ).Liam O'Connorhttps://liamoc.net/forest/dt-002P/dt-002P/forest/dt-002P/Primitive functions for functionsLiam O'Connorhttps://liamoc.net/forest/dt-002N/dt-002N/forest/dt-002N/The functionDefinitionThe function simply applies a given function to a given argument:
Liam O'Connorhttps://liamoc.net/forest/dt-002Q/dt-002Q/forest/dt-002Q/ExerciseShow that is continuous.Hint: A function is continuous iff it is continuous in each argument separately, i.e., iff is continuous, and is continuous.
Liam O'ConnorSolution
First showing is continuous for some continuous , using the alternative characterisation
is monotonic: Given where , we can see that by the monotonicity of .
preserves lubs: Given a directed , we can see that follows from the continuity of .
Next, showing is continuous for some fixed :
is monotonic: Given where , we can see that by the pointwise ordering of functions.
preserves lubs: Given a directed , we can see that follows from the lub definition for functions.Liam O'Connorhttps://liamoc.net/forest/dt-002O/dt-002O/forest/dt-002O/The functionDefinitionThe function transforms a function that takes two arguments all at once (as a product) into a function that takes the arguments one at a time. That is, if then:
Liam O'Connorhttps://liamoc.net/forest/dt-002S/dt-002S/forest/dt-002S/Continuity of Theorem is continuous on .
, given continuous , is continuous on .
, given continuous and , is continuous on .Liam O'Connorhttps://liamoc.net/forest/dt-002R/dt-002R/forest/dt-002R/Exercise What is the common (functional programming) name for ?
Liam O'ConnorSolutionLiam O'Connorhttps://liamoc.net/forest/dt-002T/dt-002T/forest/dt-002T/Universal property for functionsDefinitionLiam O'Connorhttps://liamoc.net/forest/dt-002U/dt-002U/forest/dt-002U/The currying isomorphismTheorem
Liam O'ConnorProof
Follows from the universal property for functions when set up with the isomorphism from curry and its inverse, the function in Exercise .
Liam O'Connorhttps://liamoc.net/forest/dt-002V/dt-002V/forest/dt-002V/Why the function arrow is not a covariant bifunctorRemark For the operator on cpos (Definition ) to be the object mapping for a bifunctor like is (see Corollary ), we would need to define a morphism mapping that, given two functions and , gives a function . But such a function is not implementable:
In the above hole , and . Given the value , none of our functions or take elements of , so there would be no way to produce the value required. This is because our function goes the wrong way. If were a function , things would be a lot easier.Liam O'Connorhttps://liamoc.net/forest/dm-000Q/dm-000Q/forest/dm-000Q/Dual categoryDefinitionThe dual of a category , written , is a category with the same objects as but the arrows are reversed, that is, for each morphism in , there is a morphism in .Liam O'Connorhttps://liamoc.net/forest/dt-002W/dt-002W/forest/dt-002W/The function arrow is a bifunctorThe operator introduced in Definition is is the object mapping for a binary functor: The category is the dual category to .Thus, a morphism in the category is a continuous function . Thus, the morphism mapping for our functor must take two functions (the morphism from ) and (the morphism from ), and produce . As with products, we will overload the notation for this mapping as well.Liam O'Connorhttps://liamoc.net/forest/dt-002X/dt-002X/forest/dt-002X/Morphism mapping for DefinitionGiven and , we have:
Liam O'Connorhttps://liamoc.net/forest/dt-002Y/dt-002Y/forest/dt-002Y/TheoremThe two functor laws follow as a consequence of the universal property for functions:
Liam O'ConnorUpshotOur category has exponentials.Liam O'Connorhttps://liamoc.net/forest/dt-0030/dt-0030/forest/dt-0030/SumsLiam O'Connorhttps://liamoc.net/forest/dt-0031/dt-0031/forest/dt-0031/Sum of cposConstructionThe sum construct on cpo denotes a disjoin
t union of two cpos with a new, dedicated value:
This construct is a cpo under the ordering:
Intuitively, this says that the ordering on is the same as and separately, except that is less than anything.The only directed sets are those that do not contain a mixture of elements from both and from , so the least upper bound operator is essentially the sa
me as the least upper bounds for and for . Formally:
Liam O'Connorhttps://liamoc.net/forest/dt-003D/dt-003D/forest/dt-003D/Primitive functions for sumsLiam O'Connorhttps://liamoc.net/forest/dt-0032/dt-0032/forest/dt-0032/Constructors for sumsDefinitionFor constructing sums, we use two primitive constructor functions, and :
Liam O'Connorhttps://liamoc.net/forest/dt-0033/dt-0033/forest/dt-0033/Continuity of sum constructorsTheoremThe constructor functions and are continuous.Liam O'Connorhttps://liamoc.net/forest/dt-0034/dt-0034/forest/dt-0034/The case functionDefinitionElimination of sums is captured by the case function , made from functions and . This
function is defined by:
Liam O'Connorhttps://liamoc.net/forest/dt-0035/dt-0035/forest/dt-0035/Exercise Prove that the case function is, given continuous functions and , continuous on its argument .
Liam O'ConnorSolution
As mentioned in Construction , the only directed subsets of are those that contain entirely values of the format and optionally , or those that contain entirely values of the format and optionally . Call this directed
subset .
When : This means that as is always the least element. From Definition , we have: This discharges both requirements in Definition for this case.
When : This means that consists of at least one value plus possibly , that is for some nonempty . We have the following, using the continuity of :
When : Similar to the case but using rather than .
Liam O'Connorhttps://liamoc.net/forest/dt-0039/dt-0039/forest/dt-0039/Locality of sumsWe can see by the definitions of case and our constructors that and , or, in a commutative diagram:Note that this diagram is like the dual of the diagram seen in the universal property for products -- the arrows are reversed. That is because, generally speaking, sums are dual to products. However, because of our additional value, our cpo sums are only weakly universal -- the arrow is not unique.Liam O'Connorhttps://liamoc.net/forest/dt-003A/dt-003A/forest/dt-003A/Weak universality of cpo sumsExampleConsider this scenario with the cpos and :
In this case, setting the function makes the diagram commute, but due to the different handling of .Liam O'Connorhttps://liamoc.net/forest/dt-003B/dt-003B/forest/dt-003B/Weak universal property for cpo sumsDefi
nitionThis property is called weak because it uses only the information ordering rather than equality on the right hand side.Liam O'Connorhttps://liamoc.net/forest/dt-003C/dt-003C/forest/dt-003C/Failure of sum isomorphismsWarningThe weakness of the universal property for sums means that many common isomorphisms for sums in other contexts do not hold:
Liam O'Connorhttps://liamoc.net/forest/dt-0036/dt-0036/forest/dt-0036/Sums form a bifunctorWith these, we can define the morphism mapping for the sum bifunctor . Just as with products and functions, we will overload the notation for morphisms as well as objects in the category .Liam O'Connorhttps://liamoc.net/forest/dt-0037/dt-0037/forest/dt-0037/Sum of functionsDefinitionGiven functions and , we have: Liam O'Connorhttps://liamoc.net/fores
t/dt-0038/dt-0038/forest/dt-0038/Theorem is a lawful bifunctor, that is:
Liam O'ConnorUpshot
Our category has only local sums.
Liam O'Connorhttps://liamoc.net/forest/dt-003E/dt-003E/forest/dt-003E/Strict ConstructionsWhen giving a semantics to a call-by-name (or "lazy") language, the constructions for functions, for products and for sums are exactly what we want. To properly capture call-by-value (or "strict") languages, however, we also need strict versions of these constructions.Liam O'Connorhttps://liamoc.net/forest/dt-003F/dt-003F/forest/dt-003F/The cpo of strict continuous functionsConstructionThe ordering and lubs are, mutatis mutandis, as with the non-str
ict Construction .Liam O'Connorhttps://liamoc.net/forest/dt-003G/dt-003G/forest/dt-003G/Smash products of cposConstructionThe ordering and lubs are, mutatis mutandis, as with the non-strict Construction . This operator is called a smash product because the two values from and are "smashed" into one value.Liam O'Connorhttps://liamoc.net/forest/dt-003H/dt-003H/forest/dt-003H/Smash sums of cposConstructionThe ordering and lubs are, mutatis mutandis, as with the non-strict Construction . This operator is called a smash sum because the two values from and are "smashed" into one value.Liam O'Connorhttps://liamoc.net/forest/dt-003J/dt-003J/forest/dt-003J/Isomorphisms with strict constructionsTheoremThe strict cpo constructions satisfy all the usual isomorphisms, including:
Liam O'Connorhttps://liamoc.net/forest/dt-003I/dt-003I/forest/dt-003I/The category Definition The category is the category where the objects are cpos, the morphisms are strict continuous functions between these cpos, and composition and identity are as in .
Liam O'ConnorUpshot
The category has products, exponentials, and sums (as it doesn't suffer from the problem that does).
Liam O'Connorhttps://liamoc.net/forest/dt-003K/dt-003K/forest/dt-003K/The lifting operator for cposDefinition The lifting operator adds a new value to a cpo. That is, for a cpo :
For all (including ), our new bottom value .Liam O'Connorhttps://liamoc.net/forest/dt-003L/dt-003L/forest/dt-003L/Isomorphisms with liftingTheoremWith the lifting operator, we can relate the lazy constructions like product and sum with strict constructions like smash product and sum via isomorphism:
Liam O'Connorhttps://liamoc.net/forest/dt-003T/dt-003T/forest/dt-003T/PCFFor most purposes in semantics, describing semantics in terms of (continuous functions on) cpos is enough. To demonstrate, we will give semantics to PCF: a Turing-complete, higher order functional programming language. We will then extend PCF to include more features, namely pairs (product types) and sum types.Liam O'Connorhttps://liamoc.net/forest/dt-003M/dt-003M/forest/dt-003M/The language PCFDefinitionThe language for Programming Computable Functions (PCF) is a
variant of typed -calculus with minimal extensions to be Turing-complete.
Liam O'Connorhttps://liamoc.net/forest/dt-003N/dt-003N/forest/dt-003N/Typing rules for PCFDefinitionLiam O'Connorhttps://liamoc.net/forest/dt-003O/dt-003O/forest/dt-003O/Type-dependent denotationsBecause PCF is typed, we shall assign denotations only to well-typed expressions.
The range of our denotation function for expressions is determined by the type of its input expression. That is, the denotation of a type is the cpo whose elements will be the denotations of expressions of type .
The denotation of the type , then, is merely the flat domain of the natural numbers :
And, the denotation of the function type is the domain of continuous functions on cpos:
A closed term with no free variables denotes an element of , so we might be tempted to define our denotation function for expressions like so:
However, if involves free variables from our context , the valuation of will depend on the values assigned to all the variables. Thus, the denotation of a typed expression is defined instead as a continuous function:
where the meaning of a context will be a a big -tuple of the values assigned to each variable:
Liam O'Connorhttps://liamoc.net/forest/dt-003Q/dt-003Q/forest/dt-003Q/Notation for -tuplesDefinitionGiven an -tuple, i.e. elements of the -ary product , we typically denote the entire -tuple as in vector notation:
And individual elements of the tuple are accessed with numeric subscripts:
Liam O'Connorhttps://liamoc.net/forest/dt-003P/dt-003P/forest/dt-003P/Semantics of PCFDefinition
Liam O'ConnorTypes
Liam O'ConnorExpressions
For , we have defined as follows:
0 \\
\llbracket e_3 \rrbracket _\Gamma (\vec {z}) & \text {if}\ \llbracket e_1 \rrbracket _\Gamma (\vec {z}) = 0 \\
\bot & \text {if}\ \llbracket e_1 \rrbracket _\Gamma (\vec {z}) = \bot
\end {cases}\\
\llbracket \mathsf {fix}\ x : \tau .\ e \rrbracket _\Gamma (\vec {z}) &= & \mathbf {fix}(\boldsymbol {\lambda } v \in \llbracket \tau \rrbracket .\ \llbracket e\rrbracket _{\Gamma , x : \tau }(\vec {z}, v))
\end {array}
]]>
In the above definitions a boldface lambda is used for an anonymous continuous function -- boldface to distinguish it from the lambda in the syntax of PCF. Verifying that these functions are indeed continuous is straightforward, but is necessary to justify the use of the operator.
Liam O'Connorhttps://liamoc.net/forest/dt-003R/dt-003R/forest/dt-003R/Extending PCF with product typesWe shall extend the syntax of PCF with a new type former, and three expression-level constructs for constr
ucting and deconstructing pairs:
Adding to our typing rules similarly:
To extend our semantics, we make the product type denote the product cpo , and our expression semantics are expressed straightforwardly using our projection and split operations for products:
Liam O'Connorhttps://liamoc.net/forest/dt-003S/dt-003S/forest/dt-003S/Extending PCF with sum typesWe shall extend the syntax of PCF with a new type former, and three expression-level constructs for constructing and deconstr
ucting sums:
Adding to our typing rules similarly:
To extend our semantics, we make the sum type denote the sum cpo , and our expression semantics are expressed using our primitive functions for sums.
Liam O'Connorhttps://liamoc.net/forest/dt-004Z/dt-004Z/forest/dt-004Z/Recursively defined domains and -calculusLectureThis lecture is based on material from Graham Hutton, John Longley, Dana Scott, Joseph Stoy, Carl Gunter, and Glynn Winskel.Liam O'Connorhttps://liamoc.net/forest/dt-004J/dt-004J/forest/dt-004J/Why we need
recursively defined domainsWe saw recursive domain equations with higher-order procedures in SS , but there are numerous other examples where they come up.Liam O'Connorhttps://liamoc.net/forest/dt-004L/dt-004L/forest/dt-004L/Recursive algebraic data typesSuppose we have a language with recursive data types,
such as this type in Haskell-style syntax:
As in PCF, the denotation of a type is the domain which contains all the denotations of all closed expressions of type . What, then, is the domain that corresponds to ? We need a cpo that satisfies the below equation (where is the cpo containing just one element ):
Liam O'Connorhttps://liamoc.net/forest/dt-004M/dt-004M/forest/dt-004M/Untyped higher-order languages If we take PCF, discard the type system, , natural number primitives and any other superfluous features, and
just boil our language down to a minimal, Turing-complete subset, we end up with the untyped -calculus -- a language consisting only of untyped functions.Liam O'Connorhttps://liamoc.net/forest/dt-004K/dt-004K/forest/dt-004K/Untyped -calculusDefinition Untyped -calculus consists o
nly of untyped (higher-order) functions:
Trying to give a semantics to the untyped calculus poses an issue: we can no longer rely on the type of an expression to select an appropriate semantic domain. Instead, we we must pick a single domain which, since functions can be applied to themselves, must apparently include the set of functions :
How can we find solutions to such recursive equations? How can we guarantee the existence of a (least) solution?We can start by generalising the fixed point approach we used for values (i.e. elements of cpos) to domains (i.e. cpos themselves).Liam O'Connorhttps://liamoc.net/forest/dt-004N/dt-004N/forest/dt-004N/Recursive domain equations as endofunctorsExampleThis recursive equation for lists:
Can be expressed as the least fixed point of this mapping (specifically an endofunctor) on cpos:
To ensure that least fixed points exist, and to give us a means of finding them, we must now generalise all of the concepts we used for least fixed points on values (information ordering, least upper bounds, continuity etc.) to domains themselves.Liam O'Connor
https://liamoc.net/forest/dt-004O/dt-004O/forest/dt-004O/From a cpo to the category
Liam O'ConnorProblem
The following definitions are insufficient when using function constructions in our domain equations ( and ), but it will suffice for our purposes for now.
Let us say (for now) that a cpo approximates a cpo (i.e. ) iff there is a continuous function . Then, there is a least element for this ordering: the one-element
cpo , as the continuous function exists for any cpo .
Liam O'ConnorInitialityCategorical AsideThe category has no initial object. The cpo is terminal; but also serves as a "pseudo" initial object due to the above.
Liam O'Connorhttps://liamoc.net/forest/dt-004P/dt-004P/forest/dt-004P/Colimits in the category Liam O'Connorhttps://liamoc.net/forest/dt-004Q/dt-004Q/forest/dt-004Q/-chains of cpos in the category DefinitionAn -chain of cpos in the category consists of a family of cpos , together with a family of continuous functions , shown below:https://liamoc.net/forest/dt-004R/dt-004R/forest/dt-004R/Upper bounds in the category DefinitionA cpo is an upper bound of an -chain of cpos in the category if there is a family of continuous functions such that the following diagram commutes (i.e. for all ):Liam O'Connorhttps://liamoc.net/forest/dt-004S/dt-004S/forest/dt-004S/Least upper bounds in the category DefinitionA cpo is the least upper bound of an -chain of cpos if is both an upper bound and if there exists a unique for any other upper bound such that the following diagram commutes (i.e. for all ):The least upper bound of such an -chain is also called its colimit.Note: Uniqueness of lubs is up to isomorphism. That is, if and are both colimits of our -chain, then .Liam O'Connorhttps://liamoc.net/forest/dt-004T/dt-004T/forest/dt-004T/Endofunctors on DefinitionAn endofunctor on the category is a functor , i.e. a mapping on cpos together with a mapping on continuous functions, such that:If then
Liam O'Connorhttps://liamoc.net/forest/dt-004U/dt-004U/forest/dt-004U/RemarkObserve that, given the information ordering for cpos where if there exists a continuous function , the functor laws necessarily imply monotonicity for all endofunctors .https://liamoc.net/forest/dt-004V/dt-004V/forest/dt-004V/Cocontinuous endofunctorsDefinitionAn endofunctor is cocontinuous iff it preserves colimits of -chains of cpos. That is, given a chain where is a colimit:
Then is a colimit for the following chain:
] \ar [uurrr,"\mathcal {F}(g_0)"near start] & \mathcal {F}(A_1) \ar [r,thick,"\mathcal {F}(f_1)"',->]\ar [uurr,"\mathcal {F}(g_1)"near start] & \mathcal {F}(A_2) \ar [r,thick,"\mathcal {F}(f_2)"',->] \ar [uur,"\mathcal {F}(g_2)"near start] & \mathcal {F}(A_3) \ar [uu,"\mathcal {F}(g_3)"near start] \ar [r,thick,-,dotted] & \quad
\end {tikzcd}
]]>Liam O'Connorhttps://liamoc.net/forest/dt-004W/dt-004W/forest/dt-004W/Fixed points of endofunctors on DefinitionA fixed point of an endofunctor on cpos is a cpo such that .
Liam O'ConnorNoteIn Scott's approach, which we follow here, our fixed points are up to isomorphism (suitable for languages with isorecursive types), but there are other approaches where they are equalities (suitable for languages with equirecursive types).Liam
O'Connorhttps://liamoc.net/forest/dt-004X/dt-004X/forest/dt-004X/Fixed point theorem for endofunctors on TheoremEvery cocontinuous endofunctor on cpos has a least fixed point, giv
en by the colimit of the -chain:Liam O'Connorhttps://liamoc.net/forest/dt-004Y/dt-004Y/forest/dt-004Y/Binary NumbersExampleConsider the Haskell-style data type:
So, e.g. .The recursive domain equation is, expressed as a fixed point:
We wish to show that is a cocontinuous endofunctor.We have a mapping on cpos (objects of the category ), but for it to be a functor we additionally need a mapping on continuous functions (morphisms of the category ).Recalling our sum construction, we may remember that sums are already a bifunctor (Theorem ). Thus, our mapping on continuous functions can be derived from our mapping on cpos by using the morphism mapping from the sum construction (Definition ). Given a continuous function ,
our morphism mapping is:Proof that this endofunctor is cocontinuous is left for the reader. Hence the semantics of the type , i.e. is the least fixed point of , i.e. the colimit of the -chain:Let us visualise this chain. Here the sum injections have been written as rather than (combinations of) and to keep the connection with the Haskell data type clear.,ultra thick,dotted] (6,1.5) -- (10.5,1.5);
\draw [fill=white!95!black, rounded corners=2em] (6,-1) -- (10,3.5) -- (2,3.5) -- cycle;
\draw [fill=white!97!black, rounded corners=2em,dashed] (6,-0.8) -- (8.1,1.5) -- (3.9,1.5) -- cycle;
\draw [->,ultra thick] (2,0.5) -- (4.8,0.5);
\draw [fill=white!97!black, rounded corners=2em] (2,-0.8) -- (3.8,1.5) -- (0.2,1.5) -- cycle;
\node [draw, fill=white, dashed, rounded corners] (b2) at (2,0) {$\bot $};
\draw [->,ultra thick] (b1) -- (b2);
\node (a1) at (1.2,1) {$\mathsf {Z}(\bot )$};
\node (a2) at (2,1.04) {$\mathsf {E}$};
\node (a3) at (2.8,1) {$\mathsf {O}(\bot )$};
\draw [-] (b2) -- (a2);
\draw [-] (b2) -- (a3);
\draw [-] (b2) -- (a1);
\node (b2) at (6,0) {$\bot $};
\node (a1) at (5,1) {$\mathsf {Z}(\bot )$};
\node (a2) at (6,1.04) {$\mathsf {E}$};
\node (a3) at (7,1) {$\mathsf {O}(\bot )$};
\draw [-] (b2) -- (a2);
\draw [-] (b2) -- (a3);
\draw [-] (b2) -- (a1);
\node (c1) at (3.3,3) {\footnotesize $\mathsf {Z}(\mathsf {Z}(\bot ))$};
\node (c2) at (4.3,3) {\footnotesize $\mathsf {Z}(\mathsf {E})$};
\node (c3) at (5.3,3) {\footnotesize $\mathsf {Z}(\mathsf {O}(\bot ))$};
\draw [-] (a1) -- (c2);
\draw [-] (a1) -- (c3);
\draw [-] (a1) -- (c1);
\node (c1) at (6.7,3) {\footnotesize $\mathsf {O}(\mathsf {Z}(\bot ))$};
\node (c2) at (7.7,3) {\footnotesize $\mathsf {O}(\mathsf {E})$};
\node (c3) at (8.7,3) {\footnotesize $\mathsf {O}(\mathsf {O}(\bot ))$}; \draw [-] (a3) -- (c2);
\draw [-] (a3) -- (c3);
\draw [-] (a3) -- (c1);
\end {tikzpicture}
]]>Thus, the th cpo in the chain contains binary numbers with at most defined digits. The colimit of the chain contains all binary numbers (finite, partial, and infinite!).Liam O'Connorhttps://liamoc.net/forest/dt-005M/dt-005M/forest/dt-005M/ExerciseShow that and (using our operator for functions) define an endofunctor , i.e. that they satisfy the functor laws.
Liam O'ConnorSolution
We must show .
We must show .
Liam O'Connorhttps://liamoc.net/forest/dt-0050/dt-0050/forest/dt-0050/Constructing endofunctorsIf we have a mapping on cpos that is made up of the primitives , , , , and , we can generate a corresponding morphism mapping on continuous functions by using the corresponding morphism mappings of each of these operators. Thus any such mapping can be turned into an endofunctor.Liam O'Connorhttps://liamoc.net/forest/dt-0051/dt-0051/forest/dt-0051/Making endofunctors for algebraic data typesExampleLiam O'Connorhttps://liamoc.net/forest/dt-005N/dt-005N/forest/dt-005N/ExerciseThe lazy natural numbers, also called conats, are defined as the least solution to the equation .
Sketch the first four approximations to the least fixed point. Call the two sum injections and .
Liam O'ConnorSolution
Repeat this exercise assuming:
is strict (i.e. )
Liam O'ConnorSolution
is strict (i.e. )
Liam O'ConnorSolution
Liam O'Connorhttps://liamoc.net/forest/dt-0052/dt-0052/forest/dt-0052/From to Liam O'Connorhttps://liamoc.n
et/forest/dt-0053/dt-0053/forest/dt-0053/Contravariance in the function arrowProblemWe cannot get morphism mappings in the category as easily as SS when our object mapping makes use of the function operators and , as
they are contravariant in their first argument. This means the functor that they extend to is not but , where is the dual category of . The morphisms end up the wrong way around.As an example, consider . Then, recalling the morphism mapping of the functor:
We can generate a morphism mapping for :
However, this mapping has the wrong type. For , then , which is , not the required . This is because the generated functor is contravariant, not covariant.Liam O'Connorhttps://liamoc.net/forest/dt-005O/dt-005O/forest/dt-005O/ExerciseShow that, in contrast to from Problem , the mapping can be extended to continuous functions g
iving a covariant endofunctor on .
Liam O'ConnorSolution
Given a continuous function , we must produce a continuous function , defined as follows:
Composition of continuous functions preserves continuity. The functor laws can be shown straightforwardly.
Liam O'Connorhttps://liamoc.net/forest/dt-0054/dt-0054/forest/dt-0054/Retraction pairDefinitionA retraction pair on cpos to consists of two continuous functions
such that:
(i.e. )
(i.e. )
In this retraction pair, is called a embedding and is called a projection.Retraction pairs are weakenings of isomorphisms. Intuitively, going , all information is preserved due to requirement 1, but going , we may lose some information (hence the use of in requirement 2).Liam O'Connorhttps://liamoc.net/forest/dt-0055/dt-0055/forest/dt-0055/Examples and counterexamples of retraction pairsExampleHere are two examples of retraction pairs:
] \\
b \ar [r,thick,<->] & y \ar [u,-] \\
a\ar [u,-]\ar [r,thick,<->] & x \ar [u,-]
\end {tikzcd}
$\quad \qquad \qquad $
\begin {tikzcd}
& z \ar [dl, thick,<->] \\
b & y \ar [dl, thick,->] \ar [u,-] \\
a\ar [u,-]\ar [r,thick,<->] & x \ar [u,-]
\end {tikzcd}]]>
(this demonstrates that there can be many retraction pairs )The following, however, are not retraction pairs :
] \\
b \ar [r,thick,<-] & y \ar [u,-] \\
a\ar [u,-]\ar [r,thick,<->] & x \ar [u,-]
\end {tikzcd}
]]>
] \\
b \ar [dr, thick,->] & y \ar [l, thick,->] \ar [u,-] \\
a\ar [u,-]\ar [r,thick,<->] & x \ar [u,-]
\end {tikzcd}
]]>
( but )
( but )
Liam O'Connorhttps://liamoc.net/forest/dt-0056/dt-0056/forest/dt-0056/Composition of retraction pairsDefinitionWe can compose retraction pairs by composing their embedding and projection:https://liamoc.net/forest/dt-0057/dt-0057/forest/dt-0057/Derived products of retraction pairsCorollaryIt follows from the definition of retraction pairs that, for a pair :
and are strict, i.e. and .
is uniquely determined by and vice-versa, so if another retraction pair exists, then . To see why, remember that and must be continuous and therefore monotonic.
is isomorphic to the range of , i.e. .Liam O'Connorhttps://liamoc.net/forest/dt-0058/dt-0058/forest/dt-0058/The category DefinitionThe category is the category where the objects are cpos, the morphisms are retraction pairs, composition is as in Definition and identity is just the retraction pair .Liam O'Connorhttps://liamoc.net/forest/dt-0059/dt-0059/forest/dt-0059/Information ordering in DefinitionThe third point in Corollary suggests a notion of approximation, or information ordering, for cpos. Rather than say, as we did in SS , that for cpos and , iff there exists a continuous function , we now say:
iff there exists a retraction pair Liam O'Connorhttps://liamoc.net/forest/dt-005A/dt-005A/forest/dt-005A/Generalising to All of our other notions for naturally generalise to a setting with retraction pairs : least elements, -chains, upper bounds, colimits, cocontinuous endofunctors and so on.Liam O'Connorhttps://liamoc.net/forest/dt-005C/dt-005C/forest/dt-005C/-chains of cpos in the category DefinitionAn -chain of cpos in the category consists of a family of cpos , together with a family of retraction pairs , shown below:,yshift=0.2em]\ar [r,"g_0"', <-,yshift=-0.2em] &
D_1 \ar [r,"f_1",->,yshift=0.2em]\ar [r,"g_1"', <-,yshift=-0.2em] &
D_2 \ar [r,"f_2",->,yshift=0.2em]\ar [r,"g_2"', <-,yshift=-0.2em] &
D_3 \ar [r,-,dashed,yshift=0.2em]\ar [r,dashed,-,yshift=-0.2em] &
\cdots
\end {tikzcd}
]]>Liam O'Connorhttps://liamoc.net/forest/dt-005D/dt-005D/forest/dt-005D/Endofunctors on DefinitionAn endofunctor on the category is a functor , i.e. a mapping on cpos together with a mapping on retraction pairs, such that:If is a retraction pair then is a retraction pair
(where is composition of retraction pairs)https://liamoc.net/forest/dt-005G/dt-005G/forest/dt-005G/Upper bounds in the category DefinitionA cpo is an upper bound of an -chain of cpos in the category if there is a family of retraction pairs such that the following diagram commutes (i.e. for all , , where is composition of retraction pairs):,"g_0",xshift=-0.2em]
\ar [ddl,<-,"g_1",xshift=-0.35em]\ar [ddl,->,"f_1"',xshift=0.1em]
\ar [dd,<-,"f_2"',xshift=-0.1em]\ar [dd,->,"g_2",xshift=0.3em] \\
&&&\cdots \\
A_0 \ar [r,"s_0",->,yshift=0.2em]\ar [r,"t_0"', <-,yshift=-0.2em] &
A_1 \ar [r,"s_1",->,yshift=0.2em]\ar [r,"t_1"', <-,yshift=-0.2em] &
A_2 \ar [r,-,dotted,yshift=0.2em]\ar [r,dotted,-,yshift=-0.2em]&
\cdots
\end {tikzcd}
]]>Liam O'Connorhttps://liamoc.net/forest/dt-005F/dt-005F/forest/dt-005F/Colimits in the category DefinitionA cpo is the colimit of an -chain of cpos if is both an upper bound, i.e. there exists retraction pairs , and for any other upper bound , for which there will exist retraction pairs , there exists a unique retraction pair such that for all , where is composition of retraction pairs. Viewed diagramatically, it is the same as Definition where continuous functions are replaced by retraction pairs.https://liamoc.net/forest/dt-005E/dt-005E/forest/dt-005E/Cocontinuous endofunctors on DefinitionAn endofunctor is cocontinuous iff it preserves colimits of -chains of cpos. That is, given a chain where is a colimit:
,xshift=-0.2em]
\ar [ddl,<-,xshift=-0.35em]\ar [ddl,->,xshift=0.1em]
\ar [dd,<-,xshift=-0.1em]\ar [dd,->,xshift=0.3em] \\
&&&\cdots \\
D_0 \ar [r,"f_0",->,yshift=0.2em]\ar [r,"g_0"', <-,yshift=-0.2em] &
D_1 \ar [r,"f_1",->,yshift=0.2em]\ar [r,"g_1"', <-,yshift=-0.2em] &
D_2 \ar [r,-,dotted,yshift=0.2em]\ar [r,dotted,-,yshift=-0.2em]&
\cdots
\end {tikzcd}
]]>
Then is a colimit for the following chain:
,xshift=-0.2em]
\ar [ddl,<-,xshift=-0.35em]\ar [ddl,->,xshift=0.1em]
\ar [dd,<-,xshift=-0.1em]\ar [dd,->,xshift=0.3em] \\
&&&\cdots \\
\mathcal {F}(D_0) \ar [r,"\mathcal {F}(f_0)",->,yshift=0.2em]\ar [r,"\mathcal {F}(g_0)"', <-,yshift=-0.2em] &
\mathcal {F}(D_1) \ar [r,"\mathcal {F}(f_1)",->,yshift=0.2em]\ar [r,"\mathcal {F}(g_1)"', <-,yshift=-0.2em] &
\mathcal {F}(D_2) \ar [r,-,dotted,yshift=0.2em]\ar [r,dotted,-,yshift=-0.2em]&
\cdots
\end {tikzcd}
]]>Liam O'Connorhttps://liamoc.net/forest/dt-005I/dt-005I/forest/dt-005I/Extending cpo Mappings to endofunctors on If is a mapping on cpos built up from basic cpos using the constructions , , , , , as well as and , then extends to a (covariant!) cocontinuous functor on .
We shall detail the construction for products and functions here, but the other constructions are all similar.Liam O'Connorhttps://liamoc.net/forest/dt-005J/dt-005J/forest/dt-005J/ operation for retraction pairsDefinitionGiven two retraction pairs and , our retraction pair for their product is just the product of their embedding and projection, i.e. , using our product operation on continuous functions:
Liam O'Connorhttps://liamoc.net/forest/dt-005K/dt-005K/forest/dt-005K/ operation for retraction pairsDefinitionWe are given two retraction pairs and
. To define a suitable covariant functor, we define our morphism mapping in terms of our operation on continuous functions:
Note that the positions of and are swapped in the above definition.
Unlike with the category , this functor is not contravariant but covariant: Note the positions of and are not swapped!https://liamoc.net/forest/dt-005B/dt-005B/forest/dt-005B/Fixed point theorem for endofunctors on TheoremEvery cocontinuous endofunctor on has a least fixed point, given by the colimit of the ascending -chain:
,yshift=0.2em]\ar [r,"g_0"', <-,yshift=-0.2em] &
\mathcal {F}(\mathbf {1}) \ar [r,"f_1",->,yshift=0.2em]\ar [r,"g_1"', <-,yshift=-0.2em] &
\mathcal {F}(\mathcal {F}(\mathbf {1})) \ar [r,"f_2",->,yshift=0.2em]\ar [r,"g_2"', <-,yshift=-0.2em] &
\mathcal {F}(\mathcal {F}(\mathcal {F}(\mathbf {1}))) \ar [r,-,dashed,yshift=0.2em]\ar [r,dashed,-,yshift=-0.2em] &
\cdots
\end {tikzcd}]]>
Where the retraction pairs are defined by:
Liam O'Connorhttps://liamoc.net/forest/dt-005H/dt-005H/forest/dt-005H/The colimit ConstructionGiven an -chain:,yshift=0.2em]\ar [r,"g_0"', <-,yshift=-0.2em] &
D_1 \ar [r,"f_1",->,yshift=0.2em]\ar [r,"g_1"', <-,yshift=-0.2em] &
D_2 \ar [r,"f_2",->,yshift=0.2em]\ar [r,"g_2"', <-,yshift=-0.2em] &
D_3 \ar [r,-,dashed,yshift=0.2em]\ar [r,dashed,-,yshift=-0.2em] &
\cdots
\end {tikzcd}
]]>The colimit (or inverse limit) is the cpo of -tuples:
That is, it is countable sequence of elements, one for each domain , where each element is consistent with earlier elements.Ordering: The ordering is the pointwise ordering of products, naturally generalised to -tuples. Under this ordering, is a cpo. In fact if each is a Scott domain, so is .
Liam O'ConnorProof
We shall prove that is an upper bound of the -chain. Proof that it is the least upper bound is straightforward but tedious, and is omitted.
We must construct a family of retraction pairs:
such that the following diagram commutes:
,xshift=-0.2em]
\ar [ddl,<-,xshift=-0.35em]\ar [ddl,->,xshift=0.1em]
\ar [dd,<-,xshift=-0.1em]\ar [dd,->,xshift=0.3em] \\
&&&\cdots \\
D_0 \ar [r,"f_0",->,yshift=0.2em]\ar [r,"g_0"', <-,yshift=-0.2em] &
D_1 \ar [r,"f_1",->,yshift=0.2em]\ar [r,"g_1"', <-,yshift=-0.2em] &
D_2 \ar [r,-,dotted,yshift=0.2em]\ar [r,dotted,-,yshift=-0.2em]&
\cdots
\end {tikzcd}
]]>
Defining the projection of the retraction pair is straightforward:
However, to define the embedding requires us to, for a given value , produce an -tuple of values consistent with in every domain . We do this by defining in terms of helper functions :
The helper functions are defined by composing sequences of embeddings (s) or projections (s), depending on whether or . For example, when :
Liam O'Connorhttps://liamoc.net/forest/dt-005L/dt-005L/forest/dt-005L/Semantics of untyped -calculusRecall the untyped calculus:
Liam O'Connorhttps://liamoc.net/forest/dt-004K/dt-004K/forest/dt-004K/Untyped -calculusDefinition Untyped -calculus consists only of untyped (higher-order) functions:
We mentioned before that the semantic domain of this language must be a cpo such that In other words, solutions to this equation are fixed points of . The least such fixed point can expressed, by Theorem , as the colimit of the -chain:
,yshift=0.2em]\ar [r,"g_0"', <-,yshift=-0.2em] &
\mathcal {F}(\mathbf {1}) \ar [r,"f_1",->,yshift=0.2em]\ar [r,"g_1"', <-,yshift=-0.2em] &
\mathcal {F}(\mathcal {F}(\mathbf {1})) \ar [r,"f_2",->,yshift=0.2em]\ar [r,"g_2"', <-,yshift=-0.2em] &
\mathcal {F}(\mathcal {F}(\mathcal {F}(\mathbf {1}))) \ar [r,-,dashed,yshift=0.2em]\ar [r,dashed,-,yshift=-0.2em] &
\cdots
\end {tikzcd}
]]>
But, the least solution to this equation is trivial: , because . A non-trivial solution is obtained by starting the chain at , the cpo containing just , rather than .
,yshift=0.2em]\ar [r,"g_0"', <-,yshift=-0.2em] &
\mathcal {F}(\mathbf {2}) \ar [r,"f_1",->,yshift=0.2em]\ar [r,"g_1"', <-,yshift=-0.2em] &
\mathcal {F}(\mathcal {F}(\mathbf {2})) \ar [r,"f_2",->,yshift=0.2em]\ar [r,"g_2"', <-,yshift=-0.2em] &
\mathcal {F}(\mathcal {F}(\mathcal {F}(\mathbf {2}))) \ar [r,-,dashed,yshift=0.2em]\ar [r,dashed,-,yshift=-0.2em] &
\cdots
\end {tikzcd}
]]>We will now sketch a proof of the retraction pair between and , by providing two functions, and its inverse .Observe that each element of (for 0]]>) is a function . Therefore, an elemen
t of the colimit is an -tuple of such functions. To define , we must essentially "apply" each function in the element (viewed as an -tuple of functions) to the element (viewed as an -tuple of values). More specifically, we say that is an -tuple , as follo
ws:
To define , we are given a (continuous) function and must construct the -tuple of approximations at every . We do this by projecting the action of down to . We say that is an -tuple where:
Liam O'ConnorDenotations for untyped -calculusDefinitionUsing the new functions and , it is now straightforward to define a semantics for untyped -calculus, where is an environment :
This semantics does not distinguish non-terminating computations from terminating ones. To model call-by-value more faithfully, we could use the equation instead, and for call-by-name we could use . The constructions are very similar.
Liam O'Connorhttps://liamoc.net/forest/dt-005V/dt-005V/forest/dt-005V/Monadic semantics, Scott domains and nondeterminismLectureThis lecture is based on material from Carl Gunter, Glynn Winskel, Graham Hutton, Kai Engelhardt, Dexter Kozen, Andrew Myers, John Longley, Dana Scott, and Joseph Stoy.Liam O'Connorhttps://liamoc.net/forest/dt-005Z/dt-005Z/forest/dt-005Z/Generalising our semanticsWe return to the language we saw previously:Liam O'Connorhttps://liamoc.net/forest/dt-005R/dt-005R/forest/dt-005R/The LanguageDefinitionUsing notation similar to Backus-Naur Form (BNF):
If we wish to add other kinds of effects (beyond mutation of state) to our language, this will necessarily affect the semantic domain. Rather than rewrite the entire semantics for each possible setting, we will generalise the semantics to work over any instance of an algebraic structure, called a monad.Liam O'Connorhttps://liamoc.net/forest/dm-000U/dm-000U/forest/dm-000U/MonadDefinitionA monad on the category consists of an endofunctor and two operations (natural transformations) for all -objects : and , such that the following diagrams<
/fr:link> commute:
In equational form, these laws are
In computer science, is sometimes called unit, pure, or return, and is usually called join.Liam O'Connorhttps://liamoc.net/forest/dt-005P/dt-005P/forest/dt-005P/Flat domains as monadsExampleThe flat domain lifting operation forms a monad, where the endofunctor , the operation collapses the two values, and is simply .Sometimes it is more convenient to work with the Kleisli composition operator, ra
ther than the operations and directly.Liam O'Connorhttps://liamoc.net/forest/dm-000T/dm-000T/forest/dm-000T/Kleisli categoryDefinitionFor a monad over the category , the Kleisli category has the same objects as , but the morphisms are those morphisms of that have the form . Composition is defined as follows, for morphisms and :
Identity morphisms for this category are just .Liam O'Connorhttps://liamoc.net/forest/dt-005Q/dt-005Q/forest/dt-005Q/Monadic semantics for DefinitionWe define our semantics generically in terms of a monad , using the Kleisli composition operator for :
Liam O'Connorhttps://liamoc.net/forest/dt-005S/dt-005S/forest/dt-005S/Instantiating with the lifting monadExampleInstantiating our monadic semantics where the monad is flat domain lifting, we recover our original semantics of .Liam O'Connorhttps://liamoc.net/forest/dt-005T/dt-005T/forest/dt-005T/Instantiating with exceptionsExample Let us instantiate our monadic semantics with the monad , where the added value (from ) is called . The operation collapses the two possible values to and the two possible values to , and the operation is the straightforward injection.Then we may extend our language with lightweight exception constructs:
and define their semantics, leaving our existing semantics unchanged:
Liam O'ConnorNondeterminismLiam O'Connorhttps://liamoc.net/forest/dt-005U/dt-005U/forest/dt-005U/Introduction to nondeterminismWhen modelling programming languages we sometimes require a way to be imprecise about some aspects of a program
-- usually, this takes the form of non-determinism. Non-determinism can be hard for beginners to grasp, but it typically has to be employed when modelling real programs. For example, suppose we had a greeting program that differed depending on the physical location of the computer:
If we wanted to mathematically model the behaviour of this program, it would be frightfully inconvenient to include the geography of Earth and the computer's physical location in our model. That's where non-determinism comes in. If we abstract away from the geographical details, and instead regard the program as choosing between the two options based on some unspecified criteria, then we can get away with modelling less, at the cost of some detail:
Such underspecified conditionals are usually called non-deterministic choice, where our conditional is written simply as .While we tend to view our physical machines as deterministic automata, the state upon which each decision is deterministically made includes a number of external things which are tedious to model mathematically. We can also use non-determinism to ignore details that we don't care about for our particular domain -- a common example is memory allocation, where it is very convenient (for some programs) to think of memory as infinite, and allocation as an operation that can potentially fail, without specifying exactly when and how this failure can occur. This is normally modelled as a choice between successful allocation and a failure state.Liam O'Connorhttps://liamoc.net/forest/dt-0060/dt-0060/forest/dt-0060/Instantiating our semantics for nondeterminismOur initial semantics for (without loops) was functions on states . When adding loops, we used a cpo for our semantic domain. Since non-deterministic programs can have more than one outcome, a natural choice of semantic domain would be , i.e., functions from an initial state to a non-empty set of possible outcomes.We can provide and operations for our proposed monad for non-determinism :
And, with this semantics, we can easily add a denotation for a non-deterministic choice operator, in terms of union:
Unfortunately this is only the beginning of our troubles. While we have given a valuation function above, its definition uses , and therefore our domain must be a cpo, and all our operations continuous. It is not clear how to order elements of . A natural choice of ordering would be subset inclusion . However, as we lack , there is no least element for this ordering. Furthermore, sim
ply using as our ordering would mean that the deterministic, terminating program that always returns a single state would be considered less informative than the program that may diverge . This would make most of our operations non-continuous.Instead, we shall examine three separate orderings on this set, each of which carries a different view of non-determinism. More generally, we wish to come up with a construction analogous to the powerset operator , but for our semantic domains -- a powerdomain. However, for these orderings to produce valid partial orders, we require a certain theorem that only applies to a certain class of cpos, called "algebraic" cpos. Thus, we will first introduce a richer class of cpos, called Scott domains, and then return to the problem of non-determinism.Liam O'Connorhttps://liamoc.net/forest/dt-005W/dt-005W/forest/dt-005W/Scott domainsLiam O'Connorhttps://liamoc.net/forest/dt-0040/dt-0040/forest/dt-0040/Compactness and FinitenessWe begin by formalising the notion of an element in a cpo representing a finite amount of information.Liam O'Connorhttps://liamoc.net/forest/dt-003W/dt-003W/forest/dt-003W/Boring and interesting setsDefinitionThere are two kinds of directed sets:
Boring sets contain their lub. Example: Finite directed sets are boring (but boring sets aren't all finite!).
Interesting sets don't contain their lub. Example: in the chain is interesting.Following the above intuition, we might be tempted to say that the "infinite" elements of a cpo are those which are the lub of an interesting set, but this notion is too weak. Consider this cpo :
By the above definition, the only infinite element would be , but if we consider the following isomorphic cpo, ordered by subset inclusion:
Then the set cannot be a finite set, as any finite set would be a subset of one of the finite sets in the chain . Thus, it makes more sense for us to call an "infinite" element as well.Liam O'Connorhttps://liamoc.net/forest/dt-003U/dt-003U/forest/dt-003U/CompactnessDefinitionLet be a cpo. Then is compact (a.k.a. finite) iff for all directed :
In English: A compact element will approximate some element of a directed set if it approximates the lub. We write for the set of compact elements of , i.e.:
In the example cpo above, all the elements except and would be compact. Thus, compactness better captures our notion of an element representing a finite amount of information. This understanding of compact elements is a generalisation of the notion of a finite element from the theory of algebraic lattices.Liam O'Connorhttps://liamoc.net/forest/dt-003V/dt-003V/forest/dt-003V/Compact elementsExampleEvery element in a finite cpo is compact. More generally, every element of a cpo of finite height (e.g. ) is compact. This is because finite directed sets are always boring.
Take the cpo of subsets of ordered by inclusion , as seen in Exercise . The compact elements of are those of finite cardinality.
Take the cpo of partial functions on the natural numbers, ordered by inclusion of graphs. The compact elements of are the functions which are defined only for finite domains.Liam O'Connorhttps://liamoc.net/forest/dt-003X/dt-003X/forest/dt-003X/Compact elements with infinitely many approximations Example
Compact elements may still have an infinite number of approximations. Consider the cpo , where we have tacked on an additional top element to our normal cpo of natural numbers extended with infinity. Then, while is not compact, is compact -- it is not the lub of an interesting directed set. If is the lub of a set then must be in the set . Nonetheless, there are an infinite number of approximations to , i.e., elements such that .As an aside, requiring that our compact elements have a truly finite number of approximations is the basis for the theory of Berry domains and stable functions.Liam O'Connorhttps://liamoc.net/forest/dt-003Y/dt-003Y/forest/dt-003Y/Submonoids as a cpoTheoremThe submonoids of a monoid form a cpo under , where union gives the lub.Liam O'Connorhttps://liamoc.net/forest/dt-003Z/dt-003Z/forest/dt-003Z/Both infinite and compactExerciseFind a set in the cpo of submonoids of that is both infinite and compact.
Liam O'ConnorSolution
Take . Let be directed and . Since there must exist such that . Since is a monoid, every positive multiple of is also in , thus and therefore is compact.
Seeing as compact elements are also sometimes called finite, this is surprising as is an infinite set. The reason it is nonetheless compact is that is finitely generated -- it is the smallest submonoid of such that the finite set . In fact, the compact submonoids of are precisely the finitely generated ones.
Liam O'Connorhttps://liamoc.net/forest/dt-005X/dt-005X/forest/dt-005X/Algebraicity and idealsLiam O'Connorhttps://liamoc.net/forest/dt-0041/dt-0041/forest/dt-0041/AlgebraicityDefinitionA cpo is algebraic iff every element is the lub of its compact approximations. That is, a cpo is algebraic iff for all ,
is directed;
Note: It's common in semantics to consider only algebraic cpos with a countable set of compact elements. Such cpos are called -algebraic.Aside: Plotkin provides an equivalent definition of -algebraic cpos in which directed sets are replaced with -chains throughout. Hutton claims this is less appealing, as the definition speaks of an -chain of compact approximations, rather than the
directed set of such.Liam O'Connorhttps://liamoc.net/forest/dt-0042/dt-0042/forest/dt-0042/-algebraic cposExampleMany standard examples of cpos are -algebraic cpos: finite cpos, subsets of a set , partial functions and submonoids of a monoid. In general, any cpo of subalgebras (e.g. subgroups of a group, subrings of a ring etc.) is -algebraic. This is the origin of the terminology.Liam O'Connorhttps://liamoc.net/forest/dt-0043/dt-0043/forest/dt-0043/Non-algebraic cpoCounterexample
In the cpo on the right (seen also in SS ), the element is not the lub of its compact approximations. The only compact element that approximat
es is , and the least upper bound of the set is just , not . That is:
but:
Liam O'Connorhttps://liamoc.net/forest/dt-0045/dt-0045/forest/dt-0045/Nothing suddenly invented at infinityTheoremLet and be algebraic cpos. Then a function is continuous iff, for all :
In other words, in an algebraic cpo, continuous functions are completely defined by their behaviour for compact arguments.This makes precise our earlier slogan in Definition , that continuous functions don't suddenly behave differently for infinite (i.e. non-compact) elements.
Liam O'ConnorProof
First, assuming is continuous, we show that :
It remains to show that if , then is continuous. Using the alternative definition, we shall first show that is monotone. Let for . Then and
thus , therefore:
Next, let be directed.
Liam O'Connorhttps://liamoc.net/forest/dt-0044/dt-0044/forest/dt-0044/ExerciseLet be a continuous function between algebraic cpos. Define:
Then for all , prove that:
Liam O'ConnorSolution
This is powerful. For example, the continuous function on an uncountable cpo is completely determined by the countable relation .Liam O'Connorht
tps://liamoc.net/forest/dt-0047/dt-0047/forest/dt-0047/Down-closureDefinitionGiven a poset , a set is down-closed iff, for all , any is in .Liam O'Connorhttps
://liamoc.net/forest/dt-0048/dt-0048/forest/dt-0048/IdealDefinitionA set is ideal iff it is both down-closed and directed.Liam O'Connorhttps://liamoc.net/forest/dt-0046/dt-0046/forest/dt-0046/I
deal completionDefinitionThe ideal completion of a set , written sometimes as , is the set of all ideal subsets of , i.e.:
Liam O'Connorhttps://liamoc.net/forest/dt-0049/dt-0049/forest/dt-0049/Representation theorem for algebraic cposTheoremEvery algebraic cpo is isomorphic to the ideal completion of its compact elements, ordered by subset inclusion. That is, is an algebraic cpo such that .Liam O'Connorhttps://liamoc.net/forest/dt-005Y/dt-005Y/forest/dt-005Y/Getting closureLiam O'Connorhttps://liamoc.net/forest/dt-004A/dt-004A/forest/dt-004A/BasisDefinition
A set of compact elements is a basis for a cpo iff for all , .Liam O'Connorhttps://liamoc.net/forest/dt-004B/dt-004B/f
orest/dt-004B/Compact basis for algebraic cposTheoremIf is a basis for , then is algebraic and .
Liam O'ConnorProof
If , then where , as is a basis. Since is compact, for some . But since is the lub of , as well. By antisymmetry , hence . Thus , so and is algebraic.Liam O'Connorhttps://liamoc.net/forest/dt-004C/dt-004C/forest/dt-004C/Closure of algebraic cpos under productTheoremIf and are algebraic cpos, then so is their product construction .
Liam O'ConnorProof
In the following proof, we show that is a basis for the product and thereby show via Theorem that is algebraic if and are.
: Let . To show that is compact, let us assume that where is directed. We must show that there exists some element of such that our . As , by the definition of lub on products we can conclude that:
Here we use the notation to indicate the image of a function on a set, i.e. .
Since and are both compact, there must exist and such that and . While it does not follow that , we know that there must exist a pair such that and as is directed. Hence can be our element that is approximated by , i.e. .
is directed for all :
Because and are algebraic, and are directed. As directedness is closed under product, is directed too.
Starting from the right hand side:
Liam O'ConnorProblem
-algebraic cpos are closed under all of our constructions (products and sums, including strict versions of these) except functions and strict functions !
Liam O'Connorhttps://liamoc.net/forest/dt-004D/dt-004D/forest/dt-004D/Scott's original solution: using complete latticesAsideThe lack of closure of algebraicity under the (continuous) function arrow, strict or non-strict, is not satisfying as it means that our semantic domains are not guaranteed to be algebraic even if they are composed from algebraic cpos. Instead, we must replace algebraic cpos with something stronger still.Scott's original solution to this lack of closure was to use a complete lattice instead of cpos, i.e. requiring lubs for all subsets, not just directed ones. This solves the problem with but introduces new problems:
Complete lattices need a top element , but adding a fictitious top (representing inconsistent information) to cpos like is strange.
Extending the functions that capture our primitive semantic operations to complete lattices can spoil nice algebraic properties. Consider these two possible implementations of , the function for the semantics of an expression:
Either of these solutions results in the failure of useful and expected laws for expressions. For example, the left definition above results in the failure of the common equation to eliminate unreachable cases:
And the second definition above results in the failure of this equation that removes redundant checks:
The powerdomain construction does not generalise to complete lattices, so semantics for non-deterministic programs are difficult in this setting.Liam O'Connorhttps://liamoc.net/forest/dt-004E/dt-004E/forest/dt-004E/Consistent completenessDefinitionA poset is consistent complete (or bounded complete) iff exists for all consistent . That is, any set with an upper bound (a consistent set) has a least upper bound.Liam O'Connorhttps://liamoc.net/forest/dt-004F/dt-004F/forest/dt-004F/Consistent completeness vs directed completenessExample
consistent complete
not consistent complete
not directed complete
directed complete
Liam O'Connorhttps://liamoc.net/forest/dt-004G/dt-004G/forest/dt-004G/Scott domainDefinitionA cpo is a Scott domain iff:
is -algebraic,
is consistent complete,
In other words, Scott domains can be summed up by the acronym:
Liam O'Connorhttps://liamoc.net/forest/dt-004H/dt-004H/forest/dt-004H/RemarkThe second requirement in Definition can, in light of the first, be expressed equivalently as: exists for all consistent . This is useful when needing to show that a given cpo is a Scott domain.Liam O'Connorhttps://liamoc.net/forest/dt-004I/dt-004I/forest/dt-004I/Closure of Scott domainsTheoremScott domains are closed under all our cpo constructions, including sums , products , continuous functions , smash sums , smash products and strict functions .
Liam O'ConnorThesisOur semantic domains are Scott domains.Liam O'Connorhttps://liamoc.net/forest/dt-0061/dt-0061/forest/dt-0061/Th
e Hoare powerdomainWe write to denote finite non-empty subsets of . Let be finite, non-empty sets of compact elements of a Scott domain . The Hoare powerdomain construction is based on the following ordering:
The intuition behind this is that "Anything can do, can do better". This ordering has some desirable properties: The least element is , as we might expect. It also satisfies the equation , which intuitively means that a non-deterministic choice is considered to have more information than any of its components. When specialised to the case where is a flat domain like , it simplifies to:
This is, however, not a proper order, but a preorder, as it fails antisymmetry. Even in the flat domain case, and but they are not equal. However, any preorder does induce an equivalence relation, where iff and . Furthermore, if we take the ideal completion of with respect to the preorder (i.e., the set of all -downwards-closed directed subsets of ), we can order them by inclusion to obtain an algebraic domain with compact elements which correspond to equivalence classes of elements under . We have a lub operation for these ideals:
Liam O'Connorhttps://liamoc.net/forest/dt-0062/dt-0062/forest/dt-0062/Hoare powerdomain of Example Let us find the Hoare powerdomain of . Note that is a flat domain so all elements are compact, i.e. . Let us find examine the -ideal subsets of . If and both contain , then iff . As ideal subsets are downwards closed, we can identify an ideal with its union . The ideals of are then isomorphic to domain of all subsets of under subs
et inclusion.Liam O'Connorhttps://liamoc.net/forest/dt-0063/dt-0063/forest/dt-0063/Angelic nondeterminismRemarkConsider the following three programs:
Given a state , let . Then, the possible results of these programs are , , and respectively. Because the Hoare construction identifies -equivalent sets, the Hoare powerdomain semantics will consider programs 1 and 3 to be the same. That is, the non-determinism is angelic. The bad outcome () is only said to happen if it is inevitable.Liam O'Connorhttps://liamoc.net/forest/dt-0064/dt-0064/forest/dt-0064/The Smyth powerdomainAs before, let be finite, non-empty sets of compact elements of a Scott domain . The Smyth powerdomain construction is
based on the following preorder:
The intuition here is "Everything can do, can do worse". It satisfies the equation , which intuitively means that a non-deterministic choice is considered to have less information than any of its components. When applied to a flat domain, it simplifies to:
As with the Hoare powerdomain, this fails to be a partial order, but we can use the same ideal completion trick to induce an algebraic domain where compact elements correspond to equivalence classes of elements under (where is, as with , just defined as ).Liam O'Connorhttps://liamoc.net/forest/dt-0065/dt-0065/forest/dt-0065/Smyth powerdomain of ExampleFirstly note that, as ideals are downwards-closed, any -ideal subsets of will contain all finite subsets of that contain . Let us call those sets trivial. So, a set in is non-trivial if it does not contain and an ideal subset of is non-trivial if it contains a non-trivial set. Observe that for non-trivial sets and , iff . Thus, we can identify an ideal with the down-closure of the intersection of its non-trivial elements. The smaller this set is, the larger the ideal . Hence, and confus
ingly, the non-trivial ideals in the powerdomain (ordered by subset inclusion) correspond to finite subsets of ordered by superset inclusion. As all trivial sets are identified, we just need to throw in the unique trivial ideal, and we can see that the Smyth powerdomain of is isomorphic to the domain of sets ordered by subset inclusion
.Liam O'Connorhttps://liamoc.net/forest/dt-0066/dt-0066/forest/dt-0066/Demonic nondeterminismRemarkNote that all sets that contain are considered equivalent by the Smyth construction . Thus, this models demonic non-determinism: Of the three programs in Remark , the Smyth semantics considers 2 and 3 to be the same. Thus, the possibility of divergence is no different from inevitable divergence.Liam O'Connorhttps://liamoc.net/forest/dt-0067/dt-0067/forest/dt-0067/The Plotkin powerdomainAs before, let be finite, non-empty sets of compact elements of a Scott domain . The Plotkin powerdomain construction is based on the following preorder, simply combining the orderings from the Hoare and Smyth constructions:
This ordering is also called the Egli-Milner ordering. On a flat domain, it simplifies to:
Note that this is antisymmetric in the case of a flat domain, and the lub of a chain of sets can be found by taking the union of all elements of the chain if all elements contain If not, then the element without will be the least upper bound.The failures of antisymmetry can only be observed in domains of height higher than one. Consider a set containing two elements. According to the induced equivalence from this preorder , this set would be considered equal to the set that contains those two elements plus any elements that lie between them on the information ordering:
The Plotkin powerdomain is sometimes called the convex powerdomain, due to the similarity of this to the geometric definition of convexity. Thus, we use the ideal completion trick (as with the Hoare and Smyth constructions) here to arrive at a definition of powerdomain that distinguishes between all three programs outlined in Remark .
Liam O'ConnorAsideThere is a beautiful algebraic characterisation of Plotkin powerdomains in Matthew Hennessy Gordon Plotkin's paper, Full abstraction for a simple parallel programming lang
uage.
References
Matthew Hennessy
Gordon Plotkin
1979
9
7
https://liamoc.net/forest/hennessy-plotkin-1979/
hennessy-plotkin-1979
/forest/hennessy-plotkin-1979/
Full abstraction for a simple parallel programming language
Reference
MFCS '79: Mathematical Foundations of Computer Science 1979
10.1007/3-540-09526-8_8
Context
Backlinks
2025
5
25
https://liamoc.net/forest/loc-000S/
loc-000S
/forest/loc-000S/
Against Curry-Howard Mysticism
As someone who teaches PL theory and has worked in PL theory for many years now, I love the the formulae-as-types notion of construction, also known as the Curry-Howard correspondence. It demonstrates a profound connection between lambda calculi and logic. Wadler's paper and accompanying talk provide an approachable introduction to the topic.Yet, among the audience for such talks (which are primarily geared at fu
nctional programming practitioners rather than academics) are many who, I think, are getting the wrong message somehow. I see muddled, severely distorted, or even outright untrue claims being made about type theory and Curry-Howard quite frequently as a result of these misconceptions. So, to clear the air, I'll state my thesis up-front:
2025525Thesis
For programming and software engineering practice, Curry-Howard is of essentially no practical benefit, unless you are using a dependently-typed language.
Learn it if you want, but it will not and cannot aid you in improving your programming practice (unless you're writing Idris or Lean!).The Curry-Howard correspondence says that types correspond to propositions (or formulae) and programs that inhabit these types correspond to proofs of their respective propositions. So, programs are proofs, yes, but proofs about what?. Certainly not the programs themselves -- without a dependently-typed language, we can't state propositions about programs on the type level. For most standard type systems, our propositions take the form of abstract logical sentences in a fairly limited (and inconsistent) propositional or second order logic, not theorems about programs.2025525But I get theorems from the types! It is true, however, that we learn many theorems about our programs from examining their types. From the judgement , I know that the function will, when executed with an argument, produce a result. This is indeed a theorem! But it is not a theorem arrived at by any use of the Curry-Howard correspondence, but rather a straightfoward consequence of type safety. A similar argument applies when types are used as "witnesses" of a property, e.g.
If is the only way to produce a , then one might be tempted to say that this type "corresponds" to a proposition that a tree is balanced. But this is not a theorem that follows from formulae-as-types but rather from good ol' type safety and enforcement of module boundaries, just as above.The theorems for free also popularised by Wadler, specifically the theorems obtained from the generality of a type signature, are also not a consequence of Curry-Howard, but rather a consequence of the paramet
ricity of the type system.Furthermore, type isomorphisms (for example, ), which can be used to simplify programs, are also not a consequence of Curry-Howard. The analogous logical statement that is true, sure, but so is . In a simply typed programming language, nearly all useful types ( etc.) will be logically equivalent to just , so such propositional equivalence is much too weak. Such isomorphisms are between semantic domains (covered in detail in my domain theory notes) -- the meanings of types, not their logical analogues.2025525Why does this happen?Many programmers can get swept up in mysticism about Curry-Howard, overstating its consequences. Of these, I think there are two main groups: the mathematically curious and the mathematical fetishists. The curious are those who, usually through no fault of their own, have no or little experience with program specification, verification, formal methods, semantics, proofs etc, before being introduced to Curry-Howard. They then make the mistake of thinking that Curry-Howard is central to all of these new areas to them, simply because
it was their starting point. To a certain extent, I do understand this viewpoint -- being excited about a particular topic in research is a good thing! The good thing here, is that this problem can be resolved simply by doing better education, so that programmers' first exposure to logic, for example, isn't in third year university, when puzzling out types for lambda calculus terms.Far more problematic, though, is the culture of mathematical fetishism within the functional programming community: the use of mathematical jargon to obscure rather than clarify -- to show superiority over others, rather than establishing a common vocabulary. One example of this is those who insist on calling the Curry-Howard correspondence "the Curry-Howard isomorphism" because it uses an exclusively mathematical term, "isomorphism", rather than the more commonly-used (and more accurate) "correspondence". They w
ill often talk very confidently, using large amounts of mathematical jargon, where in reality the idea under discussion is either significantly more straightforward than indicated, or outright wrong. People who behave in this way are really toxic for a programming community. The only solution I can recommend is to try hard to exclude this kind of toxic behaviour from programming communities, and to devote resources to supporting those learners who would otherwise potentially be led astray by this kind of behaviour.
Liam O'Connor
https://liamoc.net/forest/index/
index
/forest/index/
Liam O'Connor
false
https://liamoc.net/forest/liamoc/liamoc/forest/liamoc/Liam O'ConnorPersonhttps://liamoc.netAustralian National University0000-0003-2765-4269Senior LecturerI am a Senior Lecturer in Foundations at the Australian National Unive
rsity School of Computing, on Ngunnawal and Ngambri country. I'm also an Honorary Fellow at the University of Edinburgh Laboratory for Foundations of Computer Science, where I worked until 2024.Lately, my research has been focused on property-based testing, semantics and temporal logic, but I have very broad research interests. See my personal bibliography for a full list of my work.Previously, I lectured courses at UNSW Sydney, where I did my PhD with Gabriele Keller and the Trustworthy Systems Team lead by Gernot Heiser, focusing on the Cogent project.Full details about me can be found on my curriculum vitae, which includes a list of students. My contact details can be found here.I'm also an experienced liturgical singer and cantor. I journal my experiences in church music at the Church Music Corner.
Liam O'Connorhttps://liamoc.net/forest/loc-000E/loc-000E/forest/loc-000E/About this websiteThis website is a "forest" created using the Forester tool, a system of evergreen hypertext notes developed by, among others, Jon Sterling and Ke
nto Okura. To search my forest, press Ctrl+K.
Liam O'ConnorLecture notesDomain theory
Liam O'Connorhttps://liamoc.net/forest/news/news/forest/news/News
25.05.16
I have completed the domain theory lecture notes.
25.05.01
I have agreed to co-supervise Yi Yao, a new PhD student with Peter Hofner.
25.03.22
I have joined the PC for Haskell '25: 18th ACM SIGPLAN Haskell Symposium.
25.03.13
I have joined the PC for FProPer '25: 2nd ACM SIGPLAN Workshop on Functional Programming for Productivity and Performance.
25.02.04
Jack Bashford has joined me for a semester project working on Holbert.
25.01.08
I have joined the PC for APLAS '25: 23rd Asian Symposium on Programming Languages and Systems.
24.11.05
I have joined the PC for ICFP '25: 29th ACM SIGPLAN International Conference on Functional Programming.
24.10.22
I have joined the PC for PLDI '25: 46th ACM SIGPLAN International Conference on Programming Language Design and Implementation.
24.09.17
I have agreed to organise the ICFP '25 Programming Contest.
24.09.30
I was delighted to spend a week with the WG2.1 folks here at the ANU.
24.09.09
Our student Rayhana Amjad has published her first paper, Semantics for Linear-time Temporal Logic with Finite Observations at EXPRESS/SOS.
24.07.30
I have taken a new position as a Senior Lecturer at the Australian National University.
Liam O'Connor
https://liamoc.net/forest/news/
news
/forest/news/
News
25.05.16
I have completed the domain theory lecture notes.
25.05.01
I have agreed to co-supervise Yi Yao, a new PhD student with Peter Hofner.
25.03.22
I have joined the PC for Haskell '25: 18th ACM SIGPLAN Haskell Symposium.
25.03.13
I have joined the PC for FProPer '25: 2nd ACM SIGPLAN Workshop on Functional Programming for Productivity and Performance.
25.02.04
Jack Bashford has joined me for a semester project working on Holbert.
25.01.08
I have joined the PC for APLAS '25: 23rd Asian Symposium on Programming Languages and Systems.
24.11.05
I have joined the PC for ICFP '25: 29th ACM SIGPLAN International Conference on Functional Programming.
24.10.22
I have joined the PC for PLDI '25: 46th ACM SIGPLAN International Conference on Programming Language Design and Implementation.
24.09.17
I have agreed to organise the ICFP '25 Programming Contest.
24.09.30
I was delighted to spend a week with the WG2.1 folks here at the ANU.
24.09.09
Our student Rayhana Amjad has published her first paper, Semantics for Linear-time Temporal Logic with Finite Observations at EXPRESS/SOS.
24.07.30
I have taken a new position as a Senior Lecturer at the Australian National University.
Related
Liam O'Connor
https://liamoc.net/forest/typesig-dt/
typesig-dt
/forest/typesig-dt/
Domain Theory (TypeSIG)
Course
University of Edinburgh
https://typesig.pl/resources/domain-theory
I ran this course as an opt-in invited lecture series with TypeSIG at University of Edinburgh. Suprisingly, around 15 students consistently showed up throughout.
Topics include denotational semantics, fixed points, categories and constructions, PCF, scott domains, recursive domains, and powerdomains.
https://liamoc.net/forest/uoe/
uoe
/forest/uoe/
University of Edinburgh
Institution
Scotland, United Kingdom
https://ed.ac.uk
Contributions