Rewriting
from Wikipedia:
As an example we could take the natural numbers with the following term rewriting rules:
- A + 0 -> A
- A + S (B) -> S (A + B)
- A * 0 -> 0
- 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.
see:
