Stream: Miscellaneous

Topic: Readings on equality relation

Evgeniy Shishkin (Jul 22 2020 at 11:38):

Hi! Do you have suggestions on what to read about an equality relation in a context of constructive logic: what it is, what kinds of equality relation are discovered so far, etc.

jco (Jul 22 2020 at 11:40):

Evgeniy Shishkin said:

Hi! Do you have suggestions on what to read about an equality relation in a context of constructive logic: what it is, what kinds of equality relation are discovered so far, etc.

I was thinking about asking this a couple days ago, glad someone else did. Reading up on this stuff there's a lot of discussion of Hott, JMeq (axiom K) etc...equality is big business

Evgeniy Shishkin (Jul 22 2020 at 11:49):

Yeah, Ideally, I would like to read some not at all shallow overview of an equality relation in different subfields of logic or math in general, with links to more a advanced reading. Thanks to the community, I am sure those guys - titans of thought - have a lot to suggest on this )

Alexander Gryzlov (Jul 22 2020 at 12:22):

I guess one could start from something like
http://kodu.ut.ee/%7Evarmo/tday-andu/chapman-slides.pdf Chapman, "A biased history of equality in type theory"

Alexander Gryzlov (Jul 22 2020 at 12:24):

it's a bit old so it ends on OTT and doesn't mention HoTT

Evgeniy Shishkin (Jul 22 2020 at 12:36):

Thanks! We leave the HoTT equality for breakfast.

Bas Spitters (Jul 22 2020 at 19:09):

We tried to make the HoTT book accessible, and I believe with some success...

Karl Palmskog (Jul 22 2020 at 19:25):

I remember skimming the HoTT book when it came out, but to me it was a mystery who it was for (i.e., accessible to whom, and for what purpose). So maybe one answer is: it has a modern discussion of equality in type theory.

Bas Spitters (Jul 22 2020 at 19:28):

Perhaps mostly accessible to mathematicians, but I'm told quite a few people have read it by them selves.

Karl Palmskog (Jul 22 2020 at 19:29):

For example, I think the page "About this book" is not really a description of what the book is or what it tries to accomplish.

Karl Palmskog (Jul 22 2020 at 19:39):

I guess I will have to wait for the "Practical HoTT" or "HoTT for computer scientists" book

Paolo Giarrusso (Jul 23 2020 at 13:07):

I will agree the HoTT book is much more accessible than the typical book for graduate mathematicians (even tho the topic is not easy). I will confess I have a modicum of intuition about topology (at a level between pop-sci/1st year math BSc), which is probably more than is common in CS.

Karl Palmskog (Jul 23 2020 at 13:11):

is there really any place for topology at all in a BS/MS level CS curriculum outside trivial overlaps with linear algebra, graph theory, etc.? My view is that there basically isn't (and this is the case in nearly all US/European universities I'm familiar with), so I think the HoTT book is not particularly CS-background-welcoming.

Paolo Giarrusso (Jul 23 2020 at 13:36):

I'm sure you are right and I'm suffering from a knowledge bias. There's nothing I dislike more than mathematicians who say "X is easy" when all they know is "I understand X intuitively". But at the risk of committing that same sin: IIRC the first chapters require nothing more than "rubber-sheet topology".
If there is a gap, I think the missing material can be made accessible even to (good) high-school students, if you're willing to be informal (and probably silently use classical reals).

jco (Jul 23 2020 at 14:53):

I feel like writing "hott for computer scientists" is a good way for some academic to get famous :)

but it's nice to hear that the topological knowledge necessary is not so intense

Hugo Herbelin (Jul 23 2020 at 14:56):

If ever useful, I may share my own recollection of what I understand about equality (this is a personal view and I'd actually be interested in feedback about it).

We can distinguish different strengths of equality:

• intensional equality: it equates programs which evaluate the same by beta-reduction (and iota, delta, zeta, fix, cofix, ...); it generally generates a confluent rewriting system (w/o critical pairs)
• eta-equality: it equates programs which observationally behave the same; it is decidable in the finite types (e.g. on boolean, on finite products), but it is undecidable in the infinite cases (e.g. on natural numbers, on streams, ...); actually, the undecidability of eta-equality is the very reason why proofs are not machine-inferable in general, otherwise, any statement would be checkable just by testing that it is true on all inputs; it is unclear whether we can canonically associate to higher-inductive types an eta-equality but it would suspectingly be undecidable for most of them (starting with the circle)
• extensional (or observational) equality coincides with eta-equality on positive types (such as sums, products, Boolean, ...) but not in the case of functions or types:
  • in the case of functions, it is pointwise equality and it is equivalent to eta for functions + the ξ-rule which says that x ⊢ t = u implies ⊢ λx.t = λx.u
  • in the case of types, equality is equivalence (in the HoTT sense).

Here are a few properties of an equality:

• an equality is strict if any two proofs of equality are themselves equal (see UIP or axiom K)
• an equality is non-strict (or relevant) if there are provably disjoint proofs of equality of the same equality; this is typically the case of equality in the presence of univalence (= extensionality of types), since then, there are two distinct proofs of Bool = Bool (the identity and the negation).

The structure of equality proofs gives rise to:

• "homotopic" equality, also called weak equality in the context of category theory: it is an equality which supports a rich algebraic structure of equality of equality proofs, and of equality of proofs of equality proofs, etc.; in practice, from a syntactic point of view, we have actually no other choice than to work with a "homotopic" equality, because, in a syntactic view, the reflexivity, or symmetry, or transitivity of equality proofs are terms themselves, and trans p (trans q r) is syntactically different from trans (trans p q) r and we need to write an explicit proof term of the equality of trans p (trans q r) = trans (trans p q) r, and recursively, and there are different provably equal but not syntactically equal proofs of this latter statement. So, what really matters is whether the equality up to equality (and recursively in further nestings of equality) is strict or not, and if strict, whether there is a decidable subset of it that could be managed automatically at the meta-level in a proof assistant.

Indeed, there are also interactions between the equality of a theory as a proposition and the (meta)equality of the metatheory:

• judgemental equality, in the context of Martin-Löf's type theory, also called conversion in the context of Pure Type Systems, also called "equality on the nose" in the context of set theory, is used to quotient terms and types at the metalevel by a subset of strict equality.
  It can be typed or not, decidable or not:

  • in practice, the terminology "judgemental" is generally used when it is typed and when decidability does not care
  • the terminology "conversion" is generally used when it is untyped and decidable (as in Coq)

  Its extent can also vary:

  • it can includes all of strict equality, as in so-called Extensional Type Theory (as e.g. in NuPrl or Andromeda, but to some extent, this is also an extensional equality which we find in set theory, even if it has no nested dependency and proofs of equality are thus invisible anyway)
  • or it can cover only a decidable subset of strict equality (as is the case for Coq, basic Agda, ...)
  • or it can include a larger decidable subset of strict equality, as in the Calculus of Algebraic Constructions (see also CoqMT or Agda extended with rewriting rules, ...)

• by contrast, equality as a connective is called propositional (and, of course, it includes the judgemental quotient).

In another direction, we can make a difference between:

• an homogeneous equality (also called globular since it corresponds to a globular shape in geometry) which is when the comparison is between objects of the same type
• cubical equality (also called path equality in the context of cubical type theory, also called sometimes equality over in a categorical context) is an equality between objects in types which are themselves provably equal
• heterogeneous equality (aka John Major equality) was an equality useful in type theory to compare objects in non judgementally equal types; in practice, the types are often nevertheless provably equal (as e.g. in vec (n+m) = vec (m+n)) and it has the drawback that it has to be strict (i.e. it requires UIP); so, in my opinion, John Major equality is nowadays advantageously replaced by cubical equality, which is also an heterogeneous equality.

Karl Palmskog (Jul 23 2020 at 15:43):

@Hugo Herbelin can I post (reproduce) this on the Coq wiki? I think some of the non-Coq-using students in my group should read this

Hugo Herbelin (Jul 23 2020 at 17:22):

Sure. I realize that I forgot to mention also definitional equality (an oriented synonym of intensional as far as I can judge), ad hoc polymorphic equality (as in cubical or observational type theory), identity type, but I can add it afterwards. I may also try to compare with (e.g.) https://ncatlab.org/nlab/show/equality.

Karl Palmskog (Jul 23 2020 at 18:38):

https://github.com/coq/coq/wiki/Equality -- initial version, I might polish a bit more at some later point

Karl Palmskog (Jul 23 2020 at 18:38):

I would probably add setoids on the one hand and bisimilarity on infinite coinductive types on the other hand

Karl Palmskog (Jul 23 2020 at 18:47):

Per Chlipala's CPDT, there will always eventually be another member of the equality zoo:

researchers are actively investigating new definitions of what it means for two terms to be equal.

Paolo Giarrusso (Jul 24 2020 at 22:49):

I’m used to definitional and judgmental being equivalent (in ITT); where I‘ve seen a distinction, definitional equality stayed decidable

Last updated: Oct 08 2024 at 15:02 UTC