18
$\begingroup$

This answer to this question about η-equivalence in Coq draws a distinction between judgmental equality and definitional equality.

In the simply typed lambda calculus (henceforth STLC), the following is an example of a typing rule.

$$ \frac{\Gamma \vdash t_1 : \alpha \to \beta \;\; \text{and} \;\; \Gamma \vdash t_2 : \alpha}{\Gamma \vdash t_1(t_2) : \beta } \;\; \text{is modus ponens} $$

In my understanding, $t_1 : \alpha \to \beta$ is a typing judgment.

STLC can be formalized using typing judgments exclusively.

Judgmental equality is slightly more confusing.

Does it refer to a new type of judgment such as $t_1 = t_2$ for terms and $\alpha_1 = \alpha_2$ for types, as described here?

I think an equality type is just a type $t_3 : \alpha \equiv \beta$ that can be inhabited or not like any other type.

Assuming the above is true, then, I'm not sure what definitional equality would be.

$\endgroup$
2
  • $\begingroup$ This is a very good and frequently asked question. It actually reveals some fundamental design principles for type theories. (+1) $\endgroup$
    – Trebor
    Feb 10 at 16:42
  • 2
    $\begingroup$ It might also be worth comparing and contrasting judgemental equality to the equational theory of the language, though maybe that should be done as an answer to a separate question. $\endgroup$
    – mudri
    Feb 10 at 18:12

2 Answers 2

13
$\begingroup$

This answer to this question about η-equivalence in Coq draws a distinction between judgmental equality and definitional equality.

This is an incorrect attribute to the answer you linked to. Sarah didn't say that judgmental equality is distinct from definitional equality. I suggest reading that answer again.

Judgmental equality usually means the fact that two terms are semantically exactly the same (in other words, they share the same "semantical object"). Definitional equality is a synonym of judgmental equality.

Equality types are types that encode certain equality, or "witness" certain equality. Usually, an equality type is parameterized by two terms (and maybe something else), where every instance of such type is a proof that these two terms satisfy an equality. Equality relations encoded in an equality type are usually called "propositional equality". There can be different equality relations encoded by different equality types, depending on the exact definition of the equality types. In my impression, they're mostly stronger than the mathematical sense of equivalence relation (binary relation that is refl, sym, and trans).

Obviously, judgmental equality implies propositional equality (check!), but the reverse direction is not true. In case the reverse is true, we usually refer to the type theory as an extensional type theory, with the reverse known as 'equality reflection'.

$\endgroup$
1
  • 2
    $\begingroup$ Underrated anwser! $\endgroup$ Feb 10 at 22:13
11
$\begingroup$

Nick de Bruijn invented the distinction between "definitional equality" and "book equality" in:

  • Bruijn, de, N. G. (1975). Set theory with type restrictions. In A. Hajnal, R. Rado, & V. T. Sos (Eds.), Infinite and finite sets : to Paul Erdõs on his 60th birthday, vol.1 (pp. 205-214). (Colloquia Mathematica Societatis János Bolyai; Vol. 10). North-Holland Publishing Company. Eprint

Basically, two terms (or two types) are "definitional equivalent" $t_{1}=_{d}t_{2}$ if they can be transformed into the same term $t$ by definitional expansion, beta reduction, and eta expansion.

Book equality, or propositional equality, is a type $eq(-,-)$ parametrized by two terms of the same type $t_{1} : A$, $t_{2} : A$, satisfying the familiar identities of equality (reflexivity, transitivity, etc.). Usually this is the equality you're thinking of in mathematics.

See also:

  • Thierry Coquand, Nils Anders Danielsson, "Isomorphism is Equality" Eprint
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.