Discrete metric.

Stream: maths

[Wrenna Robson]

Hi all.

I needed today the Hamming distance on (fin n -> zmod 2), and (inevitably) I've gone down a rabbit hole on it. It feels like I should automatically get this by using the L_p norm - but for that I need a norm on zmod 2, and the only sensible one is the discrete metric. I realised we didn't actually have this... at all? And so I had a go at it. It's been pointed out to me, though, that these instances aren't safe because they too easily push the instance search into loops.

I was wondering if anyone had any advice on what the right approach would be?

namespace discrete

variables {K : Type*} [decidable_eq K]

instance : pseudo_metric_space K := {
  dist := λ x y, if x = y then 0 else 1,
  dist_self := λ _, by simp,
  dist_comm := λ x y, by simp_rw [dist, eq_comm],
  dist_triangle := λ x y z,
  by {  simp[dist], split_ifs;
        try {simp only [  add_zero, zero_add, zero_le_one,
                          one_add_one_eq_two, one_le_two, zero_le_two]},
        finish }
}

instance [has_zero K] : metric_space K :=
{ eq_of_dist_eq_zero := λ x y h, by { by_contradiction c, unfold dist at h,
                                      rw ite_eq_left_iff at h, exact one_ne_zero (h c) },
..discrete.pseudo_metric_space }

instance [add_comm_group K] : normed_group K := {
  norm := λ x, dist x 0,
  dist_eq := λ x y, by simp_rw [dist, sub_eq_zero] }

instance [non_unital_ring K] : non_unital_normed_ring K := {
  norm_mul := sorry,  --uh oh
  }

end discrete

[Reid Barton]

I think the main problem is lots of things have decidable equality (everything, classically) but most of them won't want this metric.

[Reid Barton]

For example, fin n -> zmod 2.

[Eric Wieser]

Kevin's claim (on discord) is that there's exactly one sane metric for zmod p given prime p, and that's this discrete metric where all distances / norms are one except on equal / zero elements

[Eric Wieser]

And therefore instance [prime p] : normed_space (zmod p) := normed_space.discrete ought to be a fine instance

[Reid Barton]

Is the idea for zmod (p^2) we want dist 0 p = 1/p? Or how about just using the discrete 0-1 metric for all zmod n for simplicity?

[Eric Wieser]

Or how about just using the discrete 0-1 metric for all zmod n for simplicity?

I think the "only for prime p" suggestion was just to be conservative

[Wrenna Robson]

I think different options exist. The main thing I wanted was the best way to define the Hamming distance - which is technically the L0 norm, or the L1 norm with the discrete metric on the underlying space, if you like.

[Wrenna Robson]

I note that for the field with four elements one could also define the Hamming norm with respect to a particular basis...

[Wrenna Robson]

Also, nLab distinguishes between a normed field and a valued field, and our current definition of the former is what they have as the latter.

Indeed, normed_field under the nLab definition is just our [normed_ring K] [field K], and that feels more right to me. I don't see why normed_field has to exist at all - one could imagine a version of normed_ring (valuation_ring, which surely is a thing?) with the current = axiom. Indeed I'm not even sure about normed_ring - that also is very strong. When doing the Hamming distance work separately from the typeclass hierarchy yesterday, I realised that you don't need very much at all to define it... (mul_zero_class was strong enough, right?)

Having spent some time yesterday looking at this I'm very sceptical of the hierarchy here... I'm not very experienced with the typeclass system but something smells off, is the best way I can put it. It feels like you want a typeclass that captures the precise axiom that the norm is compatible with the metric. I appreciate one wants to avoid diamonds very strongly, but - basically I think something is Up with the current definitions. I'm sorry that's not more specific - this isn't my specific areas of maths and there's so so many definitions and classes here it's hard to visualise, but maybe that's part of the issue.

Also, field seems too strong in the definition of normed_space. Why isn't a normed_module a coherent definition? You see the issue really - there's lots of algebraic structures that it seems like you could sensibly attach a norm to - and (appreciating this gets away from my original question somewhat) I'm just sceptical of our current approach. I don't know the best way to work out if I'm correct or to review this stuff - in general I would prefer if every time I touched mathlib I didn't fall down a rabbit hole, but such a thing doesn't appear to be my destiny.

[Wrenna Robson]

I'm sorry for typing too much. I overthink things and my confidence isn't high. I'm not saying things are wrong because of the arrogance of the novice - I'm trying to be as tentative and polite as possible and I hope that comes across. But something just doesn't feel right here.

[Wrenna Robson]

The typeclass situation here reminds me a bit of the way that the co/vontravariant class typeclass has done really good work over in "order + algebra" land.

[Eric Wieser]

The valued_field discussion came up before here

[Wrenna Robson]

Interesting, though not entirely convinced with where it reached...

[Wrenna Robson]

I see why we have the = though - I find the point that there may be no natural examples of the <= for fields convincing.

[Wrenna Robson]

The description for normed_division_ring says: "A normed division ring is a division ring endowed with a seminorm" - why seminorm?

[Eric Wieser]

I'd encourage you to revive that thread if you have more questions there - continuing here risks not getting an answer about the discrete metric!

[Wrenna Robson]

Yes, true - and I do want an answer about that!

[Reid Barton]

Eric Wieser said:

Or how about just using the discrete 0-1 metric for all zmod n for simplicity?

I think the "only for prime p" suggestion was just to be conservative

I agree being conservative like this is good, but in this case there's a mild tradeoff with complexity (& it really needs to be [fact (prime p)]) and arguably there's no great reason to accept the extra complexity.

[Wrenna Robson]

Was returning to this today. Having been hearing about other metrics that are relevant in cryptography (Lee metric, rank metric). Don't think defining the Hamming metric with reference to the L1 norm/discrete norm is the right choice.

[Wrenna Robson]

In many ways all these metrics are defined by the fact that they are all nat-valued...

[Wrenna Robson]

It might be that actually the Hamming metric is better described as a valuation?

[Wrenna Robson]

only no because the domain isn't a field necessarily

[Wrenna Robson]

or a ring

[Wrenna Robson]

This definitely feels like a kind of thing though...

[Wrenna Robson]

https://en.m.wikipedia.org/wiki/Edit_distance - this is an example of another family of things that it might be desirable to have theorems about but for which the natural range is nat or int, even though they're sort-of metrics.

[Wrenna Robson]

For an example of why this might be useful - one might want to induct on the Hamming weight of something, which is possible only because it is nat-valued.

[Eric Wieser]

I PR'd some def discretes in #14621

[Wrenna Robson]

Separately to this, I have an implementation of the hamming distance that does not use the L_p norm, which has the advantage that it's nicely computable. It's here - I might put it in a PR. https://gist.github.com/linesthatinterlace/9d13f7f13a9779e5986db573753741f7