Maths - Computational Equality


from Wikipedia:

As an example we could take the natural numbers with the following term rewriting rules:

  1. A + 0 -> A
  2. A + S (B) -> S (A + B)
  3. A * 0 -> 0
  4. A * S (B) -> A + (A * B)

abstract reduction system, (abbreviated ARS)

An object x in A is called reducible if there exists some other y in A such that x -> y otherwise it is called irreducible or a normal form.

An object y is called a normal form of x if x -> ∗ y, and y is irreducible. If x has a unique normal form, then this is usually denoted with x ↓. In example 1 above, c is a normal form, and c = a ↓ = b ↓ . If every object has at least one normal form, the ARS is called normalizing.

Referential Transparency

from Wikipedia:

An expression is called referentially transparent if it can be replaced with its corresponding value without changing the program's behavior

If all functions involved in the expression are pure functions, then the expression is referentially transparent.

In languages with no side-effects, like Haskell, we can substitute equals for equals: i.e. if x == y then f(x) == f(y). This is a property also known as indistinguishable identicals, see Identity of indiscernibles. Such properties need not hold in general for languages with side-effects. Even so it is important to limit such assertions to so-called judgmental equality, that is the equality of the terms as tested by the system, not including user-defined equivalence for types.

For instance, if B f(A x) and the type A has overridden the notion of equality, e.g. making all terms equal, then it is possible to have x == y and yet find f(x) != f(y). This is because systems like Haskell do not verify that functions defined on types with user-defined equivalence relations be well-defined with respect to that equivalence. Thus the referential transparency is limited to types without equivalence relations. Extending referential transparency to user-defined equivalence relations can be done for example with a Martin-Lof identity type, but requires a dependently typed system such as in Agda, Coq or Idris.

Category Theory - Pullback as Substitution

Usually pullback is only defined upto isomorphism so we can't fully represent pullback as substitution. How do we define pullbacks so we can use the strict laws of substitution? This is a coherence problem.



metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

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.

flag flag flag flag flag flag 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.


Terminology and Notation

Specific to this page here:


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.