Stream: Miscellaneous

Topic: Symbols for Leibniz, definitional, and syntactic equalities


view this post on Zulip Kazuhiko Sakaguchi (Nov 26 2021 at 02:29):

Are there any (standard) symbols for Leibniz, definitional, and syntactic equalities to distinguish in writing? Maybe =, ≡, and ≣ for each?

view this post on Zulip Meven Lennon-Bertrand (Nov 26 2021 at 10:06):

I fear this is not widely agreed upon… the Agda people often use \equiv for Leibnitz equality and == for the definitional one, while in Coq the tradition is rather the contrary.

view this post on Zulip Enrico Tassi (Nov 26 2021 at 10:21):

I suggest something =β=_\beta for conversion, and == for syntactic equality.
I don't think having to count the number of lines helps the reader, esp with small fonts

view this post on Zulip Pierre-Marie Pédrot (Nov 26 2021 at 10:23):

syntactic equality is actually α-conversion, so if you annotate conversion with β (which is only part of the rules btw) you should also annotate syntactic equality with α

view this post on Zulip Enrico Tassi (Nov 26 2021 at 10:23):

Also, I would use the small symbol for the most precise equality, and add sub/super scripts to include (quotient over) more staff, like computations or proofs

view this post on Zulip Enrico Tassi (Nov 26 2021 at 10:24):

ok, I consider α\alpha an error in the presentation of formal systems. It must be implicit, otherwise nothing makes sense

view this post on Zulip Enrico Tassi (Nov 26 2021 at 10:25):

but if you want, yes, =βα=_{\beta\alpha} and =α=_\alpha ...

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 10:54):

Agree with Enrico, I'd only mention alpha if you're dealing with (non-hygienic) metaprogramming like macros in your metatheory

view this post on Zulip Kenji Maillard (Nov 26 2021 at 10:55):

Though conversion (at least in Coq and Agda) contains much more than β\beta nowadays, no ?

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 10:56):

Yes, but please don't add the Greek alphabet to your subscripts by default :-|

view this post on Zulip Karl Palmskog (Nov 26 2021 at 10:56):

you can add a subscript regexp maybe? E.g., =_{[\alpha-\omega]}

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 10:56):

BTW, even the idea that propositional equality is Leibniz equality seems Coq-specific, I've never heard it in Agda (and I'm honestly a bit skeptical for Coq)

view this post on Zulip Pierre-Marie Pédrot (Nov 26 2021 at 10:59):

@Paolo Giarrusso what do you mean exactly? Do you call Leibniz equality something else? I think that it should be restricted to the impredicative encoding of equality, which is weaker than propositional equality without UIP, but that's just an opinion.

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 11:01):

I guess we're talking of the same encoding, and yes that's more clearly Leibniz

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 11:05):

actually, that opinion seems supported by the literature: https://homepages.inf.ed.ac.uk/wadler/papers/leibniz/leibniz.pdf proves Leibniz equality and identity types are isomorphic under a bunch of assumptions — hence, a priori, they must be different definitions.

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 11:06):

and to clarify for others: I assume Pierre-Marie's talking about such an encoding of Leibniz equality:

image.png

which seems much closer to what Leibniz said:

Leibniz asserted the identity of indiscernibles: two objects are equal if and only if they satisfy the same properties

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 11:08):

Ah, the identification has ~30 years of history in the Coq literature: > Further, it is well known that Leibniz equality (a =. b) implies Martin-Löf identity (a ≡ b) and vice versa. Indeed, the former is sometimes taken as the name of the latter (Pfenning & Paulin-Mohring, 1989; Coq Developers, 2017). Here, to avoid confusion, we stick to calling each by its own name as defined above.

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 11:08):

But TLDR: "propositional equality" is probably less ambiguous (and more common than "identity type" IMHO)

view this post on Zulip Stefan Monnier (Nov 26 2021 at 15:15):

BTW, I don't quite understand the OP's question: I'd understand it in a non-Coq-specific context when talking about the symbols used in a paper, but within Coq code, I can't quite see how I could even talk about an equality more discerning than Leibniz's. Unless we're talking about Coq code used to model some other system (or something like MetaCoq)?
What am I missing?

view this post on Zulip Kenji Maillard (Nov 26 2021 at 15:18):

I would expect the OP to be interested in metaprogramming (tactics) in Coq so the choice of equality is relevant (for performance/correctness/etc).

view this post on Zulip Enrico Tassi (Nov 26 2021 at 17:40):

wild guess: paper on https://github.com/math-comp/algebra-tactics

view this post on Zulip Kazuhiko Sakaguchi (Nov 29 2021 at 06:40):

Thanks for the useful comments. To be clear, my main purpose to use syntactic equality is unfolding notations.


Last updated: Aug 14 2022 at 11:02 UTC