## 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

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

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

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: May 17 2021 at 16:26 UTC