From c8578f922a64912fc0fe76026b06fc3e4d437f7f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Mar 2019 16:28:33 +0100
Subject: [PATCH] mention the connection to ultrametric spaces
---
docs/algebra.tex | 2 ++
1 file changed, 2 insertions(+)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index c0bb43698..0903115ef 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -17,6 +17,8 @@ This definition varies slightly from the original one in~\cite{catlogic}.
The key intuition behind OFEs is that elements $x$ and $y$ are $n$-equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps.
In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{ofe-mono})---and in the limit, it agrees with plain equality (\ruleref{ofe-limit}).
+Notice that OFEs are just a different presentation of bisected 1-bounded ultrametric spaces, where the family of equivalence relations gives rise to the distance function (two elements that are equal for $n$ steps are no more than $2^{-n}$ apart).
+
\begin{defn}
An element $x \in \ofe$ of an OFE is called \emph{discrete} if
\[ \All y \in \ofe. x \nequiv{0} y \Ra x = y\]
--
GitLab