Maths - Definitional Equality

Equality Of Types

 Equality can be defined in different ways, in some cases we need things to be considered equal only when they are defined in exactly the same way, in other cases we need a looser form of equality where things may be defined differently but behave the same in some way.

This page discusses definitional equality, for a more general discussion of other types of equality see the page here.

Definitional Equality

More exact equality happens when the terms are both defined in exactly the same way. The name 'definitional equality' usually allows the terms to be 'normalised' before comparing them. This means that any functions can be applied to expressions, if this reduces them.

Computational (Judgemental) Equality

Equality based on conversion or reduction rules.

Example are:

• “(λx.x+x)2” and “2+2” (β-reduction)
• “2+2” (s(s(0))+s(s(0)) reduces to “4” (s(s(s(s(0)))).

This is commonly included in definitional equality

Notes

Those equalities that are given as rewrite rules (equations) or else originate from general functional principles ( β, η, etc.) - Queiroz, Oliveira.

For 'Homotopy Type Theory' book type theory is a deductive system based on two forms of judgment:

Judgment Meaning
a:A a is an object of type A
ab : A a and b are definitionally equal objects of type A

Definitional equality is a syntactical notion and it has nothing to do with the meaning of the syntactical entries - Nordstrom, Petersson, Smith

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.