Cédric Dégremont
email: cedric.degremont@irit.fr

Antoine Venant
email: antoine.venant@irit.fr

Nicholas Asher
email: asher@irit.fr

Semantic Similarity: Foundations

Keywords: Semantics, Distance, Metric, Similarity, Lattice, Conversations

This paper investigates measures of semantic similarity between conversations from an axiomatic perspective. We abstract away from real conversations, representing them as sequences of formulas, equipped with a notion of semantic interpretation that maps them into a different space. An example we use to illustrate our approach is the language of propositional logic with its classical semantics. We introduce and study a range of different candidate properties for metrics on such conversations, for the structure of the semantic space, and for the behavior of the interpretation function, and their interactions. We define four different metrics and explore their properties in this setting.

Introduction

If linguistic behavior is to be analyzed as a form of rational behavior [START_REF] Grice | Logic and conversation[END_REF], it is important to be able to assess the conversational goals of linguistic agents and the extent to which they are fulfilled by any given conversation in a manageable way. Specifying preferences over the set of all possible choices of what to say is clearly intractable for us as theorists and for speakers as practioners. Instead, speakers must be able to group conversations into semantically similar classes and to assess the relative semantic proximity of any two pairs of conversations. The preferences of the agents over different ways of expressing themselves have to do with how close these ways are from satisfying certain positive or negative semantic goals. An elegant way to be able to do this, is to have a metric over conversations that is semantic in nature. The goal of this paper is to identify properties that characterize 'semantic metrics' and to identify reasonable axioms that can help us isolate well-behaved semantic metrics.

A workable definition of semantic distance between texts or conversations is also important for the evaluation of annotations of discourse structure in text and dialogue. It is also crucial to the success of the machine learning of semantic structures from annotated data, as all known algorithms rely on some notion of similarity or loss with respect to the target structure. While measures of syntactic similarity like ParseEval [START_REF] Black | A procedure for quantitatively comparing the syntactic coverage of english grammars[END_REF] and Leaf Ancestor [START_REF] Sampson | A proposal for improving the measurement of parse accuracy[END_REF] are well-understood and used in computational linguistics, they yield intuitively wrong results. ParseEval, for instance, places too much importance on the boundaries of discourse constituents, which are often notoriously hard even for expert annotators to agree on. Investigations of distances between semantic interpretations of a text are rarely examined. While a natural equivalence and ordering relation over contents comes from the underlying logic of formal semantic analysis, this only gives a very crude measure. Some have appealed to a language of semantic primitives to exploit the more developed measures of syntactic distance in a more semantic setting. But such an approach depends on the choice of semantic primitives, with no clear consensus on how to go about determining these primitives.

Semantic distances are also relevant in the context of formal theories of belief revision. [START_REF] Lehmann | Distance semantics for belief revision[END_REF] explores [START_REF] Alchourrón | On the logic of theory change: partial meet contraction and revision functions[END_REF] style postulates that characterize a wide family of belief revision operator based on pseudodistances on models satisfying only very mild assumptions. Our problem is also closely related to the problem of determining the distance of a scientific theory from the truth. This problem, referred to as the problem of verisimilitude or truthlikeness in philosophy of science (since Popper 1968), is arguably reducible to the problem of having a satisfactory concept of similarity between theories in a formal language.

The aim of this paper is to study semantic metrics for an abstract and simple concept of conversations. Syntactically, we assume that conversations are monoids with respect to concatenation. These conversations are equipped with an interpretation function mapping them into some distinct semantic space. In general, our assumptions about the semantic space and the interpretation function will be as minimal as possible. As far as identifying the axioms that characterize our concept of 'semanticity' for a metric goes, we will not be making any assumption. To analyze candidate axioms that characterize well-behaved semantic metrics, it will be interesting to consider the effect of assuming a bit more structure. Specifically we will pay some attention to the case in which the semantic co-domain of the interpretation function is a lattice. As an example, sequences of propositional formulas with their classical interpretation certainly fall under this category. We will moreover consider interpretation functions that satisfy some structural properties, for example assuming that the semantic meaning of a sequence is invariant under stuttering, that is immediate repetition of the same element in a sequence, or even assuming complete invariance under permutation.

To develop semantic metrics for conversations in natural language or for their representations in some formalism suitable for discourse interpretation (like for instance SDRT, [START_REF] Asher | Logics of Conversation[END_REF] we first need to clarify the space of reasonable axioms and metrics for the simplest and most general representations. We take this first step here.

The paper is organized as follows. We start with a first section, Sect. 2, that contains technical preliminaries and settles the notation. We then describe in Sect. 3 different properties that can be met by an interpretation function, regarding how it interacts with sequences-concatenation or the structure of the semantic space. Section 4 introduces some elementary background about generalized metrics and metrics over subsets of a metric space. Section 5 draws a map of different level of semanticity for metrics, corresponding to different requirements on the interaction between the interpretation function and the metric. Section 6 introduces some concrete candidate semantic metrics. Sections 6-8 then describe how these potential measures of semantic similarity fare with respect to different lists of axioms. We show that certain combinations of axioms lead to trivialization results. We then conclude.

Preliminaries and Notation

This section contains some technical preliminaries and settles notation. The reader can skip this section on a first reading, and come back to it when needed.

Sets, Functions, Sequences, Orders and Lattices

Let X, Y be two sets. We let X ⊖ Y denote the symmetric difference of X and Y . Let card(X) denote the cardinality of X. let X * be the set of finite strings over X.

If f : X → Y , we let f (X) and f [X] be alternative notation for the image of X under f , that is f (X) = f [X] = {f (x)|x ∈ X}. We let dom(f ) = X, target(f ) = Y and ran(f ) = f (X).
The kernel of f is the equivalence relation ∼, such that x ∼ y iff f (x) = f (y). We say that f is isotone whenever for all x, y with x ≤ y we have f (x) ≤ f (y). We write f : X → Y whenever f is partial function from X to Y , that is there exists a non-empty subset of A ⊆ Y such that f : A → Y .

Given a sequence σ ∈ X * we let len(σ) be the length of σ. If k ≤ len(σ) then we let σ| k , be the prefix of σ of length k, and we let σ(k) or σ[k] be the k th element of σ. We let ran(σ) be the range of σ, that is ran

(σ) = {σ[k]|1 ≤ k ≤ len(σ)}.
We let -→ ǫ be the empty sequence.

A relation ≤ on X is a pre-order on X iff it is a reflexive and transitive relation on X. (X, ≤) is a poset iff ≤ is a pre-order on X such that ≤ is antisymmetric on X, that is x ≤ y and y ≤ x, implies that x = y. A lattice (X, ≤) is a poset such that every two elements x, y ∈ X have a least upper bound (or join, denoted x ∧ y) and a greatest lower bound (or meet, denoted x ∨ y). A lattice (X, ≤) is bounded whenever X has a least and a greatest element (denoted ⊥ and ⊤).

Propositional Languages and Interpretation Functions

Given a language L we let ϕ, ψ, χ, ϕ 1 , ϕ 2 . . . range over L, and we let

-→ ϕ , -→ ψ , -→ σ , -→ τ , -→ υ , -→ σ 1 , -→ σ 2 .
. . range over L * . Given a finite set prop = {p 1 , . . . , p n } we let L prop (1) be defined as follows:

ϕ ::= p|¬p|⊤|⊥ where p ranges over prop. And we define L prop as follows:

ϕ ::= p|⊤|⊥|¬ϕ|ϕ ∧ ϕ|ϕ ∨ ϕ
where p ranges over prop. We define sig(ϕ):L → ℘(prop) where p ∈ sig(ϕ) iff p occurs in ϕ. Given a sequence -→ σ ∈ L * or a subset A ⊆ L, we write sig( -→ σ ) := ψ∈ran( - → σ ) sig(ψ) or sig(A) := ψ∈A sig(ψ), respectively.

Classical truth-functional interpretation of L prop . Let W prop = 2 prop . Depending on context, will treat a member V ∈ W prop either as a function V : prop → {0, 1} or as a subset V ⊆ prop. These two representations are of course equivalent. We let • t : L → 2 prop , be the classical truth-functional interpretation function of L prop (1) and L prop .

Properties of Interpretation Functions

In general, we will work with abstract concepts of a language and of an interpretation function. Let L, X be non-empty sets.

Definition 3.1 (Interpretation function). An interpretation function of L into X is a function • : L * → X.
An interpretation function for L is an interpretation function L into Y for some non-empty set Y.

Co-Domain

In this paper, we will sometimes assume that the semantic space has some structure. We are always explicit about these assumptions whenever we make them.

Definition 3.2. We say that • is (W, ≤)-pre-order-valued ((W, ≤)-posetvalued) whenever target( • )=W and (W, ≤) is a pre-order (respectively, a poset).

We say that • is pre-order-valued, iff it is (W, ≤)-pre-order-valued for some pre-ordered set (W, ≤), and similarly for poset-valued.

Definition 3.3. • is (W, ≤, ∧, ∨)-lattice-valued iff target( • ) = W and (W, ≤)
is a lattice, with ∧ and ∨ as its meet and join operator, respectively. and(W, ≤) is a bounded lattice, with ⊥ and ⊤ as its least and greatest element, respectively.

Definition 3.4. • is (W, ≤, ∧, ∨, ⊥, ⊤)-lattice-valued iff • is (W, ≤, ∧, ∨)- lattice-valued,
We say that • is lattice-valued, iff it is (W, ≤, ∧, ∨)-lattice-valued for some (W, ≤), ∧ and ∨. We say that • is bounded lattice-valued, iff it is (W, ≤, ∧, ∨, ⊥, ⊤)-lattice-valued, for some (W, ≤), ∧, ∨, ⊥ and ⊤.

Definition 3.5. • is set-valued iff we have target( • ) = ℘(W ) for some non-empty set W .

Structural Properties for Interpretation Functions

It will sometimes be interesting to restrict ourselves to interpretation functions satisfying certain structure properties. Assume that • is ≤-poset-valued. Below the comma ',' is the concatenation operator. The axiom in the table below, are to be understood as quantifying universally. -→ α , -→ β ranging over dom( • ) * and α, β ranging over dom( • ).

Axiom name

Meaning

contraction - → α , ϕ, ϕ, - → β ≤ - → α , ϕ, - → β expansion - → α , ϕ, - → β ≤ - → α , ϕ, ϕ, - → β exchange - → α , ϕ, ψ, - → β = - → α , ψ, ϕ, - → β right monotonicity - → α , ϕ ≤ - → α left monotonicity ϕ, - → α ≤ - → α - → ǫ -⊤ - → α ≤ - → ǫ adjunction If - → α ≤ - → β and - → α ≤ - → γ then - → α ≤ - → β - → γ mix If - → α 1 ≤ - → β 1 and - → α 2 ≤ - → β 2 then - → α 1 - → α 2 ≤ - → β 1 - → β 2
For example, • satisfies contraction iff for every -→ α , -→ β ∈ L * and ϕ ∈ L we have

-→ α , ϕ, ϕ, -→ β ≤ -→ α , ϕ, -→ β .
Remark 3.6. If • satisfies exchange, then • for every -→ ϕ and -→ ψ that are equivalent up to permutation we have -→ ϕ = -→ ψ . If • satisfies either right or left monotonicity, then • satisfies -→ ǫ -⊤.

Stronger Properties

Definition 3.7 (Conjunctive, intersective interpretation)

-• is conjunctive iff it is lattice-valued and ∀ -→ ϕ , -→ ψ , -→ ϕ -→ ψ = -→ ϕ ∧ -→ ψ . -• is intersective iff it is set-valued and ∀ -→ ϕ , -→ ψ , -→ ϕ -→ ψ = -→ ϕ ∩ -→ ψ .
Definition 3.8. We let • t be the interpretation function for L * defined by

-→ ϕ t := ϕ∈ran( - → ϕ ) t . Example 3.1. • t is intersective. If • is intersective, then it is bounded ⊆- lattice-valued.
We start by recalling some basic definitions.

Definition 4.1 (Semi-Pseudometric). A semi-pseudometric on a set X is a function d : (X × X) → R, such that for all x, y, z ∈ X we have:

1. d(x, x) = 0; 2. d(x, y) = d(y, x).
Definition 4.2 (Pseudometric). A pseudometric on a set X is a semipseudometric on X, such that for all x, y, z ∈ X we have:

3. d(x, z) ≤ d(x, y) + d(y, z) (triangle inequality).
If d is a (semi-)pseudometric on X, then (X, d) is a (semi-)pseudometric space.

Definition 4.3 (Trivial pseudo-metric). The trivial pseudo-metric over a set

A is the function d : A × A → R ∀x, y ∈ A d(x, y) = 0

Metrics on Valuations, Relations and Graphs

Given a finite set prop Hamming distance on 2 prop is the metric

δ ham : 2 prop × 2 prop → ω defined as δ ham (V, V ′ ) = card(V ⊖ V ′ ).

Aggregators

Let δ i be a pseudo-metric on a set X. We want to study closeness between subsets of X, and so we provide some natural aggregators α associating with δ i a function d i α : 2 X × 2 X → R, that may or may not be a pseudo-metric, depending on the particular aggregator. A,A). Note also that the min aggregator will return 0 for (A, B) whenever A ∩ B = ∅.

Let W be a set and let d be a pseudo-metric on W . Let L be a language and let

• be an interpretation function for L such that target( • ) = ℘(W ) for some non-empty set W . Let 5 What Is a Semantic Metric?

d i α : ℘(W ) × ℘(W ) → R be an aggregator based on the distance d i between points of W . We let d i α,L, • : L * × L * → R be defined by d i α,L, • ( -→ ϕ , -→ ψ ) = d i α ( -→ ϕ , -→ ψ ).
Now that we have set the stage for our investigations, our first task is to define our object of interest: semantic pseudometrics. Semantic pseudometrics are a subclass of linguistic pseudometrics.

Definition 5.1 (Linguistic (semi-)pseudometric). A linguistic (semi-) pseudometric on a language L is a partial function d : (L * × L * ) → R such that dom(d) is symmetric and (dom(d), d) is a (semi-)pseudometric space.
How semantic pseudometrics should be defined is not a fully straightforward matter. A minimal requirement would be the following:

If for every -→ χ 1 , -→ χ 2 with -→ χ 1 = -→ χ 2 we have d( -→ ϕ , -→ χ 1 ) = d( -→ ψ , -→ χ 2 ) then -→ ϕ = -→ ψ (min sem separation)
That is, if two sequences -→ χ 1 , -→ χ 2 are semantically non-equivalent, then there should be two (other) semantically equivalent sequences, that are not pairwise equidistant from -→ χ 1 and -→ χ 2 . A stronger, yet reasonable, assumption is:

If for every -→ χ we have d( -→ ϕ , -→ χ ) = d( -→ ψ , -→ χ ) then -→ ϕ = -→ ψ (sem separation)
The axiom states that if two sequences of formulas -→ ϕ and -→ ψ are not semantically equivalent, then there is some sequence of formulas -→ χ that is not at the same distance from both -→ ϕ and -→ ψ .

Fact 5.2. Let d be a semi-pseudometric. If d satisfies (sem separation), then it satisfies (min sem separation).

Finally we consider a stronger axiom:

If d( -→ ϕ , -→ ψ ) = 0 then -→ ϕ = -→ ψ (zero ⇒ sem≡)
The axiom is a regularity condition stating, that semantically non-equivalent sequences of formulas, should be at positive distance of each other.

Fact 5.3. Let d be a semi-pseudometric. If d satisfies (zero ⇒ sem ≡), then it satisfies (sem separation).

The two become equivalent if we assume triangle inequality.

Fact 5.4. Let d be a pseudo-metric. d satisfies (sem separation) iff d satisfies (zero ⇒ sem ≡).

The converse of (zero ⇒ sem ≡), below, states that semantically equivalent sequences formulas, should be a distance 0 of each other.

If -→ ϕ = -→ ψ then d( -→ ϕ , -→ ψ ) = 0 (sem≡ ⇒zero)
Unsurprisingly (sem ≡ ⇒ zero) will filter out syntactically driven notions such as δ count or δ synt,count .

Definition 5.5. Given a language L, let

δ count ( -→ ϕ , -→ ψ ) := card(ran( -→ ϕ )⊖ran( -→ ψ )) Definition 5.6. Given a language L, let δ synt,count ( -→ ϕ , -→ ψ ) := δ count ( -→ ϕ , -→ ψ ) + card(sig( -→ ϕ ) ⊖ sig( -→ ψ ))
Fact 5.7. (L prop (1), δ count ) does not satisfy (sem ≡ ⇒ zero).

Fact 5.8. (L prop (1), δ synt,count ) does not satisfy (sem ≡ ⇒ zero).

As observed previously, (sem ≡ ⇒ zero) rules out a number of aggregators, e.g. :

Fact 5.9. (L prop , d ham max ) does not satisfy (sem ≡ ⇒ zero). We have seen that (sem≡ ⇒ zero) and the triangle inequality together imply that two semantically equivalent points are equidistant to any other third point. This latter notion of semantic invariance implies in return (sem ≡ ⇒ zero) and might be a desirable property as well:

If -→ ϕ = -→ ψ then for every -→ χ we have d( -→ ϕ , -→ χ ) = d( -→ ψ , -→ χ ) (sem preservation) Fact 5.10. Let d be a semi-pseudometric. If d satisfies (sem preservation) then d satisfies (sem ≡ ⇒ zero).
Finally, we can require our (semi-)pseudometric to be fully induced by a distance on the co-domain of the interpretation function • , which we define as follows:

If -→ ϕ 1 = -→ ψ 1 and -→ ϕ 2 = -→ ψ 2 then d( -→ ϕ 1 , -→ ϕ 2 ) = d( -→ ψ 1 , -→ ψ 2 ) (sem induced) Fact 5.11. Let d be a semi-pseudometric. If d satisfies (sem induced) then d satisfies (sem preservation).
Fact 5.12. Let d be a pseudo-metric. If d satisfies (sem ≡ ⇒ zero), then it satisfies (sem induced).

Corollary 5.13. Let d be a pseudo-metric that satisfies (sem ≡ ⇒ zero). There exists a pseudo-metric ḋ on ran(

• ) such that ḋ( -→ ϕ , -→ ψ ) = d( -→ ϕ , -→ ψ ).
Fact 5.14. Let d be a pseudo-metric that verifies (sem ≡ ⇒ zero). Let ≡ be the kernel of • . The following holds: Figure 1, in p. 9, summarizes the relation between the axioms discussed in this section. We are now ready to define our notion of 'semanticity'.

1. If -→ ϕ ≡ -→ ψ then ∀ -→ χ d( -→ χ , -→ ϕ ) = d( -→ χ , -→ ψ ).
Definition 5.16 (Semantic Pseudometric). A linguistic (semi-)pseudometric is semantic whenever for all -→ ϕ , -→

ψ we have -→ ϕ = -→ ψ iff for all -→ χ 1 , -→ χ 2 such that -→ χ 1 = -→ χ 2 we have d( -→ ϕ , -→ χ 1 ) = d( -→ ψ , -→ χ 2 ).
Fact 5.17. A linguistic semi-pseudometric is semantic iff it satisfies (min sem separation) and (sem induced).

Fact 5.18. A linguistic pseudometric is semantic iff it satisfies (min sem separation) and (sem ≡ ⇒ zero).

Now that we have settled our definition of semantic pseudo metric, which we will use in the sequel, we can tackle our main problem-in brief:

What are reasonable properties of a semantic pseudometric on (a subset of) L * ?

In this section we will investigate how various semantic pseudo metrics behave with respect to some different axioms, some more intuitive than others. We have already introduced the Hausdorff metric d ham H over sequences of formulas in L prop . We now provide some other metrics.

Examples of Semantic Metrics

If • is finite set-valued, we can define the following metrics: Definition 6.1 (Semantic Symmetric Difference Metric). The semantic symmetric difference metric is the cardinality of the symmetric difference between the respective interpretations.

d ⊖ ( -→ ϕ , -→ ψ ) := card( -→ ϕ ⊖ -→ ψ ).
Definition 6.2 (Proportional metric). The proportional metric decreases from 1 to 0 as the ratio between the intersection and the union of the respective interpretations increases.

d α ( -→ ϕ , -→ ψ ) =    0 if -→ ϕ = -→ ψ = ∅ 1 -card( - → ϕ ∩ - → ψ ) card( - → ϕ ∪ - → ψ )
otherwise Observe that, with this measure, pairs of sequences with non-empty disjoint interpretations will always be at distance 0 of each other.

The idea is behind the next metric is to measure closeness by the continuations of two sequences. Our idea is to count how many possible semantic continuations one sequence has that can not apply to the other. For a set-valued interpretation function, this is given by the cardinal of the symmetric difference between the power sets of the respective interpretations. This should then be normalized by the possible ways to continue these sequences. This is given by the cardinal of the cartesian product of the power sets of the respective interpretations. Moreover we normalize this measure by the number of possible semantic values, prop) . Here is the definition:

card(℘({0, 1} prop )) = 2 2 card(
Definition 6.3 (Continuation-based pseudometric) d C ( -→ ϕ , -→ ψ ) = card(2 - → ϕ ⊖ 2 - → ψ ) card(2 - → ϕ × 2 - → ψ ) • 1 2 2 card(prop)
In the simplistic setting of building a semantic metric for L * prop with the classical truth functional

• t interpretation, a natural notion of understanding possible continuation, is one of consistent continuation. A set -→ ϕ t is a possible continu- ation of -→ ψ just in case -→ ϕ -→ ψ t = -→ ϕ t ∩ -→ ψ t = ∅. Following this definition, a possible continuation of -→ ϕ which is not a possible continuation of -→ ψ is uniquely decomposed into a part of -→ ϕ t \ -→ ψ t and a set of valuations that are neither in -→ ϕ t nor -→ ψ t .
Fact 6.4. For any set-valued interpretation, the preceding definition is equivalent to the following:

d C ( -→ ϕ , -→ ψ ) = 2 card( - → ϕ ) + 2 card( - → ψ ) -2 • 2 card( - → ϕ ∩ - → ψ ) 2 card( - → ϕ )+card( - → ψ )
6.2 Shortest Paths in Covering Graphs [START_REF] Monjardet | Metrics on partially ordered sets -a survey[END_REF] summarizes interesting results concerning metrics on posets and lattices. We will make use of two of these results to shed a different light on the semantic metrics defined in the previous section. In what follows, let W, ∨, ⊤, ≤ be a bounded semi-lattice with ⊤ as greatest element. For all x, y ∈ W , we say that y covers x iff x < y and ∀z, x < z ≤ y → y = z. Define also inductively the rank of an element, by setting all < -minimal elements of rank 0, and for every y covering a x of rank n, setting y of rank n + 1.

Definition 6.5 (Covering graph of a semi-lattice). Let W, ⊤, ≤ be a semi-lattice with ⊤ as greatest element. The covering graph

G(W ) = V, E of W is such that V = W and (x, y) ∈ E iff x covers y or y covers x.
Definition 6.6. An upper valuation is an isotone map v :

W → R such that ∀z z ≤ x, y → v(x) + v(y) ≥ v(x ∨ y) + v(z).
Let G(W ) = W, E be the covering graph of W and let v be an upper valuation on W . For each edge (x, y) ∈ E, let the weight function ω v : E → R induced by v be defined by ω(x, y) = |v(x)v(y)|. Moreover, let π(x, y) be the set of paths from x to y. We make use of two results exposed in [START_REF] Monjardet | Metrics on partially ordered sets -a survey[END_REF]:

Fact 6.7 [START_REF] Monjardet | Metrics on partially ordered sets -a survey[END_REF]. Let v be an isotone upper valuation. We have:

1. the function d v (x, y) = 2v(x ∨ y)v(x)v(y) is positive and verifies the triangle inequality. 2. d v (x, y) = δ v (x, y) := min pxy∈π(x,y) (z1,z2)∈pxy ω(x, y). Definition 6.8. If v is an isotone, positive, upper valuation that assigns 0 to minimal elements in the semi-lattice, then the normalized distance is defined by

d n v (x, y) = dv(x,y) v(x∨y) if v(x ∨ y) = 0, 0 otherwise.
Fact 6.9. If v is an isotone, positive, upper valuation that assigns 0 to minimal elements in the semi-lattice, then the normalized distance d n v ≥ 0 and d n v verifies the triangle inequality.

This offers a new perspective on the Symmetric difference and Proportional metrics as metrics defined by minimal-weighted paths in the lattice: Fact 6.10. Consider the (semi-)lattice 2 prop , ⊆, prop , and the mapping v 0 that assigns to each V ∈ 2 prop its rank. We have

d ⊖ ( -→ ϕ , -→ ψ ) = δ v0 ( -→ ϕ , -→ ψ ) = card( -→ ϕ ⊖ -→ ψ )
Fact 6.11. Consider the (semi-)lattice 2 prop , ⊆, prop , and the mapping v 0 that assigns to each V ∈ 2 prop its rank. We have

d α ( -→ ϕ , -→ ψ ) = δ n v0 ( -→ ϕ , -→ ψ )
When the lattice is the lattice of subsets of some set A, the rank of X ⊆ A coincide with its cardinal, hence the two facts above. This suggest d v0 and d n v0 as natural generalisations of d ⊖ and d α for more general semi-lattices.

The continuations-based metric is also expressible in these minimal-weighted paths terms, but this requires a little more work: Fact 6.12. Let v : W → R be an isotone, mapping. The mapping w : W → R such that w : x → -2 -v(x) is isotone as well. Moreover, if v is an upper valuation, then so is w. Corollary 6.13. Consider the (semi-)lattice 2 prop , ⊆, prop , and the mapping v 0 that assigns to each V ∈ 2 prop its rank, and w 0 defined by w 0 (x) = -2 -v0(x) . We have

d C ( -→ ϕ , -→ ψ ) = δ w0 ( -→ ϕ , -→ ψ )
Corollary 6.14. d ⊖ , d α and d C are all pseudo-metrics.

Stronger Semantic Axioms

We next move to axioms that differentiate between our metrics. We start by considering the following axiom: Assume that • is -poset-valued. The following axiom is very mild:

d( -→ ϕ , -→ ϕ -→ ψ ) ≤ d( -→ ϕ , -→ ψ ) ( rebar
If -→ ϕ -→ ψ then d( -→ ϕ , -→ ϕ -→ ψ ) ≤ d( -→ ϕ , -→ ψ ) (antitonicity)
Fact 6.17. Let • satisfy adjunction and right weakening and let d be a semipseudometric. If d satisfies (sem ≡ ⇒ zero), then d satisfies (antitonicity).

Domain Axioms for Semantic Pseudometrics

Domain axioms require the metric to be well-defined on large portions of the language. Given an interpretation function • : L * → D of these sequences of sentences into some co-domain, we could expect to have: Weakening the preceding axiom, without dropping it entirely, can be done if the co-domain of • is a bounded poset. Recall that ⊥ denote the least element of a bounded poset.

If -→ ϕ , -→ ψ ∈ L * , then d( -→ ϕ , -→ ψ ) ∈ R. ( linguistic
If -→ ϕ = ⊥ and -→ ψ = ⊥, then d( -→ ϕ , -→ ψ ) ∈ R. (consistent domain)
Fact 6.20. (L prop , d ham H ) satisfies (consistent domain).

Axioms for Set-Valued Semantic Pseudometrics

If • is set-valued and target( • ) = ℘(W ) for some W and (W, δ) is a metric space then we can investigate axioms like the following one considered in [START_REF] Eiter | Distance measures for point sets and their computation[END_REF]:

whenever -→ ϕ = {w} and -→ ψ = {v} then d( -→ ϕ , -→ ψ ) = δ(w, v) (EM)
A semantic metric defined as an aggregator of the values of the distance between points in the interpretation of either sequences, will satisfy the preceding axiom.

Signature Invariance Axioms

The next condition states that the relative proximity of conversations should not depend on irrelevant aspects pertaining to the choice of signature.

If -→ ϕ , -→ ψ , -→ χ ∈ L ′ * and L ′ ⊆ L, then we have (weak sig inv) d L ( -→ ϕ , -→ χ ) ≤ d L ( -→ ψ , -→ χ ) iff d L ′ ( -→ ϕ , -→ χ ) ≤ d L ′ ( -→ ψ , -→ χ )
Fact 6.21. (L prop (1), δ count ) and (L prop (1), δ synt,count ) satisfy (weak sig inv).

Uniform Preservation Axioms

The following axiom states that extending conversations with a given piece of information should not change the relative proximity of conversations. Formally:

If d( -→ ϕ , -→ χ ) ≤ d( -→ ψ , -→ χ ) then d( -→ ϕ -→ ϕ 0 , -→ χ -→ ϕ 0 ) ≤ d( -→ ψ -→ ϕ 0 , -→ χ -→ ϕ 0 ) ( uniform
→ ϕ ≤ o -→ ψ iff o( -→ ϕ ) ≤ o( -→ ψ ). Let [ -→ ϕ ] be the equivalence class of -→ ϕ in L * / ∼. Let ↓ [ -→ ϕ ] = { -→ ψ ∈ L * |o( -→ ψ ) ≤ o( -→ ϕ )} and let ↓ [ -→ ϕ ] * be the reflexive transitive closure of ↓ [ -→ ϕ ].
Corollary 7.2. Let • satisfy exchange, contraction, expansion and -→ ǫ -⊤ and let d be a pseudometric. If d satisfies (uniform preservation) and (sem ≡ ⇒ zero), then for every

-→ ϕ , -→ χ ∈ [ -→ ϕ ], -→ ψ 1 , -→ ψ 2 ∈↓ [ -→ ϕ ] * we have d( -→ ϕ , -→ ψ 1 -→ χ -→ ψ 2 ) = 0.
Corollary 7.3. Let • satisfy exchange, contraction, expansion and -→ ǫ -⊤ and let d be a pseudometric. If d satisfies (uniform preservation), (sem ≡ ⇒ zero) and (min sem separation), then for every

-→ ϕ , -→ χ ∈ [ -→ ϕ ], -→ ψ 1 , -→ ψ 2 ∈↓ [ -→ ϕ ] * we have -→ ϕ = -→ ψ 1 -→ χ -→ ψ 2 .
Hence (uniform preservation) comes with very disputable consequences. The converse is even more problematic:

If d( -→ ϕ -→ ϕ 0 , -→ χ -→ ϕ 0 ) ≤ d( -→ ψ -→ ϕ 0 , -→ χ -→ ϕ 0 ) then d( -→ ϕ , -→ χ ) ≤ d( -→ ψ , -→ χ ) (uniform anti-preservation)
These two axioms are quite demanding. But the situation is much more radical for (uniform anti-preservation): if the interpretation satisfies very mild conditions: such as contraction, expansion and exchange, then the only semi-pseudometric satisfying (uniform anti-preservation) and (sem ≡ ⇒ zero), is the trivial metric.

Fact 7.6. Let • be an interpretation satisfying contraction, expansion and exchange and let d be a semi-pseudometric on target( • ). The following are equivalent:

1. d satisfies (uniform anti-preservation) and (sem ≡ ⇒ zero) 2. d is the trivial metric on target( • ) This result is a very strong argument against the reasonableness of (uniform antipreservation).

Preservation Axioms: Close Information

The preceding axioms considered extensions of two sequences with the same sequence of formulas. As we have seen, they are too demanding. What if instead, we are interested in the relative effect of extending with a sequences that might be more or less similar to the sequence it is extending. We could expect, that the closer that new sequence is from the original one, the closer the resulting conversation will be from the original one. Or at least that a reverse in respective orderings cannot occur. Formally,

If d( -→ ϕ , ψ 1 ) < d( -→ ϕ , ψ 2 ) then d( -→ ϕ , -→ ϕ ψ 1 ) ≤ d( -→ ϕ , -→ ϕ ψ 2 ) (action pref) Fact 7.7. d ham H , d ⊖ , d α , d C
do not satisfy (action pref) Conversely, we can require the deviation of the resulting sequence to be smaller, whenever the original sequence is closer to the new one by which it is extended.

If d( -→ ϕ , χ) < d( -→ ψ , χ) then d( -→ ϕ , -→ ϕ χ) < d( -→ ψ , -→ ψ χ) (coherent deviation)
Fact 7.8. Let • = • t . d α satisfy neither (action pref) nor (coherent deviation).

Fact 7.9. Let d be a semi-pseudometric on target( • ). The following are equivalent:

1. d satisfies (coherent deviation) and the triangle inequality 2. d is the trivial metric on target( • )

As we will show, the respective converses of the two preceding axioms are certainly unreasonable.

If d( -→ ϕ , -→ ϕ ψ 1 ) ≤ d( -→ ϕ , -→ ϕ ψ 2 ) then d( -→ ϕ , ψ 1 ) ≤ d( -→ ϕ , ψ 2 ) (converse strong action pref)
Fact 7.10. Let d be a pseudometric on target( • ). The following are equivalent:

1. d satisfies (converse strong action pref) 2. d is the trivial metric on target( • ) If d( -→ ϕ , -→ ϕ χ) ≤ d( -→ ψ , -→ ψ χ) then d( -→ ϕ , χ) ≤ d( -→ ψ , χ) (converse coherent deviation)
Fact 7.11. Let d be a pseudometric on target( • ). The following are equivalent:

1. d satisfies (converse coherent deviation) 2. d is the trivial metric on target( • ).

Conjunction and Disjunction Axioms

Conjunction Axioms

Assume that • is lattice-valued. The following axiom regulates the behavior of the distance with respect to the meet. But as we will see, it is much too demanding. The above facts follow from the equality case in (strong ∧ rule): for any sequences

If -→ ϕ 1 ∧ -→ ϕ 2 ≤ -→ ϕ 1 ∧ -→ ϕ 3 then δ( -→ ϕ 1 , -→ ϕ 2 ) ≥ δ( -→ ϕ 1 , -→ ϕ 3 ) (strong ∧ rule) Fact 8.1. Let • be lattice-valued and let d be a semi-pseudometric on target( • ). If d satisfies (strong ∧ rule), then whenever -→ ϕ ≤ -→ ψ , we have d( -→ χ , -→ ϕ ) ≥ d( -→ χ , -→ ψ ) for any -→ χ .
-→ ϕ , -→ ψ 1 , -→ ψ 2 , if -→ ψ 1 ∧ -→ ϕ = -→ ψ 2 ∧ -→ ϕ then -→ ψ 1 and -→
ψ 2 have to be equidistant from -→ ϕ . Removing this assumption yields a weakening of (strong ∧ rule) which no longer support the trivialisation result above:

If -→ ϕ 1 ∧ -→ ϕ 2 -→ ϕ 1 ∧ -→ ϕ 3 then δ( -→ ϕ 1 , -→ ϕ 2 ) ≥ δ( -→ ϕ 1 , -→ ϕ 3 ) (weak ∧ rule)
Fact 8.4. d ham H , d ⊖ and d α do not satisfy (weak ∧ rule). Fact 8.5. For any set-valued • , d C verifies (weak ∧ rule).

Corollary 8.6. • t is an intersective interpretation which yield a d C that verifies (weak ∧ rule), the triangle inequality and is not trivial.

Disjunction Axioms

Assume that • is lattice-valued. The following axiom is very mild.

If

-→ ψ = -→ ϕ 1 ∨ -→ ϕ 2 then d( -→ ϕ 1 , -→ ψ ) ≤ d( -→ ϕ 1 , -→ ϕ 2 ) (∨ rule)
Fact 8.7. Assume that target( • ) = ℘(W ) for some non-empty W and that • is lattice-valued. Let δ be a metric on W . d δ H satisfies (∨ rule). Fact 8.8. d ⊖ , d α and d C also satisfy (∨ rule).

Future Directions

So far we have focused on isolating an abstract concept of semanticity for metrics. We have explored general axioms that help us express components of this concept. We have also identified more specific axioms that were candidates at defining the contour of a notion of 'good behavior' for semantic metrics, and thus at being criterion for evaluating such metrics. We have done this at an abstract level, considering conversations as sequences of formulas where one conversational agent plays a sequence of formulas after the other. The conversation thus has the structure of a (syntactic) monoid with a syntactic composition operation of concatenation. Corresponding to sequences of formulas is their abstract interpretation in a different, semantic space; the generic notion of a semantic interpretation furnishes the correspondence, mapping these sequences into the semantic space.

Coming back to the goals outlined in the introduction of this paper, the next step of our work is to extend this perspective to structures that represent real conversations. We mention a few directions here, each of which can be explored independently. In order to do this, we need to fill in this abstract framework with notions that capture aspects of conversational content at various levels of detail. A first step is to refine the notion of sequence of formulas into something that preserves more of the logical form of conversations. Most models of discourse interpretation assume a more structured representation of conversations, e.g., trees or graphs, in which elementary discourse units are linked together via discourse relations to form more complex discourse units. Using such structures to represent conversations would require us to adapt the structural properties of interpretation functions considered in Sect. 3.2 to be able to reflect the semantics of discourse relations and the units they link together. Second we would need to revisit the axioms that make use of concatenation, replacing the latter with a notion of a graph update or graph extension.

Furthermore, to deal adequately with some natural language phenomena such as questions, commands, agreements and disagreements among speakers, explicit or implicit corrections, it is natural to assume additional structure for semantic spaces, on top of that provided by general lattices. This additional semantic structure could also serve to refine some of our axioms, in particular those making hypotheses on lattice-theoretic relations between the semantic interpretations of two conversations.

Different notions of semantic interpretation carry different amounts of the initial syntactic structure into the semantic space. The classical notion of information content for a discourse erases all structural information, mapping discourses such as Jane fell because John pushed her and John pushed Jane so she fell into the exact same semantic interpretation (either a set of possible worlds or a set of world assignment pairs as in SDRT and other dynamic semantic theories). Differently structured discourses, even when they share the same meaning, however, may exhibit different semantic and pragmatic behavior, concerning the possibility of future coreferences and of ways to extend the conversation. Intuitions dictate that these features are important for a notion of conversational similarity. It will therefore be important to test metrics defined on more structurally-conservative spaces, for instance conserving some aspects of the conversational graph. These metrics should match intuitions as to how far two real conversations are from each other.

Conclusions

Our first task was to explore the concept of a semantic metric by identifying a certain number of reasonable axioms that characterize the idea of 'semanticity' for a distance. We clarified the relation between these different axioms and the triangle inequality, and we mapped out a lattice of axioms in terms of their logical strength. Next, we explored a structured list of candidate axioms or desirable properties for any semantic metric. We found several to be too demanding, in the sense that under some structural constraints on the interpretation function and on the distance, they could only be satisfied by the trivial metric. These axioms divide into a certain number of categories. First, we considered a certain number of axioms pertaining to general properties of semantic metrics, including arguably mild assumptions about their structure, their domain and their insensitivity to the choice of signature. Then, we considered preservation axioms that carry a general idea of coherence between the relative proximity of sequences and of their extensions. Finally we considered axioms that are more specific to a lattice-or a set-theoretic approach.

We concentrated on the foundational case of conversations as sequences of propositional formulae with a classical truth functional interpretation by studying four semantically induced metrics that looked intuitively promising (based respectively on the ideas of symmetric semantic difference, semantic proportionality, Hausdorff metric and on possible continuations). We now have a clear picture of their different behavior. Overall however, these metrics satisfy only few of our axioms that do not lead to a triviality result. One reason for this are the very strong structural hypotheses behind the set-theoretic, classical interpretation of the language of the propositional calculus. A further exploration of these axioms in the context of interpretation into structures like lattices with fewer structural hypotheses and of more general families of metrics remains to be done. We hope that the abstract setting that we have set up in this paper can serve a first step towards achieving this goal.

A Appendix: Selected Proofs (Proof of Fact 5.2). Assume that for every -→

χ 1 , -→ χ 2 with -→ χ 1 = -→ χ 2 we have d( -→ ϕ , -→ χ 1 ) = d( -→ ψ , -→ χ 2 ) (i)
. Now take some -→ χ . We have -→ χ = -→ χ . Hence by (i), we have d

( -→ ϕ , -→ χ ) = d( -→ ψ , -→ χ ). But -→ χ was arbitrary, hence ∀χ d( -→ ϕ , -→ χ ) = d( -→ ψ , -→ χ ). It follows, by (sem separation), that -→ ϕ = -→ ψ . qed (Proof of Fact 5.3). Assume that ∀ -→ χ , d( -→ ϕ , -→ χ ) = d( -→ ψ , -→ χ ). In particular d( -→ ϕ , -→ ψ ) = d( -→ ψ , -→ ψ ) = 0. Hence by (zero ⇒ sem ≡), -→ ϕ = -→ ψ . qed
(Proof of Fact 5.4). The right to left direction follows from Fact 5.3. For the left to right direction, assume that d( -→ ϕ , -→ ψ ) = 0 (i). Take any -→ χ . By triangle inequality, d(

-→ χ , -→ ϕ ) ≤ d( -→ χ , -→ ψ ) + d( -→ ψ , -→ ϕ ). Hence, by (i) we have d( -→ χ , -→ ϕ ) ≤ d( -→ χ , -→ ψ ). Similarly we have d( -→ χ , -→ ψ ) ≤ d( -→ χ , -→ ϕ ). Hence d( -→ χ , -→ ψ ) = d( -→ χ , -→ ϕ ). But χ was arbitrary, hence for all χ we have d( -→ χ , -→ ψ ) = d( -→ χ , -→ ϕ )
. By (sem separation), it follows that -→ ϕ = -→ ψ . qed (Proof of Fact 5.7). p¬p = q¬q but δ count (p¬p, q¬q) = 4. qed (Proof of Fact 5.8). p¬p = q¬q but δ synt,count (p¬p, q¬q) = 6. qed (Proof of Fact 5.9). Take some ϕ such that card( ϕ ) ≥ 2. qed 5.11). Assume that -→ ϕ 1 = -→ ψ 1 . Take some -→ χ . We have -→ χ = -→ χ . Hence by (sem induced) we have d

(Proof of Fact 5.10). Assume that -→ ϕ = -→ ψ . By (sem preservation) we have d( -→ ϕ , -→ χ ) = d( -→ ψ , -→ χ ). In particular we have d( -→ ϕ , -→ ψ ) = d( -→ ψ , -→ ψ ) = 0 qed (Proof of Fact
( -→ ϕ 1 , -→ χ ) = d( -→ ψ 1 , -→ χ )
. qed (Proof of Fact 5.12). Assume that -→ ϕ 1 = -→ ψ 1 (i) and -→ ϕ 2 = -→ ψ 2 (ii). By triangle inequality we have:

d( -→ ϕ 1 , -→ ϕ 2 ) ≤ d( -→ ϕ 1 , -→ ψ 1 ) 0, by(sem≡ ⇒ zero) +d( -→ ψ 1 , -→ ϕ 2 ) d( -→ ψ 1 , -→ ϕ 2 ) ≤ d( -→ ψ 1 , -→ ψ 2 ) + d( -→ ψ 2 , -→ ϕ 2 ) 0, by(sem≡ ⇒ zero) Hence, d( -→ ϕ 1 , -→ ϕ 2 ) ≤ d( -→ ψ 1 , -→ ψ 2 ). Similarly, we have d( -→ ϕ 1 , -→ ϕ 2 ) ≥ d( -→ ψ 1 , -→ ψ 2 ). qed
(Proof of Corollary 5.13). By Fact 5.12, d satisfies (sem induced), hence for every

-→ ϕ 1 , -→ ϕ 2 , -→ ψ 1 , -→ ψ 2 with -→ ϕ 1 = -→ ψ 1 and -→ ϕ 2 = -→ ψ 2 we have d( -→ ϕ 1 , -→ ϕ 2 ) = d( -→ ψ 1 , -→ ψ 2 ) It follows that ḋ( -→ ϕ , -→ ψ ) := d( -→ ϕ , -→ ψ ) is well-defined. Moreover for any -→ ϕ , d( -→ ϕ , -→ ϕ ) = d( -→ ϕ , -→ ϕ ) = 0.
Triangle inequality is proven similarly. qed (Proof of Fact 5.14). First observe, that by triangle inequality, we have

d( -→ χ , -→ ϕ ) ≤ d( -→ χ , -→ ψ ) + d( -→ ψ , -→ ϕ ) Now, assume that -→ ϕ ≡ -→ ψ . By (sem ≡ ⇒ zero) we have d( -→ ψ , -→ ϕ ) = 0, hence d( -→ χ , -→ ϕ ) ≤ d( -→ χ , -→ ψ ). Similarly, d( -→ χ , -→ ψ ) ≤ d( -→ χ , -→ ϕ ) which proves (1). qed (Proof of Fact 5.15). Assume that ∀χ we have d(ϕ, χ) = d(ψ, χ) (i). Take some -→ χ 1 , -→ χ 2 with -→ χ 1 = -→ χ 2 . By (sem ≡ ⇒ zero) we have d( -→ χ 1 , -→ χ 2 ) = 0 (ii)
. By triangle inequality we have:

d( -→ ϕ , -→ χ 1 ) ≤ d( -→ ϕ , -→ χ 2 ) + d( -→ χ 2 , -→ χ 1 ) 0, by(ii) d( -→ ϕ , -→ χ 2 ) ≤ d( -→ ϕ , -→ χ 1 ) + d( -→ χ 1 , -→ χ 2 ) 0, by(ii) Hence d( -→ ϕ , -→ χ 1 ) = d( -→ ϕ , -→ χ 2 ). Moreover by (i) we have d( -→ ϕ , -→ χ 2 ) = d( -→ ψ , -→ χ 2 ). Hence d( -→ ϕ , -→ χ 1 ) = d( -→ ψ , -→ χ 2 ). Since -→ χ 1 , -→ χ 2
were arbitrary, it follows by (min sem separation), that -→ ϕ = -→ ψ . qed (Proof of Fact 6.12). Let v be an isotone upper valuation and z ≤ x, y.

Assume without loss of generality that v(y) ≥ v(x). We can write, for 0 ≤ α ≤ 1: x) .

-α • 2 -v(y) ≥ -2 -v(y) ≥ -2 -v(x) , which ensures that -α • 2 -v(y) - 1 α 2 -v(x) ≤ -2 -v(y) -2 -v(
Instantiating this result for α = 2 v(z)-v(x) yields after development

-2 v(z)-v(x)-v(y) -2 -v(z) ≤ -2 -v(y) -2 -v(x) .
Since v is an upper-valuation, we have -

v(x ∨ y) ≥ v(z) -v(x) -v(y) and thus -2 -v(x∨y) -2 -v(z) ≤ -2 v(z)-v(x)-v(y) -2 -v(z) ≤ -2 -v(y) -2 -v(x)
i.e., w(x ∨ y) + w(z) ≤ w(x) + w(y) which concludes the proof. The case v(x) ≥ v(y) is symmetrically dealt with. qed (Proof of Fact 6.16). Let -→ ϕ :=(p 1 ∧p 2 )∨(¬p 1 ∧¬p 2 ∧¬p 3 ) and -→ ψ :=(p 1 ∧(p 2 → p 3 )), and assume some intersective interpretation of concatenation. We have

-→ ϕ -→ ψ = p 1 ∧ p 2 ∧ p 3 . d ham H ( -→ ϕ , -→ ϕ -→ ψ ) = 3, but d ham H ( -→ ϕ , -→ ψ ) = 1. qed (Proof
:= p 1 → (¬p 2 ∧ . . . ∧ ¬p n ) ∧ ¬p 1 → (p 2 ∧ . . . ∧ p n ), ψ := p 1 ∧ ¬p 2 ∧ . . . ∧ p 2k-1 ∧ ¬p 2k , χ := p 1 ∧ . . . ∧ p n and ϕ 0 := p 1 . Since k ≥ 2 we have 1 = d ham H (ϕ, χ) < d ham H (ϕ, χ) = k, and, n -1 = d ham H (ϕϕ 0 , χϕ 0 ) > d ham H (ϕϕ 0 , χϕ 0 ) = k = n/2
Concluding our proof. qed (Proof of Fact 7.6). (1 ⇒ 2). Take some -→ ϕ , -→ ψ . By contraction, expansion and exchange we have

-→ ϕ -→ ϕ -→ ψ = -→ ψ -→ ϕ -→ ψ Hence by (sem ≡ ⇒ zero), d( -→ ϕ -→ ϕ -→ ψ , -→ ψ -→ ϕ -→ ψ ) = 0 (i). Hence d( -→ ϕ -→ ϕ -→ ψ , -→ ψ -→ ϕ -→ ψ ) ≤ d( -→ ψ -→ ϕ -→ ψ , -→ ψ -→ ϕ -→ ψ ) (i). Now, let -→ χ = -→ ψ and -→ ϕ 0 = -→ ϕ -→ ψ . By (i) and (uni- form anti-preservation) we have If d( -→ ϕ -→ ϕ -→ ψ , -→ ψ -→ ϕ -→ ψ ) ≤ d( -→ ψ -→ ϕ -→ ψ , -→ ψ -→ ϕ -→ ψ ) then d( -→ ϕ , -→ ψ ) ≤ d( -→ ψ , -→ ψ ) = 0 Hence by (i), d( -→ ϕ , -→ ψ ) = 0.
Concluding the proof for this direction. The other direction is trivial. qed (Proof of Fact 7.8). Let n ∈ ω be such that n > 5. Moreover let: ϕ

:= (p 3 ∧ . . .∧p n )∧¬(p 1 ∧p 2 ), ψ 1 := (p 1 ∨. . .∨p n )∧¬(p 2 ∧. . .∧p n ) and ψ 2 := (p 2 ∧. . .∧p n ). We have d α (ϕ, ψ 1 ) = 1 -2 n+3 = n+1 n+3 > d α (ϕ, ψ 2 ) = 1 -1 4 = 3 4 . But we have d α (ϕ, ϕψ 1 ) = 1 -2 3 = 1 3 < d α (ϕ, ϕψ 2 ) = 1 -1 3 = 2 3
. qed (Proof of Fact 7.9). Take some -→ ϕ , -→ ψ . By (coherent deviation) we have

If d( -→ ϕ , -→ ǫ ) < d( -→ ψ , -→ ǫ ) then d( -→ ϕ , -→ ϕ -→ ǫ ) < d( -→ ψ , -→ ψ -→ ǫ ) If d( -→ ψ , -→ ǫ ) < d( -→ ϕ , -→ ǫ ) then d( -→ ψ , -→ ψ -→ ǫ ) < d( -→ ϕ , -→ ϕ -→ ǫ )
Since -→ ϕ , -→ ψ were arbitrary, it follows that for any

-→ ϕ , -→ ψ , d( -→ ϕ , -→ ǫ ) = d( -→ ψ , -→ ǫ ). In particular d( -→ ϕ , -→ ǫ ) = d( -→ ψ , -→ ǫ ) = d( -→ ǫ , -→ ǫ ) = 0. Hence by (triangle inequality) we have ∀ -→ ϕ , -→ ψ d( -→ ϕ , -→ ψ ) ≤ d( -→ ϕ , -→ ǫ ) + d( -→ ǫ , -→ ψ ) = 0. qed (Proof of Fact 7.10). (1 ⇒ 2). Take some -→ ϕ , -→ ψ . We have 0 = d( -→ ϕ , -→ ϕ -→ ǫ ) ≤ d( -→ ϕ , -→ ϕ -→ ψ ) Hence by (converse strong action pref) d( -→ ϕ , -→ ǫ ) ≤ d( -→ ϕ , -→ ψ ). But ψ was arbitrary, hence, in particular d( -→ ϕ , -→ ǫ ) ≤ d( -→ ϕ , -→ ϕ ) = 0.
→ ϕ , -→ ψ 1 , -→ ψ 2 with -→ ϕ ∩ -→ ψ 1 -→ ϕ ∩ -→ ψ 2 .
And consider the cardinalities assigned in Fig. 2. Let X 1 := α 1 + η 0 and let X 2 := α 2 + η 0 . Using these cardinalities and inserting them in the expression of the distance, gives us: Similarly:

d C (ϕ, ψ 1 ) = 2 card( - → ϕ ) + 2 card( -→ ψ1 ) -2 • 2 card( - → ϕ ∩ -→ ψ1 ) 2 card( - → ϕ )+card( -→ ψ1 ) = 2 Xϕ+η1+η2 + 2 X1+η1 -2 • 2 η1 2 Xϕ+X1+2η1+η2 - → ϕ -→ ψ2 -→ ψ1
d C (ϕ, ψ 2 ) = 2 Xϕ+η1+η2 + 2 X2+η1+η2 -2 • 2 η1+η2 2 Xϕ+X2+2η1+2η2
From the two previous expression, after simplifications we find:

d C (ϕ, ψ 1 ) -d C (ϕ, ψ 2 ) = 2 Xϕ (2 X2+η2 -2 X1 ) + 2(2 X1 -2 X2 ) 2 Xϕ+X1+X2+η1+η2
From the assumption that -→ ϕ ∩ -→ ψ 1 -→ ϕ ∩ -→ ψ 2 , it follows that η 2 ≥ 1, hence:

2 Xϕ (2 X2+η2 -2 X1 ) + 2(2 X1 -2 X2 ) ≥ 2 X2+η2 -2 X2+1 + 2 X1+1 -2 X1 ≥ 0
which concludes the proof. qed (Proof of Fact 8.7). Take -→ ϕ 1 , -→ ϕ 2 . Assume that -→ ψ = -→ ϕ 1 ∨ -→ ϕ 2 (i). By definition, we have

Fact 5 .

 5 15. Let d be a pseudo-metric. If d satisfies (min sem separation) and (sem ≡ ⇒ zero), then it satisfies (sem separation).

Fig. 1 .

 1 Fig. 1. Summary of the results in Sect. 5. Dashed arrows follow from definitions.

Fact 6 .

 6 22. d ham H , d ⊖ , d α , d C satisfy (weak sig inv)

  preservation) But such an axiom can lead to triviality. Fact 7.1. Let • satisfy exchange, contraction and expansion and let d be a pseudometric. If d satisfies (uniform preservation) and (sem ≡ ⇒ zero), then whenever d(ϕ, χ) ≤ d(ψ, χ) then d(ψχ, ϕψχ) = 0. The next corollary is slightly technical. Let us introduce a bit of notation. Let o : L * → R be defined by o( -→ ϕ ) = d( -→ ǫ , -→ ϕ ), and let ∼ be the kernel of o. Let ≤ o be the total pre-order induced by o, with -

Fact 7. 4 .

 4 Let • = • t . d ham H satisfy neither (uniform preservation), nor uniform anti-preservation. Fact 7.5. Let • = • t . d α , d ⊖ and d C satisfy neither (uniform preservation), nor (uniform anti-preservation).

Corollary 8. 2 .

 2 Let • be lattice-valued and let d be a semi-pseudometric on target( • ). If d satisfies (strong ∧ rule), then whenever-→ ϕ ≤ -→ ψ , we have d( -→ ϕ , -→ ψ ) = d( -→ ψ , -→ ϕ ) = 0.Corollary 8.3. Let • be a lattice-valued interpretation satisfying ( -→ ǫ -⊤) and let d be a semi-pseudometric on target( • ). The following are equivalent:1. d satisfies (strong ∧ rule) and the triangle inequality. 2. d is the trivial metric on target( • ).

  But ϕ was arbitrary as well, hence ∀χd( -→ ϕ , -→ ǫ ) = 0. Hence by triangle inequality for any formula -→ ϕ , -→ψ we have d( -→ ϕ , -→ ψ ) ≤ d( -→ ϕ , -→ ǫ ) + d( -→ ǫ , -→ ψ ) = 0. Concluding our proof. qed (Proof of Fact 7.11).(1 ⇒ 2). Take some -→ ϕ and -→ ψ . We have0 = d( -→ ϕ , -→ ϕ -→ ǫ ) ≤ d( -→ ǫ , -→ ǫ -→ ǫ ) = 0 By (converse coherent deviation) d( -→ ϕ , -→ ǫ ) ≤ d( -→ ǫ , -→ ǫ ) = 0 (i). Similarly, we have d( -→ ψ , -→ ǫ ) = 0 (ii). By (i), (ii) and triangle inequality we have d( -→ ϕ , -→ ψ ) ≤ d( -→ ϕ , -→ ǫ )+ d( -→ ǫ , -→ ψ ) = 0.Concluding our proof. qed (Proof of Fact 8.1). Take some -→ χ and assume that -→ ϕ ≤ -→ ψ . Since target( • ) is a lattice. We have -→ χ ∧ -→ ϕ ≤ -→ χ ∧ -→ ψ . Hence by (strong ∧ rule) δ( -→ χ , -→ ϕ ) ≥ δ( -→ χ , -→ ψ ). qed (Proof of Corollary 8.2). Assume that -→ ϕ ≤ -→ ψ . Since d satisfies (strong ∧ rule), we have by Fact 8.1 we have in particular 0= δ( -→ ϕ , -→ ϕ ) ≥ δ( -→ ϕ , -→ ψ ) = δ( -→ ψ , -→ ϕ ). qed (Proof of Corollary 8.3). (1 ⇒ 2). Take two arbitrary -→ ϕ , -→ ψ . By ( -→ ǫ -⊤) we have -→ ϕ ≤ -→ ǫ and -→ ψ ≤ -→ ǫ . Since d satisfies (strong ∧ rule), it follows by Corollary 8.2 that d( -→ ϕ , -→ ǫ ) = d( -→ ǫ , -→ ψ ) = 0. By triangle inequality it follows that d( -→ ϕ , -→ ψ ) = 0. The (2 ⇒ 1) direction is trivial. qed (Proof of Fact 8.5). Take -

Fig. 2 .

 2 Fig. 2. Assigning cardinalities to the respective intersections.

ψ

  are in one of two cases.(1) max x∈ -→ ϕ1 min y∈ -→ ϕ2 δ(x, y)= d δ H ( -→ ϕ 1 , -→ ϕ 2 ), or, (2) max y∈ -→ ϕ2 min x∈ -→ ϕ1 δ(x, y) = d δ H ( -→ ϕ 1 , -→ ϕ 2 ).Case 1. There are two subcases. Subcase 1a. Assume thatd δ H ( -→ ϕ 1 , min x∈ -→ ϕ1 δ(x, y) (b). Since δ is a metric we have max y∈ -→ ϕ1 min x∈ -→ ϕ1 δ(x, y) = 0.Hence by (i) and (b) we haved δ H ( -→ ϕ 1 , ψ ) = max y∈ - → ϕ 2 min x∈ -→ ϕ1 δ(x, y) (ii). But by (1) and definition of d δ H ( -→ ϕ 1 , -→ ϕ 2 ) we have max y∈ - → ϕ 2 min x∈ -→ ϕ1 δ(x, y) ≤ d δ H ( -→ ϕ 1 , -→ ϕ 2 ) (iii). By (ii)and (iii) we haved δ H ( two subcases. Subcase 2a. d δ H ( -→ ϕ 1 , -→ ψ ) = max x∈ -→ ϕ1 min y∈ - → ψ (a). But since δ is a metric we have max x∈ -→ ϕ1 min y∈ - → ψ ≤ max x∈ -→ ϕ1 min y∈ - → ϕ 2 (v). But by definition d δ H ( -→ ϕ 1 , -→ ϕ 2 ) and (2) we have max x∈ -→ ϕ1 min y∈ - → ϕ 2 ≤ d δ H ( -→ ϕ 1 , -→ ϕ 2 ) (vi). By (v), (vi) and (a), it follows that d δ H ( -→ ϕ 1 ,

max{max x∈A min y∈B d i (x, y), max y∈B min x∈A d i (x, y)}.

  In general max and mean will return a non-zero value for (

	Definition 4.4 (min aggregator). Let d i min (A, B) = min x∈A,y∈B d i (x, y).
	Definition 4.5 (max aggregator). Let d i max (A, B) = max x∈A,y∈B d i (x, y).
	Definition 4.6 (Hausdorff aggregator). Formally d i H (A, B)= Definition 4.7 (mean aggregator). Formally d i am (A, B) x∈A,y∈B 1 card(A×B) d i (x, y).	=
	Remark 4.8.

  When L and • are clear from context, we will simply write d i α for d i α,L, • . For instance, d ham H,L prop , • t is sometimes shortened as d ham H when L prop and • t are clear from context.

  domain)It should be realized that the preceding axiom is relatively strong. Consider for example d ham H . Fact 6.18. But (L prop , d ham H ) does not satisfy (linguistic domain).

	Fact 6.19. d

⊖ , d α , d C verify (linguistic domain)

  By exchange, contraction, expansion, and (sem ≡ ⇒ zero), we have d(ψψχ, χψχ) = 0. Hence d(ϕψχ, χψχ) = 0. By exchange, contraction, expansion, and (sem ≡ ⇒ zero), we have d(ϕψχ, χψ) = 0. Concluding our proof. qed (Proof of Corollary 7.2). We only give the idea of the proof. The idea of the proof is to define a linear order on L * compatible with ≤ o . By induction, using Fact 7.1 we first show the claim for formulas in the same o-equivalence class, then we show that the claim propagate downward, that is for every -→ ψ ∈↓ [ -→ ϕ ]. Finally we show that the claim propagates with transitive closure. qed (Proof of Corollary 7.3). Direct from Fact 5.15 and Corollary 7.2.

	(Proof of Fact 6.21). Adding a new propositional letter that does not occur in
	either sequence will not affect the symmetric difference of the range of formulas,
	nor the symmetric difference of the respective signature. Allowing for the nega-
	tion of the propositional letter that was previously forbidden will not change the
	sets either.	qed
	(Proof of Fact 7.1). Assume that d(ϕ, χ) ≤ d(ψ, χ) then d(ϕψχ, χψχ) ≤
	d(ψψχ, χψχ).
	of Fact 6.18). For any ϕ, d ham H	is neither well-defined for (ϕ, ⊥) nor
	for (⊥, ϕ).	qed

qed (Proof of Fact 7.4). Let k ≥ 2, n = 2k. Now let ϕ

This research was supported by ERC Grant 269427.