Referential Transparency

The meaning of “referential transparency” differs between authors.

It seems to stem from Russel and Whitehead's “Principa Mathematica”, was then adopted by Quine (1960), then by Strachey (1967), and finally by different other authors.

Søndergaard and Sestof take the term to mean what Quine suggests: A form f(...) is referentially transparent, if its argument can be replaced by the argument's definition.

Søndergaard and Sestof suggest other names for similar but (in some cases) independed properties, which are sometimes also called "referential transparency" by individual authors.

These properties are as follows.

extensionality

To find the value of an expression, the only thing one needs to know about a subexpression is its (the subexpression's) value.

definiteness

A symbol (within the some context or scope) always stands for the same thing. (One needs to figure out the details of when exactly two contexts are considered the same context.)

substitutivity of identity

Any subexpression can be replaced by any other equal in value.

unfoldability

An application f(x) of a defined function f can be replaced by its instantiated right-hand side (definition).

Søndergaard and Sestof then show that most of these properties are independed of each other.

Søndergaard and Sestoft define a language Q₀ with a a predicate “@” for numerals. The language Q₀ is not referentially transparent, because @(1 − 0) ≠ @1.

Variables are indefinite: (λx.(x − x))(0 ⊓ 1) can give any value of {0, 1, #}, because “0 ⊓ 1” means "one of 0 or 1" and each x in “x − x” might evaluate to 0 or 1 (the language is indeterministic). Moreover, 0 − 1 is defined as # (i.e., “undefined”/“bottom”), because only the values 0 and 1 are possible.

Unfoldability does not apply. (λx.0)(0 - 1) gives #, because (0 - 1) gives # and the application is strict.

When “@” is redefined as the identity, a new language Q₁ is formed, which now is referentially transparent.

When normal order evaluation is used, a new language Q₂ is formed from Q₁, which has unfoldability.

When call time choice semantics are used, a new language Q₃ is formed, which has definiteness. (λx.(x − x))(0 ⊓ 1) now always gives 0, because the decision between 0 and 1 is made once for the whole lambda. However, this loses unfoldability, because ((0 ⊓ 1) − (0 ⊓ 1)) might be 0, 1, or #.

Giving up non-determinism, a language Q₄ is formed that has both definiteness and unfoldability.

Thus, the values for eterminacy, definiteness, unfoldability, and referential transparency, respectively are given for these languages as follows.

Q₀: no, no, no, no.

Q₁: no, no, no, yes.

Q₂: no, no, yes, yes.

Q₃: no, yes, no, yes.

Q₄: yes, yes, yes, yes.