Stream: General

Topic: Symbol for equivalence

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)?

Manuel Eberl (Mar 18 2020 at 11:07):

equivalence of what?

Lukas Stevens (Mar 18 2020 at 11:10):

Equivalence of two terms in propositional logic.

Josh Chen (Mar 18 2020 at 11:13):

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

Lukas Stevens (Mar 18 2020 at 11:14):

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

Manuel Eberl (Mar 18 2020 at 11:15):

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

Manuel Eberl (Mar 18 2020 at 11:16):

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

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.

So?

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.

Manuel Eberl (Mar 18 2020 at 11:27):

Then consider deleting it after you're done

Manuel Eberl (Mar 18 2020 at 11:27):

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

Manuel Eberl (Mar 18 2020 at 11:28):

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

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

Manuel Eberl (Mar 18 2020 at 11:29):

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

Manuel Eberl (Mar 18 2020 at 11:29):

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

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: Aug 15 2022 at 02:13 UTC