Zulip Chat Archive

Stream: maths

Topic: Discrete metric.


Wrenna Robson (May 03 2022 at 17:04):

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 (May 03 2022 at 23:40):

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 (May 03 2022 at 23:42):

For example, fin n -> zmod 2.

Eric Wieser (May 04 2022 at 00:21):

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 (May 04 2022 at 00:22):

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

Reid Barton (May 04 2022 at 00:27):

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 (May 04 2022 at 00:32):

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 (May 04 2022 at 08:07):

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 (May 04 2022 at 08:16):

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

Wrenna Robson (May 04 2022 at 08:35):

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 (May 04 2022 at 08:36):

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 (May 04 2022 at 08:36):

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 (May 04 2022 at 08:37):

The valued_field discussion came up before here

Wrenna Robson (May 04 2022 at 09:32):

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

Wrenna Robson (May 04 2022 at 09:40):

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 (May 04 2022 at 09:47):

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

Eric Wieser (May 04 2022 at 09:59):

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 (May 04 2022 at 11:00):

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

Reid Barton (May 05 2022 at 13:49):

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 (Jun 01 2022 at 16:01):

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 (Jun 01 2022 at 16:01):

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

Wrenna Robson (Jun 01 2022 at 16:06):

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

Wrenna Robson (Jun 01 2022 at 16:06):

only no because the domain isn't a field necessarily

Wrenna Robson (Jun 01 2022 at 16:08):

or a ring

Wrenna Robson (Jun 01 2022 at 16:10):

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

Wrenna Robson (Jun 01 2022 at 17:26):

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 (Jun 01 2022 at 17:28):

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 (Jun 08 2022 at 15:41):

I PR'd some def discretes in #14621

Wrenna Robson (Jun 09 2022 at 11:36):

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


Last updated: Dec 20 2023 at 11:08 UTC