Zulip Chat Archive

Stream: new members

Topic: decidable_eq with functions


view this post on Zulip Marcus Rossel (Dec 29 2020 at 17:56):

Why is equality of functions not decidable?

view this post on Zulip Johan Commelin (Dec 29 2020 at 18:15):

Doesn't that depend on from where and to where the functions go?

view this post on Zulip Kevin Buzzard (Dec 29 2020 at 18:21):

import tactic

instance : decidable_eq (bool  bool) := by apply_instance

view this post on Zulip Rob Lewis (Dec 29 2020 at 18:21):

For the nat -> bool case: let fn(k)=Tf_n(k) = T iff Turing machine nn halts in at most kk steps. If you could decide fn=λk,Ff_n = \lambda k, F you'd decide the halting problem.

view this post on Zulip Kevin Buzzard (Dec 29 2020 at 18:22):

https://xenaproject.wordpress.com/2019/06/11/the-inverse-of-a-bijection/

view this post on Zulip Eric Wieser (Dec 29 2020 at 22:40):

I assume there is a docs#decidable_eq instance for arguments with fintype inputs and decidable_eq outputs?


Last updated: May 09 2021 at 20:11 UTC