Zulip Chat Archive

Stream: Is there code for X?

Topic: semidecidable

Edward Ayers (Dec 12 2020 at 14:02):

I don't think semidecidable is quite the right word but I want the decidable equivalent of option: 

inductive semidecidable (P : Prop) : Type
|  yes : P → semidecidable
| idk : semidecidable

Mario Carneiro (Dec 12 2020 at 14:11):

I have proposed this before, with the same name, so I think that's evidence for its naturalness even though it's technically incorrect

Edward Ayers (Dec 12 2020 at 14:12):

ok, so I guess it's not in mathlib

Mario Carneiro (Dec 12 2020 at 14:13):

nope, not unless you are happy with option (plift p)

Edward Ayers (Dec 12 2020 at 14:13):

yeah that loses the semantics somewhat

Edward Ayers (Dec 12 2020 at 14:13):

ok cool I'll just add it at the top of my file

Edward Ayers (Dec 12 2020 at 14:18):

I wonder how you would define real semidecidable

Mario Carneiro (Dec 12 2020 at 14:19):

I don't think synthetic semidecidability makes sense in lean

Mario Carneiro (Dec 12 2020 at 14:19):

you can of course define it using computability/ stuff

Mario Carneiro (Dec 12 2020 at 14:20):

but this isn't going to reflect into a kernel decision procedure

Edward Ayers (Dec 12 2020 at 14:20):

yeah I couldn't think what it would be without using computability

Mario Carneiro (Dec 12 2020 at 14:26):

A simple example of a semidecision procedure is nat.find. It has the type (\ex n : nat, p n) -> {n | p n} where p is a decidable proposition. The sense in which this is complete is that if the algorithm terminates, then \ex n : nat, p n; but we knew that already, it's a precondition. In the traditional definition we would say that if the property fails to hold then the algorithm does not terminate, but in lean's case there's no algorithm in that regime at all

Edward Ayers (Dec 12 2020 at 14:30):

nice

Edward Ayers (Dec 12 2020 at 14:33):

I was daydreaming that you could have a VM override for semidecidable a = b which checks if the VM objects are the same but the code as written in Lean always returns idk. Although that might just be confusing.

Mario Carneiro (Dec 12 2020 at 14:34):

Also, this kind of object comes up in the pointer equality test in the lean 4 "pointer-based optimizations" paper

Mario Carneiro (Dec 12 2020 at 14:37):

does this look familiar? (p.12 of https://arxiv.org/pdf/2003.01685.pdf)

inductive PtrEqResult (x y : α) : Type
| unknown  : PtrEqResult
| yesEqual : x = y → PtrEqResult

Mario Carneiro (Dec 12 2020 at 14:37):

although in their case they are really returning a trunc (semidecidable (x = y))

Mario Carneiro (Dec 12 2020 at 14:39):

so actually I guess your daydream already exists in lean 4 by another name

Mario Carneiro (Dec 12 2020 at 14:40):

Note that it is unsound to actually have the primitive return semidecidable (x = y), because you can use it to detect if you are running in the logic or as compiled code, and do something evil in the second case

Edward Ayers (Dec 12 2020 at 14:47):

Yeah which is why they have the subsingleton β constraint

Mario Carneiro (Dec 12 2020 at 14:48):

right

Mario Carneiro (Dec 12 2020 at 14:48):

it's not necessary to write it in continuation passing style though, if you have trunc and subsingleton

Edward Ayers (Dec 12 2020 at 14:49):

jolly good

Edward Ayers (Dec 12 2020 at 14:50):

I'm asking about it because I effectively sneak in a pointer-eq check in widgets (which is fine because it's all in meta mode anyway). But I was thinking about how to implement in Lean 4 but looks like they've got my case covered

Mario Carneiro (Dec 12 2020 at 14:51):

I think it's also useful for general decision procedures where you can't be bothered to prove the converse, for example equality in a random ring

Mario Carneiro (Dec 12 2020 at 14:52):

or type checking a term

Last updated: Dec 20 2023 at 11:08 UTC