Stream: General

Topic: Symbol for equivalence


view this post on Zulip Lukas Stevens (Mar 18 2020 at 11:02):

Since ≡ is already taken, what would be the canonical symbol to use for equivalence (specifically a conversion)?

view this post on Zulip Manuel Eberl (Mar 18 2020 at 11:07):

equivalence of what?

view this post on Zulip Lukas Stevens (Mar 18 2020 at 11:10):

Equivalence of two terms in propositional logic.

view this post on Zulip Josh Chen (Mar 18 2020 at 11:13):

Is there a specific context? Rewriting? Logical equivalence? Some arbitrary equivalence relation?

view this post on Zulip Lukas Stevens (Mar 18 2020 at 11:14):

It's rewriting based. I want to represent Isabelle/ML conversions in HOL.

view this post on Zulip Manuel Eberl (Mar 18 2020 at 11:15):

First of all, you should think about whether you need notation for this at all

view this post on Zulip Manuel Eberl (Mar 18 2020 at 11:16):

if you do, I guess you could do something like ≡ with an aptly chosen index

view this post on Zulip Lukas Stevens (Mar 18 2020 at 11:18):

Ah right, I forgot about indexing. I do think that it is necessary because I also need a proof system (with proof terms that are a HOL datatype) that certifies those conversions.

view this post on Zulip Manuel Eberl (Mar 18 2020 at 11:19):

So?

view this post on Zulip Lukas Stevens (Mar 18 2020 at 11:21):

Sorry, I misunderstood you. The notation is of course not necessary. But it is nice for presentation.

view this post on Zulip Manuel Eberl (Mar 18 2020 at 11:27):

Then consider deleting it after you're done

view this post on Zulip Manuel Eberl (Mar 18 2020 at 11:27):

or making it optionally possible to enable/disable it with bundles

view this post on Zulip Manuel Eberl (Mar 18 2020 at 11:28):

syntax is global and in my opinion people tend to overuse custom syntax

view this post on Zulip Manuel Eberl (Mar 18 2020 at 11:28):

that's okay if your stuff is unlikely to ever be used by other developments, but otherwise it can be problematic

view this post on Zulip Manuel Eberl (Mar 18 2020 at 11:29):

e.g. there are about three different theories in Isabelle that use "$" as a binary operator

view this post on Zulip Manuel Eberl (Mar 18 2020 at 11:29):

if you import more than one of them at the same time, all hell breaks loose

view this post on Zulip Lukas Stevens (Mar 18 2020 at 11:51):

Thanks, I will definitely keep that in mind for when it comes to that point :D


Last updated: Sep 25 2022 at 23:25 UTC