leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Work on setoids

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-12 16:17:35 +01:00
parent 978eb83a7f
commit 32e29aedb8
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
7 changed files with 310 additions and 136 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
thesis/.vscode/ltex.hiddenFalsePositives.en-US.txt vendored
View file

@ -31,3 +31,4 @@
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: First, note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can equivalently be reformulated as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we are left to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: First, note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can equivalently be reformulated as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we are left to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"IF_IS","sentence":"^\\QLet \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid morphism, we define \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q point wise: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"IF_IS","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}

63
thesis/bib.bib
View file

@ -1,35 +1,43 @@
% @inproceedings{agda,
% title = {Towards a practical programming language based on dependent type theory},
% author = {Ulf Norell},
% year = {2007},
% url = {https://api.semanticscholar.org/CorpusID:118357515}
% }
@software{agda,
author = {{Agda Developers}},
title = {{Agda}},
url = {https://agda.readthedocs.io/},
version = {2.6.5}
author = {{Agda Developers}},
title = {{Agda}},
url = {https://agda.readthedocs.io/},
version = {2.6.5}
}
@manual{agda-man,
title = {Agda User Manual},
author = {The Agda Team},
year = {2024},
month = {03},
day = {06},
title = {Agda User Manual},
author = {The Agda Team},
year = {2024},
month = {03},
day = {06},
version = {2.6.4.3},
url = {https://agda.readthedocs.io/en/v2.6.4.3/}
url = {https://agda.readthedocs.io/en/v2.6.4.3/}
}
@manual{coq-man,
title = {The Coq Reference Manual},
author = {The Coq Development Team},
year = {2024},
month = {03},
day = {01},
title = {The Coq Reference Manual},
author = {The Coq Development Team},
year = {2024},
month = {03},
day = {01},
version = {8.19.1},
url = {https://coq.inria.fr/doc/V8.19.0/refman/}
url = {https://coq.inria.fr/doc/V8.19.0/refman/}
}
@article{setoids,
title = {Category theoretic structure of setoids},
journal = {Theoretical Computer Science},
volume = {546},
pages = {145-163},
year = {2014},
note = {Models of Interaction: Essays in Honour of Glynn Winskel},
issn = {0304-3975},
doi = {https://doi.org/10.1016/j.tcs.2014.03.006},
url = {https://www.sciencedirect.com/science/article/pii/S0304397514001819},
author = {Yoshiki Kinoshita and John Power},
keywords = {Setoid, Proof assistant, Proof irrelevance, Cartesian closed category, Coproduct, -category, -inserter, -category, -coinserter},
abstract = {A setoid is a set together with a constructive representation of an equivalence relation on it. Here, we give category theoretic support to the notion. We first define a category Setoid and prove it is Cartesian closed with coproducts. We then enrich it in the Cartesian closed category Equiv of sets and classical equivalence relations, extend the above results, and prove that Setoid as an Equiv-enriched category has a relaxed form of equalisers. We then recall the definition of E-category, generalising that of Equiv-enriched category, and show that Setoid as an E-category has a relaxed form of coequalisers. In doing all this, we carefully compare our category theoretic constructs with Agda code for type-theoretic constructs on setoids.}
}
@inproceedings{agda-categories,
@ -50,6 +58,15 @@ version = {2.6.5}
series = {CPP 2021}
}
@software{agda-stdlib,
author = {{The Agda Community}},
month = dec,
title = {{Agda Standard Library}},
url = {https://github.com/agda/agda-stdlib},
version = {2.0},
year = {2023}
}
@incollection{Altenkirch_2017,
doi = {10.1007/978-3-662-54458-7_31},
url = {https://doi.org/10.1007%2F978-3-662-54458-7_31},

6
thesis/main.tex
View file

@ -104,7 +104,8 @@
\makeatother
% \usepackage{noto-mono}
\usepackage[scale=.8]{noto-mono}
% \usepackage{noto}
% TODO Need different mono font, noto-mono has weird font sizing...
\usepackage{unicode-math}
% \setmainfont{STIX-Regular}
@ -113,6 +114,9 @@
\usepackage{mathrsfs}
\usepackage{xargs}
\usepackage{xstring}
\usepackage{accents} % provides \accentset
\newcommand*{\dbtilde}[1]{\tilde{\raisebox{0pt}[0.85\height]{\(\tilde{#1}\)}}}
% https://unicodeplus.com/U+3016
\newcommand*{\lbparen}{〖}

13
thesis/src/01_preliminaries.tex
View file

@ -96,7 +96,7 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
=\; & dstl \circ \lbrack id \times i_1 , id \times i_2 \rbrack \circ (f \times g + f \times h) \\
=\; & dstl \circ dstl^{-1} \circ (f \times g + f \times h) \\
=\; & (f \times g + f \times h) \\
=\; & (f \times g + f \times h) \circ dstl \circ dstl^{-1}
=\; & (f \times g + f \times h) \circ dstl \circ dstl^{-1}\tag*{\qedhere}
\end{alignat*}
\end{proof}
@ -156,7 +156,7 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
\\=\;&dstl \circ [ (id \times i_1) \circ swap , (id \times i_2) \circ swap ] \circ dstr
\\=\;&dstl \circ [ id \times i_1 , id \times i_2 ] \circ (swap + swap) \circ dstr
\\=\;&dstl \circ dstl^{-1} \circ (swap + swap) \circ dstr
\\=\;&(swap + swap) \circ dstr
\\=\;&(swap + swap) \circ dstr\tag*{\qedhere}
\end{alignat*}
\end{enumerate}
\end{proof}
@ -235,10 +235,10 @@ Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tup
Let \((X , \alpha : X \rightarrow FX), (Y, \beta : Y \rightarrow FY)\) and \((Z , \gamma : Z \rightarrow FZ)\) be F-coalgebras.
Composition of \(f : (X, \alpha) \rightarrow (Y, \beta)\) and \(g : (Y, \beta) \rightarrow (Z, \gamma)\) is composition of the underlying morphisms in \(\C \) where:
\begin{alignat*}{1}
& \gamma \circ g \circ f \\
=\; & Fg \circ \beta \circ f \\
=\; & Fg \circ Ff \circ \alpha \\
=\; & F(g \circ f) \circ \alpha
& \gamma \circ g \circ f \\
=\; & Fg \circ \beta \circ f \\
=\; & Fg \circ Ff \circ \alpha \\
=\; & F(g \circ f) \circ \alpha\tag*{\qedhere}
\end{alignat*}
\end{proof}
@ -514,5 +514,6 @@ to establish some notation and then describe how to obtain a monad via existence
\item[\ref{K3}] \(\free{f} \circ \free{g} = \free{\freee{f} \circ g}\) for any \(f : Y \rightarrow UFZ, g : X \rightarrow UFY\)
By uniqueness of \(\free{\freee{f} \circ g}\) we are left to show \(\free{f} \circ \free{g} \circ \eta = \free{f} \circ g\) which again follows directly by the universal property of \(\free{g}\).
\qedhere
\end{itemize}
\end{proof}

15
thesis/src/03_partiality-monads.tex
View file

@ -34,7 +34,7 @@ To ensure that programs are partial, we recall the following notion by Cockett a
\end{lemma}
\begin{proof}
This follows by~\ref{R3} and~\ref{R1}:
\[\tdom f \circ \tdom f = \tdom (f \circ \tdom f) = \tdom f\]
\[\tdom f \circ \tdom f = \tdom (f \circ \tdom f) = \tdom f\tag*{\qedhere}\]
\end{proof}
The idempotent morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness of \(f : X \rightarrow Y\). In the category of partial functions this takes the following form:
@ -144,7 +144,7 @@ The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_2) \circ \langle i_2 , id \rangle
\\=\;&(id\;+\;!) \circ i_2 \circ \langle i_2 , id \rangle
\\=\;&i_2 \;\circ \; ! \circ \langle i_2 , id \rangle
\\=\;&i_2 \;\circ \; !
\\=\;&i_2 \;\circ \; !\tag*{\qedhere}
\end{alignat*}
\end{proof}
@ -259,6 +259,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
Thus, \([ g , id ] = \coalg{\alpha}\) by uniqueness of \(\coalg{\alpha}\).
It follows: \[g = [ g , id ] \circ i_1 =\;\coalg{\alpha} \circ i_1 = f^*\]
\item[\ref{D3}] This follows immediately since \(\tau \) is the unique coalgebra morphism from \((X \times DY, dstl \circ (id \times out))\) into the terminal coalgebra \((D(X \times Y) , out)\).
\qedhere
\end{itemize}
\end{proof}
@ -300,6 +301,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
\\=\;&out \circ f^* \circ later \tag*{\ref{D2}}
\end{alignat*}
\end{itemize}
Thus, the postulated properties have been proven.
\end{proof}
\begin{theorem}
@ -326,6 +328,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
\\=\;&[ out \circ f^* \circ g , i_2 \circ f^* \circ g^* ] \circ out\tag*{\ref{D2}}
\end{alignat*}
\end{itemize}
This concludes the proof.
\end{proof}
Finality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C}}\) yields the following proof principle:
@ -435,6 +438,7 @@ Finality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C}
\end{tikzcd}
\]
\end{itemize}
Thus, it has been shown that \(\mathbf{D}\) is a strong monad.
\end{proof}
To prove that \(\mathbf{D}\) is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} or \textit{Parametric Corecursion}~\cite{param-corec}. In our setting this takes the following form:
@ -462,7 +466,7 @@ To prove that \(\mathbf{D}\) is commutative we will use another proof principle
Let \(g : X \rightarrow D(Y + X)\) be guarded by \(h : X \rightarrow Y + D(Y+X)\) and \(f, i : X \rightarrow DY\) be solutions of g.
It suffices to show \({[ now , f ]}^* = {[ now , i ]}^*\), because then follows:
\[f = {[ now , f ]}^* \circ g = {[ now , i ]}^* \circ g = i\]
We prove this by coinduction using:
This is proven by coinduction using
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcY29hbGd7LX0iXSxbMiwwLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
\[
\begin{tikzcd}[ampersand replacement=\&]
@ -475,6 +479,7 @@ To prove that \(\mathbf{D}\) is commutative we will use another proof principle
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=2-1]
\end{tikzcd}
\]
which concludes the proof.
\end{proof}
Let us record some facts that we will use to prove commutativity of \(\mathbf{D}\):
@ -512,7 +517,7 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
\begin{alignat*}{1}
& out \circ \sigma \circ (out^{-1} \times id)
\\=\;&(id + \sigma) \circ dstr \circ (out \times id) \circ (out^{-1} \times id)\tag*{\ref{sigma1}}
\\=\;&(id + \sigma) \circ dstr
\\=\;&(id + \sigma) \circ dstr\tag*{\qedhere}
\end{alignat*}
\end{itemize}
\end{proof}
@ -571,7 +576,7 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
& Ddstr \circ \tau \circ dstr^{-1}
\\=\;&[ Ddstr \circ \tau \circ (i_1 \times id) , Ddstr \circ \tau \circ (i_2 \times id) ]
\\=\;&[ Ddstr \circ D(i_1 \times id) \circ \tau , Ddstr \circ D(i_2 \times id) \circ \tau ]
\\=\;&[ Di_1 \circ \tau , Di_2 \circ \tau ]
\\=\;&[ Di_1 \circ \tau , Di_2 \circ \tau ]\tag*{\qedhere}
\end{alignat*}
\end{proof}

9
thesis/src/04_iteration.tex
View file

@ -329,9 +329,8 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
\\=\;&[ (id + dstr) \circ (eval + id) \circ (id + (i_1 \times id)) \circ dstr \circ (f \times id)
\\&, (id + dstr) \circ (eval + id) \circ i_2 \circ (h \times id) ]
\\=\;&[ (eval + i_1) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ]
\\=\;&[ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr \circ dstr^{-1}.
\\=\;&[ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr \circ dstr^{-1}.\tag*{\qedhere}
\end{alignat*}
\qedhere
\end{itemize}
\end{proof}
@ -674,6 +673,7 @@ Of course there is also a symmetric version of this.
\\=\;&(((\tau \circ (id \times \tau) \circ \alpha) + id) \circ dstl \circ (id \times h))^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
\end{itemize}
Thus, strength of \(\mathbf{K}\) has been proven.
\end{proof}
As we did when proving commutativity of \(\mathbf{D}\), let us record some facts about \(\tau \) and the induced \(\sigma \), before proving commutativity of \(\mathbf{K}\).
@ -727,6 +727,7 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
\\=\;&\sigma \circ (f^* \times g^*)
\end{alignat*}
\end{itemize}
This concludes the proof.
\end{proof}
The following Lemma is central to the proof of commutativity.
@ -907,7 +908,7 @@ The following Lemma is central to the proof of commutativity.
\\=\;&((((\psi + id) \circ dstr \circ (g \times id))^\sharp + id) \circ dstl \circ (id \times h))^\sharp\tag{\ref{law:uniformity}}
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\sharp \times ((\eta + id) \circ h)^\sharp)
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times ((\eta + id) \circ h)^\sharp)\tag{\autoref{lem:KCommKey}}
\\=\;&((((\psi + id) \circ dstl \circ (id \times h))^\sharp + id) \circ dstr \circ (g \times id))^\sharp.
\\=\;&((((\psi + id) \circ dstl \circ (id \times h))^\sharp + id) \circ dstr \circ (g \times id))^\sharp.\tag*{\qedhere}
\end{alignat*}
\end{proof}
@ -943,7 +944,7 @@ The following Lemma is central to the proof of commutativity.
\\=\;&((\tau \circ \Delta) + \langle f^\sharp , id \rangle) \circ f
\\=\;&(\tau + id) \circ (\Delta + \langle f^\sharp , id \rangle) \circ f
\\=\;&(\tau + id) \circ dstl \circ \langle f^\sharp , f \rangle
\\=\;&(\tau + id) \circ dstl \circ (id \times f) \circ \langle f^\sharp , id \rangle.
\\=\;&(\tau + id) \circ dstl \circ (id \times f) \circ \langle f^\sharp , id \rangle.\tag*{\qedhere}
\end{alignat*}
\end{proof}

339
thesis/src/05_setoids.tex
View file

@ -2,33 +2,34 @@
In \autoref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality, but it also respects computation time. One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified. In this chapter we will use the quotients-as-setoid approach, i.e.\ we will work in the category of setoids and show that the quotiented delay monad is the initial pre-Elgot monad in this category.
Let us introduce the category that we are working in:
\section{Setoids in Type Theory}
We will now introduce the category that the rest of the chapter will take place in. Let us start with some basic definitions.
\begin{definition}[Setoid]
A setoid is a tuple \((A, \hat{=})\) where \(A\) (usually called the \textit{carrier}) is a type and \(\hat{=}\) an equivalence relation on the inhabitants of \(A\).
A setoid is a tuple \((A, \overset{A}{=})\) where \(A\) (usually called the \textit{carrier}) is a type and \(\overset{A}{=}\) is an equivalence relation on the inhabitants of \(A\).
\end{definition}
Morphisms between setoids are functions that respect the equivalence relation.
In the rest of this chapter we will not use the tuple notation for introducing setoids, instead we will just say `Let \(A\) be a setoid' and implicitly call the equivalence relation \(\overset{A}{=}\).
\begin{definition}[Setoid Morphism]
A morphism between two setoids \((A , =^A)\) and \((B , =^B)\) is a function \(f : A \rightarrow B\) such that \(x =^A y\) implies \(fx =^B fy\) for any \(x, y : A\).
\begin{definition}[Setoid Function]
A function on setoids \(A\) and \(B\) is a function \(f : A \rightarrow B\) between the carriers, such that \(f\) respects the equivalences, i.e.\ for any \(x,y : A\), \(x \overset{A}{=} y\) implies \(f\;x \overset{B}{=} f\;y\). We will denote setoid functions as \(A \leadsto B\).
\end{definition}
Setoids and setoid morphisms form a category that we call \(\setoids\).
\improvement[inline]{Talk about equality between setoid morphisms}
\improvement[inline]{Text is not good}
The function space setoid is of special interest, since it defines equality between functions.
\begin{definition}[Function Space Setoid]
Given two setoids \(A\) and \(B\). The function space setoid on these setoids is defined as \((A \leadsto B, \doteq)\) or just \(A \leadsto B\), where \(\doteq\) is point wise equality on setoid functions.
\end{definition}
Setoids together with setoid functions form a category that we will call \(\setoids\). Properties of \(\setoids\) have already been examined in~\cite{setoids}, however we will reiterate some of these properties now to introduce notation that will be used for the rest of the chapter.
\begin{lemma}
\(\setoids\) is a distributive category.
\end{lemma}
\begin{proof}
To show that \(\setoids\) is (co)Cartesian we will give the respective data types and unique morphisms, this also introduces notation we will use for the rest of the chapter. We will not include the proofs that the morphisms are setoid morphisms, these can be looked up in the Agda standard library. % chktex 36
\todo[inline]{Cite agda-stdlib}
\todo[inline]{Introduce coproduct equality sign}
To show that \(\setoids\) is (co)Cartesian we will give the respective data types and unique functions. % chktex 36
For brevity, we will omit the proofs that the functions respect the corresponding equivalences, these are however included in the Agda standard library~\cite{agda-stdlib}.
\begin{itemize}
\item \textbf{Products}:
@ -43,6 +44,7 @@ Setoids and setoid morphisms form a category that we call \(\setoids\).
→ (A → B) → (A → C) → A → (B × C)
< f , g > x = (f x , g x)
\end{minted}
The product setoid is denoted \((A \times B, \overset{\times}{=})\) or just \(A \times B\). Equality of products is defined in the canonical way.
\item \textbf{Terminal Object}:
\begin{minted}{agda}
record ⊤ {l} : Set l where
@ -51,6 +53,7 @@ Setoids and setoid morphisms form a category that we call \(\setoids\).
! : ∀ {l} {X : Set l} → X → ⊤ {l}
! _ = tt
\end{minted}
The terminal setoid is thus \((\top, \overset{\top}{=})\), where \(\top \overset{\top}{=} \top\).
\item \textbf{Coproducts}:
\begin{minted}{agda}
data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
@ -62,6 +65,7 @@ Setoids and setoid morphisms form a category that we call \(\setoids\).
[ f , g ] (i₁ x) = f x
[ f , g ] (i₂ x) = g x
\end{minted}
Similarly to products, the coproduct setoid is denoted \((A + B, \overset{+}{=})\) or just \(A + B\), where equality of coproducts is defined in the canonical way.
\item \textbf{Initial Object}:
\begin{minted}{agda}
data ⊥ {l} : Set l where
@ -69,31 +73,31 @@ Setoids and setoid morphisms form a category that we call \(\setoids\).
¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
¡ ()
\end{minted}
The initial setoid is then \((\bot, \emptyset)\), where the equivalence is the empty relation.
\end{itemize}
Lastly we need to show that the canonical distributivity morphism is an iso. Recall that the canonical distributive morphism is defined as \(dstl^{-1} = [ id \times i_1 , id \times i_2 ] : A \times B + A \times C \rightarrow A \times (B + C)\). This corresponds to the following definition using pattern matching:
Lastly we need to show that the canonical distributivity function is an iso. Recall that the canonical distributivity function is defined as \(dstl^{-1} = [ id \times i_1 , id \times i_2 ] : A \times B + A \times C \rightarrow A \times (B + C)\). This is equivalent to the following definition that uses pattern matching.
\begin{minted}{agda}
distributeˡ⁻¹ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ (A × B) + (A × C) → A × (B + C)
distributeˡ⁻¹ (i₁ (x , y)) = (x , i₁ y)
distributeˡ⁻¹ (i₂ (x , y)) = (x , i₂ y)
\end{minted}
The inverse can be defined similarly:
The inverse can then be defined similarly:
\begin{minted}{agda}
distributeˡ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ A × (B + C) → (A × B) + (A × C)
distributeˡ (x , i₁ y) = i₁ (x , y)
distributeˡ (x , i₂ y) = i₂ (x , y)
\end{minted}
Then these functions are inverse by definition, and it is easy to show that they are setoid morphisms.
Note that these functions are inverse by definition, and it is easy to show that they are setoid functions.
\end{proof}
\begin{lemma}
\(\setoids\) is Cartesian closed.
\end{lemma}
\begin{proof}
We have already shown that \(\setoids\) is Cartesian, we need to show that given two setoids \((A, =^A), (B, =^B)\) we can construct an exponential object.
Indeed, take the function space setoid \((A \rightarrow B, \doteq)\) where \(\doteq\) is point wise equality of setoid morphisms i.e. \(f , g : A \rightarrow B\) are point wise equal \(f \doteq g\) \textit{iff} \(f x =^B g x\) for any \(x : A\). \(curry\) and \(eval\) are then defined as expected.
Let \(A\) and \(B\) be two setoids. The function space setoid \(A \leadsto B\) is an exponential object of \(A\) and \(B\), together with the functions \(curry\) and \(eval\) defined in the following listing.
\begin{minted}{agda}
curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ (C × A → B) → C → A → B
@ -102,6 +106,7 @@ Setoids and setoid morphisms form a category that we call \(\setoids\).
eval : ∀ {a b} {A : Set a} {B : Set b} → ((A → B) × A) → B
eval (f , x) = f x
\end{minted}
The universal property of exponential objects follows instantly.
\end{proof}
\section{Quotienting the Delay Monad}
@ -110,111 +115,95 @@ Setoids and setoid morphisms form a category that we call \(\setoids\).
% Historically proof assistants like Agda and Coq have been offering multiple ways of defining coinductive types, nowadays the manuals of both Agda and Coq advise users to use coinductive records instead of defining coinductive types by constructors, we will heed this advice.
% Since the delay monad is usually defined by the constructors \(now\) and \(later\)
In this section we will introduce data types only using inference rules. For that we adopt the convention that coinductive types are introduced by doubled lines while inductive types are introduced with a single line.
Recall from previous chapters that Capretta's delay monad~\cite{delay} is a coinductive type defined by the two constructors:
Now, recall from previous chapters that Capretta's delay monad~\cite{delay} is a coinductive type defined by the two constructors:
\[
\mprset{fraction={===}}\inferrule*{x : A}{now\; x : Delay \;A} \qquad
\inferrule*{x : Delay \;A}{later \;x : Delay\; A} \qquad
\mprset{fraction={===}}\inferrule*{x : A}{now\; x : D\;A} \qquad
\inferrule*{x : D\;A}{later \;x : D\;A} \qquad
\]
Furthermore, let us now recall two notions of equality between inhabitants of the delay type that have been introduced in~\cite{delay}. Afterwards, we will state some facts that have been proven in~\cite{quotienting} to then finally prove that the quotiented delay type extends to an instance of the monad \(\mathbf{K}\) that has been introduced in \autoref{chp:iteration}.
Furthermore, let us now recall two notions of equality between inhabitants of the \(Delay\) type that have been introduced in~\cite{delay}. Afterwards, we will state some facts that have been proven in~\cite{quotienting} to then finally prove that the quotiented \(Delay\) type extends to an instance of \(\mathbf{K}\).
Given a setoid \((A , \overset{A}{=})\), the equivalence relation that is received by lifting \(\overset{A}{=}\) to \(Delay\;A\) is called \emph{strong bisimilarity}, it is defined by the rules
Let \(A\) be a setoid. Lifting the equivalence \(\overset{A}{=}\) to \(D\;A\) yields another equivalence called \emph{strong bisimilarity}. This equivalence is defined by the following rules.
\[
\mprset{fraction={===}}\inferrule*{eq : x =^A y}{now \;eq : x \sim y} \qquad
\inferrule*{eq : force \;x \sim force\; y}{later\;eq : later\; x \sim later\; y} \qquad
\mprset{fraction={===}}\inferrule*{x \overset{A}{=} y}{x \sim y} \qquad
\inferrule*{x \sim y}{later\; x \sim later\; y} \qquad
\]
\begin{proposition}[\cite{quotienting}]
\((Delay\;A, \sim)\) is a setoid.
\((D\;A, \sim)\) is a setoid and admits a monad structure.
\end{proposition}
\begin{proposition}[\cite{quotienting}]
\((Delay\;A, \sim)\) is a setoid.
\end{proposition}
In \((Delay\;A, \sim)\) computations that evaluate to the same result are not identified if their computation times differ. In many contexts this behavior is too intensional. Instead, we will now consider the quotient of this setoid, where all computations that evaluate to the same result are identified. Let us first define a relation that states that two computations evaluate to the same result
% In \((Delay\;A, \sim)\) computations that evaluate to the same result but in a different amount of time are not equal. We will now build the quotient of this type by weak bisimilarity, i.e. we will identify all computations that terminate with the same result. Let us first consider what it means for a computation to evaluate to some result:
Computations in \((D\;A, \sim)\) are only identified if they evaluate to the same result in the same amount of steps. In many contexts this behavior is too intensional. Instead, we will now consider the quotient of this setoid, where all computations that evaluate to the same result are identified. Let us first define a relation that states that two computations evaluate to the same result
\[
\inferrule*{eq : x =^A y}{now\; eq : now\;x \downarrow y} \qquad
\inferrule*{d : force\;x \downarrow c}{later\;d : later\;x \downarrow c }
\inferrule*{x \overset{A}{=} y}{now\;x \downarrow y} \qquad
\inferrule*{x \downarrow c}{later\;x \downarrow c }.
\]
Now, we call two computations \(p\) and \(q\) \emph{weakly bisimilar} or \(p \approx q\) if they evaluate to the same result, or don't evaluate at all, which is specified by these rules
Now, we call two computations \(p\) and \(q\) \emph{weakly bisimilar} or \(p \approx q\) if they evaluate to the same result, or don't evaluate at all, which is specified by the rules
\[
\mprset{fraction={===}}\inferrule*{eq : a =^A b \\ xa : x \downarrow a \\ yb : y \downarrow b}{\downarrow\approx \; eq \; xa \; yb : x \approx y} \qquad
\inferrule*{eq : force \;x \approx force \;y}{later\;eq : later \;x \approx later \;y} \qquad
\mprset{fraction={===}}\inferrule*{a \overset{A}{=} b \\ x \downarrow a \\ y \downarrow b}{x \approx y} \qquad
\inferrule*{x \approx y}{later \;x \approx later \;y} \qquad
\]
\begin{proposition}[\cite{delay}]
\((Delay\;A, \approx)\) is a setoid.
\end{proposition}
\begin{proposition}[\cite{delay}]
\((Delay\;A, \approx)\) is a monad.
\((D\;A, \approx)\) is a setoid and admits a monad structure.
\end{proposition}
\begin{proof}
The monad unit is the constructor \texttt{now} and the multiplication can be defined as follows:
The monad unit is the constructor \(now : A \rightarrow D\;A\) and the multiplication \(\mu : D\;D\;A \rightarrow D\;A\) can be defined as follows:
\[\mu\;x = \begin{cases}
z & \text{if } x = now\;z \\
later(\mu\;z) & \text{if } x = later\;z
\end{cases}\]
The monad laws have already been proven in~\cite{quotienting} and in our own formalization, so we will not reiterate the proofs here.
It has been shown in~\cite{delay} that this indeed a monad.
\end{proof}
For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\) and \(\dbtilde{D}\;A = (D_A, \approx)\).
\begin{lemma}\label{lem:Delgot}
Every \((Delay\;A , \approx)\) can be equipped with an Elgot algebra structure.
Every \(\dbtilde{D}\;A\) can be equipped with an Elgot algebra structure.
\end{lemma}
\begin{proof}
We need to show that for every setoid \((A, =^A)\) the resulting setoid \((Delay\;A, \approx)\) can be extended to an Elgot algebra.
We need to show that for every setoid \(A\) the resulting setoid \(\dbtilde{D}\;A\) can be extended to an Elgot algebra.
Let \((X , \overset{X}{=}) \in \obj{\setoids}\) and \(f : X \rightarrow Delay\; A + X\) be a setoid morphism, we define \(f^\sharp : X \rightarrow Delay\;A\) point wise:
Let \(X\) be a setoid and \(f : X \leadsto \dbtilde{D}\;A + X\) be a setoid function, we define \(f^\sharp : X \leadsto \dbtilde{D}\;A\) point wise:
\[
f^\sharp (x) :=
f^\sharp\;x :=
\begin{cases}
a & \text{if } f\;x = i_1 (a) \\
later\;(f^{\sharp} a) & \text{if } f\;x = i_2 (a)
a & \text{if } f\;x = i_1 (a) \\
later\;(f^{\sharp}\;a) & \text{if } f\;x = i_2 (a)
\end{cases}
\]
Let us first show that \(f^\sharp\) is a setoid morphism, i.e.\ given \(x, y : X\) with \(x \overset{X}{=} y\), we need to show that \(f^\sharp(x) = f^\sharp(y)\). Since \(f\) is a setoid morphism we know that \(f(x) \overset{+}{=} f(y)\) in the coproduct setoid \((Delay\;A + X, \overset{+}{=})\). We proceed by case distinction on \(f(x)\):
\begin{mycase}
\case{} \(f(x) = i_1 (a)\)
\[f^\sharp (x) = a = f^\sharp(y)\]
\case{} \(f(x) = i_2 (a)\)
\[f^\sharp (x) = later (f^{\sharp}(a)) = f^\sharp (y)\]
\end{mycase}
Let us first verify that \(f^\sharp\) is indeed a setoid function, i.e.\ given \(x, y : X\) with \(x \overset{X}{=} y\), we need to show that \(f^\sharp\;x \approx f^\sharp\;y\). Since \(f\) is a setoid function we know that \(f\;x \overset{+}{=} f\;y\), which already implies that \(f^\sharp\;x \approx f^\sharp\;y\) by the definition of \(f^\sharp\). Note that by the same argument we can define an iteration operator that respects strong bisimilarity, let us call it \(f^{\tilde{\sharp}}\) as we will later need to distinguish between \(f^\sharp\) and \(f^{\tilde{\sharp}}\).
Next, we check the iteration laws:
\begin{itemize}
\item \ref{law:fixpoint}: We need to show that \(f^\sharp (x) \approx ([ id , f^\sharp ] \circ f)(x)\) for any \(x : X\). Let us proceed by case distinction:
\item \ref{law:fixpoint}: We need to show that \(f^\sharp \;x \approx [ id , f^\sharp ](f\;x)\) for any \(x : X\). Let us proceed by case distinction: % chktex 2
\begin{mycase}
\case{} \(f(x) = i_1 (a)\)
\[ f^\sharp(x) \approx a \approx [ id , f^\sharp ] (i_1 (a)) \approx ([ id , f^\sharp ] \circ f) (x) \]
\case{} \(f(x) = i_2 (a)\)
\[ f^\sharp(x) \approx later (f^{\sharp}(a)) \approx f^\sharp(a) \approx [ id , f^\sharp ] (i_2 (a)) \approx ([ id , f^\sharp ] \circ f) (x)\]
\case{} \(f\;x = i_1\;a\)
\[ f^\sharp\;x \approx a \approx [ id , f^\sharp ] (i_1\;a) \approx [ id , f^\sharp ] (f\;x) \]
\case{} \(f\;x = i_2\;a\)
\[ f^\sharp\;x \approx later (f^{\sharp}\;a) \approx f^\sharp\;a \approx [ id , f^\sharp ] (i_2 \;a) \approx [ id , f^\sharp ] (f\;x)\]
\end{mycase}
\item \ref{law:uniformity}: Let \((Y , =^Y) \in \obj{\setoids}\) and \(g : Y \rightarrow Delay\; A + Y, h : X \rightarrow Y\) be setoid morphisms, where \((id + h) \circ f = g \circ h\). We need to show that \(f^\sharp\;x = g^\sharp(h\;x)\), for any \(x : X\). Let us proceed by case distinction over \(f\;x\) and \(g (h\;x)\), note that by the requisite equation \((id + h) \circ f = g \circ h\), we only need to consider two cases:
\item \ref{law:uniformity}: Let \(Y\) be a setoid and \(g : Y \leadsto \dbtilde{D}\;A + Y, h : X \leadsto Y\) be setoid functions, such that \((id + h) \circ f \doteq g \circ h\). We need to show that \(f^\sharp\;x \approx g^\sharp(h\;x)\), for any \(x : X\). Let us proceed by case distinction over \(f\;x\) and \(g (h\;x)\), note that by the requisite equation \((id + h) \circ f \doteq g \circ h\), we only need to consider two cases: % chktex 2
\begin{mycase}
\case{} \(f\;x = i_1\;a\) and \(g (h\;x) = i_1\;b\)\\
Consider that \((id + h) \circ f = g \circ h\) on \(x\) yields \(i_1 \; a = i_1 \; b\) and thus \(a \approx b\). Then indeed,
Consider that \((id + h) \circ f \doteq g \circ h\) on \(x\) yields \(i_1 \; a \overset{+}{=} i_1 \; b\) and thus \(a \approx b\). Then indeed,
\[f^\sharp\; x \approx a \approx b \approx g^\sharp (h\;x)\]
\case{} \(f\;x = i_2\;a\) and \(g (h\;x) = i_2\;b\)\\
Note that \((id + h) \circ f = g \circ h\) on \(x\) yields \(i_2(h\;a) = i_2\;b\) and thus \(h\;a = b\).
We need to show that
\[f^\sharp\;x = later(f^\sharp\;a) = later(g^\sharp(h\;a)) = later(g^\sharp\;b) = g^\sharp (h\;x),\]
which indeed follows by coinduction.
Note that \((id + h) \circ f \doteq g \circ h\) on \(x\) yields \(i_2(h\;a) \overset{+}{=} i_2\;b\) and thus \(h\;a \overset{Y}{=} b\).
We are done by coinduction, which yields
\[f^\sharp\;x \approx later(f^\sharp\;a) \approx later(g^\sharp(h\;a)) \approx later(g^\sharp\;b) \approx g^\sharp (h\;x).\]
\end{mycase}
\item \ref{law:folding}: Let \((Y , =^Y) \in \obj{\setoids}\) and \(h : Y \rightarrow X + Y\), we need to show that \({(f^\sharp + h)}^\sharp\;z = {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp\;z\) for any \(z : X + Y\).
\item \ref{law:folding}: Let \(Y\) be a setoid and \(h : Y \leadsto X + Y\) a setoid function, we need to show that \({(f^\sharp + h)}^\sharp\;z \approx {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp\;z\) for any \(z : X + Y\). % chktex 2
Let us first establish the following fact
\[f^\sharp\;c = {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c) \qquad \text{for any } c : X, \tag{*}\label{folding-helper}\]
\[f^\sharp\;c \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c) \qquad \text{for any } c : X, \tag{*}\label{folding-helper}\]
which follows by case distinction on \(f\;c\) and coinduction:
\begin{mycase}
\case{} \(f\;c = i_1\;a\)
@ -222,19 +211,19 @@ Now, we call two computations \(p\) and \(q\) \emph{weakly bisimilar} or \(p \ap
\case{} \(f\;c = i_2\;a\)
\[f^\sharp\;c \approx later(f^\sharp\;a) \approx later({[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;a)) \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c)\]
\end{mycase}
Thus, we are done. Let us now proceed with the proof of \ref{law:folding}, by case distinction on \(z\):
Thus, we are done. Let us now proceed with the proof of \ref{law:folding}, by case distinction on \(z\): % chktex 2
\begin{mycase}
\case{} \(z = i_1\;x\)\\
Another case distinction on \(f\;x\) yields:
\subcase{} \(f\;x = i_1\;a\)\\
We are done, since \({(f^\sharp + h)}^\sharp(i_1 \; x) = i_1\;a = (id + i_1) (f\;x) = {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;x)\)
We are done, since \({(f^\sharp + h)}^\sharp(i_1 \; x) \approx a \approx {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;x)\)
\subcase{} \(f\;x = i_2\;a\)\\
This concludes the first case, since:
Now, using the fact we established prior
\begin{alignat*}{1}
& {(f^\sharp + h)}^\sharp(i_1 \; x)
\\=\;&later(f^\sharp\;a)
\\=\;&later({[(id + i_1) \circ f , i_2 \circ h]}^\sharp (i_1\;a))\tag{\ref{folding-helper}}
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;x).
\\\approx\;&later(f^\sharp\;a)
\\\approx\;&later({[(id + i_1) \circ f , i_2 \circ h]}^\sharp (i_1\;a))\tag{\ref{folding-helper}}
\\\approx\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;x).
\end{alignat*}
\case{} \(z = i_2\;y\)\\
Let us proceed by discriminating on \(h\;y\).
@ -242,47 +231,203 @@ Now, we call two computations \(p\) and \(q\) \emph{weakly bisimilar} or \(p \ap
Indeed by coinduction,
\begin{alignat*}{1}
& {(f^\sharp + h)}^\sharp(i_2 \; y)
\\=\;&later((f^\sharp + h)(i_1\;a))
\\=\;&later({[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;a))
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;y)
\\\approx\;&later((f^\sharp + h)(i_1\;a))
\\\approx\;&later({[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;a))
\\\approx\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;y)
\end{alignat*}
\subcase{} \(h\;y = i_2\;a\)\\
Similarly by coinduction,
\begin{alignat*}{1}
& {(f^\sharp + h)}^\sharp(i_2 \; y)
\\=\;&later((f^\sharp + h)(i_2\;a))
\\=\;&later({[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;a))
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;y)
\\\approx\;&later((f^\sharp + h)(i_2\;a))
\\\approx\;&later({[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;a))
\\\approx\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;y)
\end{alignat*}
\end{mycase}
\end{itemize}
This concludes the proof that every \((Delay\;A,\approx)\) can be extended to an Elgot algebra.
This concludes the proof that every \(\dbtilde{D}\;A\) can be extended to an Elgot algebra.
\end{proof}
\todo[inline]{Discretization corollary here}
In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a setoid \(Z\), we can discretize \(Z\) by replacing the equivalence relation with propositional equality, yielding \(\disc{Z} := (Z, \equiv)\). Now, the following corollary describes how to transform an iteration on \(\dbtilde{D}\;A\) into an iteration on \(\tilde{D}\;A\).
\begin{corollary}\label{cor:discretize}
Given a setoid function \(g : X \rightarrow \dbtilde{D}\;A + X\). There exists a setoid function \(\bar{g} : \disc{X} \rightarrow \tilde{D}\;A + \disc{X}\) such that \(g^\sharp\;x \sim \bar{g}^\sharp\;x\) for any \(x : X\).
\end{corollary}
\begin{proof}
It is clear that propositional equality implies strong bisimilarity and thus \(\bar{g}\) is a setoid function that behaves as \(g\) does but with a different type profile.
The requisite property follows by case distinction on \(g\;x\).
\begin{mycase}
\case{} \(g\;x = i_1\;a\)\\
We are done, since \(g^\sharp\;x \sim a \sim \bar{g}^\sharp\;x\)
\case{} \(g\;x = i_2\;a\)\\
By coinduction \(g^\sharp\;x \sim later(g^\sharp\;a) \sim later(\bar{g}^\sharp\;a) \sim \bar{g}^\sharp\;x\), which concludes the proof.
\qedhere
\end{mycase}
\end{proof}
\begin{theorem}\label{thm:Dfreeelgot}
Every \((Delay\;A , \approx)\) can be equipped with a free Elgot algebra structure.
Every \(\dbtilde{D}\;A\) can be equipped with a free Elgot algebra structure.
\end{theorem}
\begin{proof}
We build on \autoref{lem:Delgot}, it thus suffices to show that the induced Elgot algebras are free.
Given an Elgot algebra \((B , \overset{B}{=}, {(-)}^{\sharp_b})\) and a setoid morphism \(f : A \rightarrow B\). We need to define an Elgot algebra morphism \(\free{f} : Delay\;A \rightarrow B\). Consider \(g : Delay\;A \rightarrow B + Delay\;A\) defined by
We build on \autoref{lem:Delgot}, it thus suffices to show that for any setoid \(A\), the Elgot algebra \((\dbtilde{D}\;A, {(-)}^\sharp)\) together with the setoid function \(now : A \leadsto \dbtilde{D}\;A\) is a free such algebra.
Given an Elgot algebra \((B, {(-)}^{\sharp_b})\) and a setoid function \(f : A \leadsto B\). We need to define an Elgot algebra function \(\free{f} : \dbtilde{D}\;A \leadsto B\). Consider \(g : \tilde{D}\;A \leadsto B + \tilde{D}\;A\) defined by
\[g\;x =
\begin{cases}
i_1(f\;a) & \text{if } x = now\;a \\
i_2\;a & \text{if } x = later\;a
\end{cases}\]
\(g\) is trivially a setoid morphism with respect to strong bisimilarity, we can thus take \(\free{f} = g^{\sharp_b} : Delay\;A \rightarrow B\). Next, we need to show that \(g^{\sharp_b}\) is a setoid morphism with respect to weak bisimilarity.
\(g\) trivially respects strong bisimilarity, thus consider \(g^{\sharp_b} : \tilde{D}\;A \leadsto B\). We need to show that \(g^{\sharp_b}\) also respects weak bisimilarity, thus yielding the requisite function \(\free{f} = g^{\sharp_b} : \dbtilde{D}\;A \leadsto B\). However, the proof turns out to be rather complex, let us postpone it to~\autoref{cor:respects}
Let us now show that \(g^{\sharp_b}\) is iteration preserving. Given a setoid function \(h : X \leadsto \dbtilde{D}\;A + X\), we need to show that \(g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x\) for any \(x : X\).
Let us now show that \(g^{\sharp_b}\) is iteration preserving. Given a setoid morphism \(h : X \rightarrow Delay\;A + X\) with respect to weak bisimilarity, we need to show that \(g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x\) for any \(x : X\).
Using \autoref{cor:discretize} we will proceed to show
\[g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\]
We will first need to introduce the notion of discretized setoid. Given a setoid \((Z, \overset{Z}{=})\) the discretized setoid is defined as \(\disc{Z} := (Z , \equiv)\). Given a setoid morphism \(u : (Z, \overset{Z}{=}) \rightarrow (A, \approx) + (Z, \overset{Z}{=})\), we can define its discretized version \(\bar{u} : \disc{Z} \rightarrow (A, \sim) + \disc{Z}\) which is a setoid morphism with respect to strong bisimilarity. Now, the following will be key for proving preservation:
\[u^\sharp\;x \sim \bar{u}^\sharp\;x \qquad \text{ for any } x : X,\]
which follows by coinduction and case distinction on \(u\;x\).
The second step instantly follows by \ref{law:uniformity}, considering that the identity function easily extends to a setoid function \(id : \disc{X} \leadsto X\), and thus \({((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}(id\;x)\). % chktex 2
For the first step consider
\begin{alignat*}{1}
& g^{\sharp_b} (h^\sharp\;x)
\\\overset{B}{=}\;&g^{\sharp_b} (\bar{h}^\sharp\;x)\tag{\autoref{cor:discretize}}
\\\overset{B}{=}\;&(g^{\sharp_b} \circ [ id , \bar{h}^\sharp])(i_2\;x)
\\\overset{B}{=}\;&{([(id + i_1) \circ g , i_2 \circ i_2 ] \circ [i_1 , h])}^{\sharp_b} (i_2\;x)\tag{\ref{law:uniformity}}
\\\overset{B}{=}\;&{((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\tag{\ref{law:compositionality}}
\end{alignat*}
Now, we can continue with the proof of preservation. We will proceed by showing that
\[g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x\]
Thus, \(g^{\sharp_b}\) is an Elgot algebra function. We are left to check that \(g^{\sharp_b}\) satisfies the requisite properties of free objects. First, note that \(g^{\sharp_b} \circ now \doteq [ id , g^\sharp_b ] \circ g \circ now \doteq f\) by \ref{law:fixpoint} and the definition of \(g\). % chktex 2
Next, we need to check uniqueness of \(g^{\sharp_b}\). It suffices to show that any two Elgot algebra functions \(e, h : \dbtilde{D}\;A \leadsto B\) satisfying \(e \circ now \doteq f\) and \(h \circ now \doteq f\) are equal.
First, note that the identity function can be extended to the following conversion setoid function \(conv : \tilde{D}\;A \leadsto \dbtilde{D}\;A\), since strong bisimilarity implies weak bisimilarity. Furthermore, consider the setoid function \(o : \tilde{D}\;A \leadsto \tilde{D}\;A + \tilde{D}\;A\) defined by
\[o\;x := \begin{cases}
i_1(now\;z) & \text{if } x = now\;z \\
i_2\;z & \text{if } x = later\;z
\end{cases}\]
Now, by coinduction we can easily follow that
\[x \approx {((conv + id) \circ o)}^\sharp\;x \qquad \text{for any } x : D\;A.\tag{\(\Asterisk\)}\label{uniq-helper}\]
Let us now return to the proof of uniqueness. We proceed by
\begin{alignat*}{1}
& e\;x
\\\approx\;&e({((conv + id) \circ o)}^\sharp\;x)\tag{\ref{uniq-helper}}
\\\approx\;&{((e \circ conv + id) \circ o)}^{\sharp_b}\;x\tag{Preservation}
\\\approx\;&{((h \circ conv + id) \circ o)}^{\sharp_b}\;x
\\\approx\;&h({((conv + id) \circ o)}^\sharp\;x)\tag{Preservation}
\\\approx\;&h\;x.\tag{\ref{uniq-helper}}
\end{alignat*}
It thus suffices to show that \((e \circ conv + id)(o\;x) \approx (h \circ conv + id)(o\;x)\). Indeed, discriminating over \(x\) yields:
\begin{mycase}
\case{} \(x = now\;z\)
\begin{alignat*}{1}
& (e \circ conv + id)(o(now\;z))
\\\overset{+}{=}\;&(e \circ conv + id)(i_1(now\;z))
\\\overset{+}{=}\;&e(now\;z)
\\\overset{+}{=}\;&f\;z
\\\overset{+}{=}\;&h(now\;z)
\\\overset{+}{=}\;&(h \circ conv + id)(i_1(now\;z))
\\\overset{+}{=}\;&(h \circ conv + id)(o(now\;z))
\end{alignat*}
\case{} \(x = later\;z\)
\begin{alignat*}{1}
& (e \circ conv + id)(o(later\;z))
\\\overset{+}{=}\;&(e \circ conv + id)(i_2\;z)
\\\overset{+}{=}\;&i_2\;z
\\\overset{+}{=}\;&(h \circ conv + id)(i_2\;z)
\\\overset{+}{=}\;&(h \circ conv + id)(o(later\;z))
\end{alignat*}
\end{mycase}
It has thus been proven that every \(\dbtilde{D}\;A\) admits a free Elgot algebra structure.
\end{proof}
Let us now establish some functions for inspecting and manipulating the computation of elements of \(D\;A\). These functions and some key facts will then be used to finish the remaining proof of \autoref{thm:Dfreeelgot}.
First, consider the ordering with respect to execution time on elements of \(D\;A\), defined by
\[
\mprset{fraction={===}}\inferrule*{p: x \downarrow a}{now_\lesssim\;p : now\;a \lesssim x} \qquad
\inferrule*{p : x \lesssim y}{later_\lesssim\;p : later\;x \lesssim later\;y}.
\]
Note that \(x \lesssim y\) implies \(x \approx y\) for any \(x, y : D\;A\), which follows easily by coinduction.
Now, consider the following function \(race : D\;A \rightarrow D\;A \rightarrow D\;A\) which tries running two computations and returns the one that finished first:
\[race\;p\;q := \begin{cases}
now\;a & \text{if } p = now\;a \\
now\;b & \text{if } p = later\;a \text{ and } q = now\;b \\
later\;(race\;a\;b) & \text{if } p = later\;a \text{ and } q = later\;b
\end{cases}\]
The following Corollary, whose proof can be found in the formalization, will be crucial.
\begin{corollary}\label{cor:race}
\(race\) satisfies the following properties:
\begin{alignat*}{3}
& x \approx y & & \text{ implies } race\;x\;y \sim race\;y\;x & \text{ for any } x, y : D\;a
\\ &x \approx y && \text{ implies } race\;x\;y \lesssim y &\text{ for any } x, y : D\;A.
\end{alignat*}
\end{corollary}
Next, let us consider functions for counting steps of computations, first regard \(\Delta_0 : (x : D\;A) \rightarrow (a : A) \rightarrow (x \downarrow a) \rightarrow \mathbb{N}\), which returns the number of steps a terminating computation has to take and is defined by
\[\Delta_0\;x\;a\;p := \begin{cases}
0 & \text{if } x = now\;y \\
(\Delta_0\; y\;a\;q) + 1 & \text{if } x = later\;y \text{ and } p = later_\downarrow q
\end{cases}\]
Similarly, consider \(\Delta : (x, y : D\;A) \rightarrow x \lesssim y \rightarrow D(A \times \mathbb{N})\) defined by
\[\Delta\;x\;y\;p := \begin{cases}
now(a , \Delta_0\;x\;a\;q) & \text{if } x = now\;a \text{ and } p = now_\lesssim q \\
later(\Delta\;a\;b\;q) & \text{if } x = later\;a, y = later\;b \text{ and } p = later_\lesssim q
\end{cases}\]
Lastly, consider the function \(\iota : A \times \mathbb{N} \rightarrow D\;A\), which adds a number of \(later\) in front of a value and is given by
\[\iota\;(a, n) := \begin{cases}
now\;x & \text{if } n = 0 \\
later(\iota\;(a, m)) & \text{if } n = m + 1
\end{cases}\]
Trivially, \(\iota\) can be extended to a setoid function \(\iota : A \times \mathbb{N} \leadsto \tilde{D}\;A\), where the equivalence on \(\mathbb{N}\) is propositional equality. Let us state two facts about \(\Delta\), the proof can again be found in the formalization.
\begin{corollary}\label{cor:delta}
\(\Delta\) satisfies the following properties:
\begin{alignat*}{4}
& p : x \lesssim y & & \text{ implies } \tilde{D}(fst (\Delta\;x\;y\;p))\; & \sim x & & \text{ for any } x, y : D\;A\tag{\(\Delta_1\)}\label{delta1} \\
& p : x \lesssim y & & \text{ implies } \iota^* (\Delta\;x\;y\;p) & \sim y & & \text{ for any } x, y : D\;A.\tag{\(\Delta_2\)}\label{delta2}
\end{alignat*}
\end{corollary}
Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
\begin{corollary}\label{cor:respects}
The setoid function \(g^{\sharp_b} : \tilde{D}\;A \leadsto B\) defined in \autoref{thm:Dfreeelgot} respects weak bisimilarity, thus yielding \(\free{f} = g^{\sharp_b} : \dbtilde{D}\;A \leadsto B\).
\end{corollary}
\begin{proof}
Let \(x, y : D\;A\) such that \(x \approx y\). Recall that by \autoref{cor:race} \(x \approx y\) implies \(p: race\;x\;y \lesssim y\) and symmetrically \(q: race\;y\;x \lesssim x\), now, using Corollaries~\ref{cor:race} and~\ref{cor:delta}:
\begin{alignat*}{1}
& g^{\sharp_b}\;x
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*(\Delta\;(race\;y\;x)\;x\;q))\tag{\ref{delta2}}
\\\overset{B}{=}\;&g^{\sharp_b}(\tilde{D}fst(\Delta\;(race\;y\;x)\;x\;q))\tag{\ref{respects-key-helper}}
\\\overset{B}{=}\;&g^{\sharp_b}(race\;y\;x)\tag{\ref{delta1}}
\\\overset{B}{=}\;&g^{\sharp_b}(race\;x\;y)\tag{\autoref{cor:race}}
\\\overset{B}{=}\;&g^{\sharp_b}(\tilde{D}fst(\Delta\;(race\;x\;y)\;y\;p))\tag{\ref{delta1}}
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*(\Delta\;(race\;x\;y)\;y\;p))\tag{\ref{respects-key-helper}}
\\\overset{B}{=}\;&g^{\sharp_b}\;y.\tag{\ref{delta2}}
\end{alignat*}
We have thus reduced the proof to showing that
\[g^{\sharp_b} (\tilde{D}fst\;z) \overset{B}{=} g^{\sharp_b}(\iota^*\;z) \text{ for any } z : D(A \times \mathbb{N}). \tag{*}\label{respects-key-helper}\]
Let us proceed as follows
\begin{alignat*}{1}
& g^{\sharp_b} (\tilde{D}fst\;z)
\\\overset{B}{=}\;&g_1^{\sharp_b}\tag{\ref{law:uniformity}}
\\\overset{B}{=}\;&g_2^{\sharp_b}
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*\;z). \tag{\ref{law:uniformity}}
\end{alignat*}
Now, we are left to find suitable \(g_1, g_2 : \tilde{D}(A \times \mathbb{N}) \leadsto B + (\tilde{D} (A \times \mathbb{N}))\). Consider,
\[g_1 p := \begin{cases}
i_1(f\;x) & \text{if } p = now\;(x, zero) \\
i_2(\tilde{D}o (\iota\;(x,n))) & \text{if } p = now\;(x, n + 1) \\
i_2\;(x,n) & \text{if } p = later\;(x, n)
\end{cases}\]
\end{proof}