Editing Referential transparency (section)

== Formal definitions ==
There are three fundamental properties concerning substitutivity in formal languages: referential transparency, definiteness, and unfoldability.<ref name="sondergaard1990">{{cite journal |last1=Søndergaard |first1=Harald |last2=Sestoft |first2=Peter |date=1990 |title=Referential Transparency, Definiteness and Unfoldability |url=http://www.itu.dk/people/sestoft/papers/SondergaardSestoft1990.pdf |journal=Acta Informatica |volume=27 |issue=6 |pages=505–517 |doi=10.1007/bf00277387}}</ref>

Let’s denote syntactic equivalence with ≡ and semantic equivalence with =.

=== Referential transparency ===
A ''position'' is defined by a sequence of natural numbers. The empty sequence is denoted by ε and the sequence constructor by ‘.’.

''Example.'' — Position 2.1 in the expression {{math|(+ (&lowast; ''e''<sub>1</sub> ''e''<sub>1</sub>) (&lowast; ''e''<sub>2</sub> ''e''<sub>2</sub>))}} is the place occupied by the first occurrence of {{math|{{var|e}}<sub>2</sub>}}.

Expression {{mvar|e}} ''with'' expression {{mvar|e′}} ''inserted at'' position {{mvar|p}} is denoted by {{math|''e''[''e′''/''p'']}} and defined by
: {{math|''e''[''e′''/ε] ≡ ''e′''}}
: {{math|''e''[''e′''/''i''.''p''] ≡ <Ω ''e''<sub>1</sub> … ''e''<sub>''i''</sub>[''e′''/''p''] … ''e''<sub>''n''</sub>>}} if {{math|''e'' ≡ <Ω ''e''<sub>1</sub> … ''e''<sub>''i''</sub> … ''e''<sub>''n''</sub>>}} else undefined, for all operators {{math|Ω}} and expressions {{math|{{var|e}}<sub>1</sub>, …, {{var|e}}<sub>{{var|n}}</sub>}}.

''Example.'' — If {{math|''e'' ≡ (+ (&lowast; ''e''<sub>1</sub> ''e''<sub>1</sub>) (&lowast; ''e''<sub>2</sub> ''e''<sub>2</sub>))}} then {{math|''e''[''e''<sub>3</sub>/2.1] ≡ (+ (&lowast; ''e''<sub>1</sub> ''e''<sub>1</sub>) (&lowast; ''e''<sub>3</sub> ''e''<sub>2</sub>))}}.

Position {{mvar|p}} is ''purely referential'' in expression {{mvar|e}} is defined by
: {{math|1=''e''<sub>1</sub> = ''e''<sub>2</sub>}} implies {{math|1=''e''[''e''<sub>1</sub>/''p''] = ''e''[''e''<sub>2</sub>/''p'']}}, for all expressions {{math|{{var|e}}<sub>1</sub>, {{var|e}}<sub>2</sub>}}.
In other words, a position is purely referential in an expression if and only if it is subject to the substitutivity of equals. {{mvar|ε}} is purely referential in all expressions.

Operator {{math|Ω}} is ''referentially transparent'' in place {{mvar|i}} is defined by
: {{mvar|p}} is purely referential in {{mvar|e<sub>''i''</sub>}} implies {{math|''i''.''p''}} is purely referential in {{math|''e'' ≡ <Ω ''e''<sub>1</sub> … ''e''<sub>''i''</sub> … ''e''<sub>''n''</sub>>}}, for all positions {{mvar|p}} and expressions {{math|{{var|e}}<sub>1</sub>, …, {{var|e}}<sub>{{var|n}}</sub>}}.
Otherwise {{math|Ω}} is ''referentially opaque'' in place {{mvar|i}}.

An operator is ''referentially transparent'' is defined by it is referentially transparent in all places. Otherwise it is ''referentially opaque''.

A formal language is ''referentially transparent'' is defined by all its operators are referentially transparent. Otherwise it is ''referentially opaque''.

''Example.'' — The ‘_ lives in _’ operator is referentially transparent:
: ''She lives in London.''
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 first position is also purely referential for the same substitutivity reason.

''Example.'' — The ‘_ contains _’ and quote operators are referentially opaque:
: ''‘London’ contains six letters.''
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.

''Example.'' — The ‘_ refers to _’ operator is referentially transparent, despite the referential opacity of the quote operator:
: ''‘London’ refers to the largest city of the United Kingdom.''
Indeed, the first position is purely referential in the statement, though it is not in the quotation, because substituting ''The capital of the United Kingdom'' for ''London'' does not change the value of the statement. So in the first position, the ‘_ refers to _’ operator restores the relation between an expression and the value that it denotes. The second position is also purely referential for the same substitutivity reason.

=== Definiteness ===
A formal language is ''definite'' is defined by all the occurrences of a variable within its scope denote the same value.

''Example.'' — Mathematics is definite:
: {{math|3''x''<sup>2</sup> + 2''x'' + 17}}.
Indeed, the two occurrences of {{mvar|x}} denote the same value.

=== Unfoldability ===
A formal language is ''unfoldable'' is defined by all expressions are [[Lambda calculus|β-reducible]].

''Example.'' — The [[lambda calculus]] is unfoldable:
: {{math|((λ''x''.''x'' + 1) 3)}}.
Indeed, {{math|1=((λ''x''.''x'' + 1) 3) = (''x'' + 1)[3/''x'']}}.

=== Relations between the properties ===
Referential transparency, definiteness, and unfoldability are independent.
Definiteness implies unfoldability only for deterministic languages.
Non-deterministic languages cannot have definiteness and unfoldability at the same time.