Zulip Chat Archive

Stream: Is there code for X?

Topic: semidecidable


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Edward Ayers (Dec 12 2020 at 14:12):

ok, so I guess it's not in mathlib

view this post on Zulip Mario Carneiro (Dec 12 2020 at 14:13):

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

view this post on Zulip Edward Ayers (Dec 12 2020 at 14:13):

yeah that loses the semantics somewhat

view this post on Zulip Edward Ayers (Dec 12 2020 at 14:13):

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

view this post on Zulip Edward Ayers (Dec 12 2020 at 14:18):

I wonder how you would define real semidecidable

view this post on Zulip Mario Carneiro (Dec 12 2020 at 14:19):

I don't think synthetic semidecidability makes sense in lean

view this post on Zulip Mario Carneiro (Dec 12 2020 at 14:19):

you can of course define it using computability/ stuff

view this post on Zulip Mario Carneiro (Dec 12 2020 at 14:20):

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

view this post on Zulip Edward Ayers (Dec 12 2020 at 14:20):

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

view this post on Zulip 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

view this post on Zulip Edward Ayers (Dec 12 2020 at 14:30):

nice

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 12 2020 at 14:37):

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

view this post on Zulip Mario Carneiro (Dec 12 2020 at 14:39):

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

view this post on Zulip 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

view this post on Zulip Edward Ayers (Dec 12 2020 at 14:47):

Yeah which is why they have the subsingleton β constraint

view this post on Zulip Mario Carneiro (Dec 12 2020 at 14:48):

right

view this post on Zulip 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

view this post on Zulip Edward Ayers (Dec 12 2020 at 14:49):

jolly good

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 12 2020 at 14:52):

or type checking a term


Last updated: May 17 2021 at 16:26 UTC