# Applications of metric structures on posets/lattices in theoryCS

Since the term is overloaded, a brief definition first. A poset is a set $X$ endowed with a partial order $\le$. Given two elements $a,b \in X$, we can define $x \vee y$ (join) as their least upper bound in $X$, and similarly define $x \wedge y$ (meet)(join)as a greatest lower bound.

A lattice is a poset in which any two elements have a unique meet and a unique join.

Lattices (in this form) show up in theoryCS in (briefly) the theory of submodularity (with the subset lattice) and clustering (the partition lattice), as well as in domain theory (which I don't understand too well) and static analysis.

But I'm interested in applications which use metric structures on lattices. A simple example comes from clustering, where any antimonotone submodular function $f : X \rightarrow R$ (antimonotone means that if $x \le y, f(x) \le f(y)$) induces a metric $$d(x,y) = 2f(x \wedge y) - f(x) - f(y)$$

This metric has been used extensively as a way to compare two different clusterings of a data set.

Are there other applications of lattices that care about metric structures ? I've been interested in the domain theory/static analysis application, but so far I've not seen any need for metrics.

First, a comment. Your question sort of depends on how geometrically you intend to mean the word "metric". It's reasonably common to use ultrametrics in semantics and static analysis, but ultrametrics tend to have a combinatorial rather than a geometric interpretation. (This is a variant of the observation that domain theory has the flavor of a combinatorial rather than geometric use of topology.)

That said, I'll give you an example of how this comes up in program proofs. First, recall that in a program proof, we want to show that a formula describing a program holds. In general, this formula does not necessarily have to be interpreted with the booleans, but can be drawn from the elements of some lattice of truth values. Then a true formula is just one which is equal to the top of the lattice.

Furthermore, when specifying very self-referential programs (for example, programs that make extensive use of self-modifying code) matters can get very difficult. We typically want to give a recursive specification of the program, but there might not be an obvious inductive structure upon which to hang the definition. To solve this problem, it's often helpful to equip the truth value lattice with extra metric structure. Then, if you can show that the predicate whose fixed point you want is strictly contractive, you can appeal to Banach's fixed point theorem to conclude that the recursive predicate you want is well-defined.

The case I am most familiar with is called "step-indexing". In this setting, we take our lattice $\Omega$ of truth values to be downwards-closed subsets of $\mathbb{N}$, whose elements we can loosely interpret as "the lengths of the evaluation sequences on which the property holds". Meets and joins are intersections and unions, as usual, and since the lattice is complete we can define the Heyting implication as well. The lattice can also be equipped with an ultrametric by letting the distance between two lattice elements be $2^{-n}$, where $n$ is the smallest element in one set but not the other.

Then, Banach's contraction map thoerem tells us that a contractive predicate $p : \Omega \to \Omega$ has a unique fixed point. Intuitively, this says that if we can define a predicate which holds for $n+1$ steps using a version which holds for $n$ steps, then we actually have an unambiguous definition of a predicate. If we then show that the predicate equals $\top = \mathbb{N}$, then we know that the predicate always holds of the program.

• ah interesting. In answer to your question, all I care about is that the metric is just that: it satisfies triangle inequality. So ultrametrics are perfectly fine. However, (and this is my shortcoming in the question) it seems to me that the use of the metric here is structural, so as to gain access to Banach. You don't care about the metric in an of itself (and so things like approximating the metric or computing it are irrelevant). Is that right ? Feb 3 '11 at 17:59
• Yes, we don't tend to care much about the metric. This is actually a source of discomfort with metric or step-indexed models -- why are we tracking information we don't really care about? Showing that a model was stable under a class of approximations to the metric (perhaps conservative with respect to contractiveness) would actually increase comfort with it. Feb 4 '11 at 10:08

As an alternative to the more commonly used CPOs, Arnold and Nivat explored (complete) metric spaces as domains of denotational semantics [1]. In his thesis Bonsangue [2] explored dualities between such denotational semantics and axiomatic semantics. I mention it here because it gives a very comprehensive overall picture.

[1]: A Arnold, M Nivat: Metric Interpretations of Infinite Trees and Semantics of non Deterministic Recursive Programs. Theor. Comput. Sci. 11: 181-205 (1980).
[2]: MM Bonsangue Topological Duality in Semantics volume 8 of ENTCS, Elsevier 1998.

• Fantastic -- I didn't know this thesis was online! Feb 4 '11 at 10:05
• I let Marcello (Bonsangue) know that he's being talked about. (Perhaps he'll join.) Feb 4 '11 at 12:14

Here's one (from, coincidentally, the top of my reading queue):

Swarat Chaudhuri, Sumit Gulwani and Roberto Lublinerman. Continuity Analysis of Programs. POPL 2010.

The authors give a denotational semantics for an imperative language with simple loops, interpreting expressions as functions from values in an underlying product metric space. The point is to determine which programs represent continuous functions, even in the presence of "if" and loops. They even allow questions about continuity restricted to certain inputs and outputs. (This is important for analyzing Dijkstra's algorithm, which is continuous in its path length, but not in the actual path.)

I haven't seen anything yet that requires a metric space - it seems it could have been done using general topology so far - but I'm only on page 3. :)

• of course there's no poset or lattice here, like in the previous answer. that's what I'm missing. Feb 4 '11 at 16:23

Apologies for adding another answer, but this one is unrelated to my other one above.

A metric spaces I routinely use to irritate (or is it educate?) students of concurrency is that of infinite traces. The topology it induces is precisely the one Alpern and Schneider [1] used to characterize safety and liveness properties as limit-closed and dense, respectively.

The distance between two traces is smaller if their common prefix is longer: $$\begin{array}{@{}rcl} d : \Sigma^\omega\times\Sigma^\omega & \longrightarrow & \mathbb{R}_{{}\ge 0}\\ % (\sigma,\tau) & \mapsto & 2^{-\sup \{~i\in\mathbb{N} ~|~ \sigma|_i = \tau|_i~\}} \end{array}$$ where $\sigma|_i$ denotes $\sigma$'s prefix of length $i$ and $2^{-\infty} = 0$.

In retrospect I realize that this answer also lacks the essential ingredient of a lattice or poset structure. Such a lattice structure is however present when moving one level up to what Clarkson and Schneider call hyperproperties [2]. At the time of writing it is unclear to me how to lift the metric though.

[1] B Alpern and FB Schneider. Defining liveness. IPL, 21(4):181–185, 1985.
[2] MR Clarkson and FB Schneider. Hyperproperties. CSF, p51-65, IEEE, 2008.

• Here we can type in LaTeX just like we normally do - put dollar signs around \sum_{k=1}^n k = \frac{k(k+1)}{2} and we will get $\sum_{k=1}^n k = {n(n+1)}/{2}$. See this meta post for more information. Feb 5 '11 at 8:53
• @HCH thanks, I've edited my post accordingly and removed the blatant cry for formatting advice.
– Kai
Feb 5 '11 at 10:50
• Nice formula! Feb 5 '11 at 12:31