Applications of metric structures on posets/lattices in theoryCS

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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. :)

Answer 4

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.