Stream: Beginner Questions

Topic: Cantor's pairing function


view this post on Zulip Lukas Stevens (May 03 2021 at 13:33):

I need an injective function from (int * int) => int, e.g. Cantor's pairing function. Where is this formalised?

view this post on Zulip Mathias Fleury (May 03 2021 at 13:38):

like https://www.isa-afp.org/browser_info/current/AFP/Recursion-Theory-I/CPair.html?

view this post on Zulip Manuel Eberl (May 03 2021 at 13:43):

No need to turn to the AFP. You can use prod_encode/prod_decode from HOL-Library.Nat_Bijection. This is also used to prove the countability of products in HOL-Library.Countable.

view this post on Zulip Lukas Stevens (May 03 2021 at 13:44):

Thanks Manuel, I was hoping for something like that :D

view this post on Zulip Manuel Eberl (May 03 2021 at 13:45):

Unrelatedly, my favourite pairing function at least for theoretical purposes is (a,b)2a(2b+1)(a,b) \mapsto 2^a \cdot (2b+1). It's much easier to see why this is bijective, and it's very easy to invert as well. The drawback is that it is not as economic as the other one.

view this post on Zulip Lukas Stevens (May 03 2021 at 13:47):

For my application, the function does not have to be economic.

view this post on Zulip Manuel Eberl (May 03 2021 at 13:50):

Yes but still, it's easier to take the one that's already in the library.

view this post on Zulip Manuel Eberl (May 03 2021 at 13:51):

I just like telling people about the one above because it's neat and few people seem to know about it.

view this post on Zulip Manuel Eberl (May 03 2021 at 13:52):

By the way, if you're wondering how I found prod_encode: I knew about HOL-Library.Countable_Set and figured there has to be a pairing function in there somewhere, and I was right. :smile:

view this post on Zulip Lukas Stevens (May 03 2021 at 13:59):

Related question: are there any helpers for proving that combining bijective functions again yield a bijective function? Specifically, I am looking at the function (λ(a, b). int_decode (prod_encode (int_encode a, int_encode b))).

view this post on Zulip Lukas Stevens (May 03 2021 at 14:00):

I tried a bit and only managed to prove it by taking annoyingly small steps

view this post on Zulip Lukas Stevens (May 03 2021 at 14:04):

*prove parts of it (until now)

view this post on Zulip Manuel Eberl (May 03 2021 at 14:05):

Write it with as a composition of bijective functions with and map_prod:

lemma map_prod_bij:
  assumes "bij f" "bij g"
  shows   "bij (map_prod f g)"
  using assms unfolding bij_def by (intro conjI prod.inj_map map_prod_surj) auto

lemma "(λ(a, b). int_decode (prod_encode (int_encode a, int_encode b))) =
       int_decode ∘ prod_encode ∘ map_prod int_encode int_encode"
  by auto

lemma "bij (int_decode ∘ prod_encode ∘ map_prod int_encode int_encode)"
  by (intro map_prod_bij bij_comp bij_int_encode bij_prod_encode bij_int_decode)

view this post on Zulip Lukas Stevens (May 03 2021 at 14:10):

Thanks!


Last updated: Sep 25 2021 at 09:17 UTC