Each expression built from a referentially opaque linguistic construction states something about a subexpression, whereas each expression built from a referentially transparent linguistic construction states something not about a subexpression, meaning that the subexpressions are ‘transparent’ to the expression, acting merely as ‘references’ to something else.
This can help in proving correctness, simplifying an algorithm, assisting in modifying code without breaking it, or optimizing code by means of memoization, common subexpression elimination, lazy evaluation, or parallelization.
The concept originated in Alfred North Whitehead and Bertrand Russell's Principia Mathematica (1910–1913):[3] A proposition as the vehicle of truth or falsehood is a particular occurrence, while a proposition considered factually is a class of similar occurrences.
The term appeared in its contemporary computer science usage in the discussion of variables in programming languages in Christopher Strachey's seminal set of lecture notes Fundamental Concepts in Programming Languages (1967):[2] One of the most useful properties of expressions is that called by Quine [4] referential transparency.
Any other features of the sub-expression, such as its internal structure, the number and nature of its components, the order in which they are evaluated or the colour of the ink in which they are written, are irrelevant to the value of the main expression.
There are three fundamental properties concerning substitutivity in formal languages: referential transparency, definiteness, and unfoldability.
— The ‘_ lives in _’ operator is referentially transparent: Indeed, the second position is purely referential in the assertion because substituting The capital of the United Kingdom for London does not change the value of the assertion.
— The ‘_ contains _’ and quote operators are referentially opaque: Indeed, the first position is not purely referential in the statement because substituting The capital of the United Kingdom for London changes the value of the statement and the quotation.
So in the first position, the ‘_ contains _’ and quote operators destroy the relation between an expression and the value that it denotes.
So in the first position, the ‘_ refers to _’ operator restores the relation between an expression and the value that it denotes.
A formal language is definite is defined by all the occurrences of a variable within its scope denote the same value.