Referential transparency: Difference between revisions

Revision as of 12:12, 29 July 2023

Latest revision as of 02:11, 25 May 2025

(9 intermediate revisions by 7 users not shown)

Line 2:

{{About|referential transparency in programming language theory|its use in linguistics and philosophy|Opaque context}}

In [[analytic philosophy]] and [[computer science]], '''referential transparency''' and '''referential opacity''' are properties of linguistic constructions<ref>,{{efn|A linguistic construction (also called mode of containment, context, or operator) is an expression with holes.</ref>,}} and by extension of languages. A linguistic construction is called ''referentially transparent'' when for any expression built from it, [[Rewriting|replacing]] a subexpression with another one that [[Denotation|denotes]] the same value<ref>{{efn|Here a value is the denotation (also called meaning, object, or referent) of an expression, not the [[Expression (computer science)|result]] of the evaluation process.</ref>}} does not change the value of the expression.<ref name="quine1960">{{cite book |last=Quine |first=Willard Van Orman |author-link=Willard Van Orman Quine |date=1960 |title=Word and Object |edition=1st |url=https://archive.org/details/in.ernet.dli.2015.529086 |___location=Cambridge, Massachusetts |publisher=MIT Press |page=144 |isbn=978-0-262-17001-7}}</ref><ref name="strachey1967">{{cite techreporttech report |last1=Strachey |first1=Christopher |date=1967 |title=Fundamental Concepts in Programming Languages |url= |institution=Lecture notes for the International Summer School in Computer Programming at Copenhagen |number=}} Also: {{cite journal |last1=Strachey |first1=Christopher |date=2000 |title=Fundamental Concepts in Programming Languages |url=https://link.springer.com/article/10.1023%2FA%3A1010000313106 |journal=Higher-Order and Symbolic Computation |volume=13 |issue=1–2 |pages=11–49 |doi=10.1023/A:1010000313106 |s2cid=14124601 |doi-access=|url-access=subscription }}</ref> Otherwise, it is called ''referentially opaque''. 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.<ref name="whitehead1927">{{cite book |last1=Whitehead |first1=Alfred North |last2=Russell |first2=Bertrand |author-link1=Alfred North Whitehead |author-link2=Bertrand Russell |date=1927 |title=Principia Mathematica |volume=1 |edition=2nd |url=https://archive.org/details/dli.ernet.247278 |___location=Cambridge |publisher=Cambridge University Press |page=665 |isbn=978-0-521-06791-1}}</ref> For example, the linguistic construction ‘_ was wise’ is referentially transparent (e.g., ''Socrates was wise'' is equivalent to ''The founder of Western philosophy was wise'') but ‘_ said _’ is referentially opaque (e.g., ''Xenophon said ‘Socrates was wise’'' is not equivalent to ''Xenophon said ‘The founder of Western philosophy was wise’'').

Referential transparency, in programming languages, depends on thesemantic valuesequivalences associatedamong todenotations of expressions, thator on [[contextual equivalence]] of expressions themselves. That is, referential transparency depends on the semantics of the language. So, both [[declarative language]]s and [[imperative language]]s can behave referentially transparent orpositions, referentially opaque positions, or (usually) both, according to the semantics they are given.

The importance of referentialreferentially transparencytransparent positions is that itthey allowsallow the [[programmer]] and the [[compiler]] to reason about program behavior as a [[rewrite system]] at those positions. This can help in proving [[correctness (computer science)|correctness]], simplifying an [[algorithm]], assisting in modifying code without breaking it, or [[optimization (computer science)|optimizing]] code by means of [[memoization]], [[common subexpression elimination]], [[lazy evaluation]], or [[parallelization]].

== History ==

The concept originated in [[Alfred North Whitehead]] and [[Bertrand Russell]]'s ''[[Principia Mathematica]]'' (1910–1913):<ref name="whitehead1927" />

<blockquote>

A proposition as the vehicle orof truth or falsehood is a particular occurrence, while a proposition considered factually is a class of similar occurrences. It is the proposition considered factually that occurs in such statements as “''A'' believes ''p''“ and “''p'' is about ''A''.”

Of course it is possible to make statements about the particular fact “Socrates is Greek.” We may say how many centimetres long it is; we may say it is black; and so on. But these are not the statements that a philosopher or logician is tempted to make.

Line 33:

== 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-517505–517 |doi=10.1007/bf00277387}}</ref>

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

Line 40:

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''₁ ''e''₁) (*&lowast; ''e''₂ ''e''₂))}} is the place occupied by the first occurrence of {{mvarmath|{{var|e}}₂}}.

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''₁ … ''e''_''i''[''e′''/''p''] … ''e''_''n''>}} if {{math|''e'' ≡ <''Ω'' ''e''₁ … ''e''_''i'' … ''e''_''n''>}} else undefined, for all operators {{mvarmath|Ω}} and expressions {{mvarmath|{{var|e}}₁, …, {{mvarvar|e}}_{{{mvarvar|n}}}}}.

''Example.'' — If {{math|''e'' ≡ (+ (*&lowast; ''e''₁ ''e''₁) (*&lowast; ''e''₂ ''e''₂))}} then {{math|''e''[''e''₃/2.1] ≡ (+ (*&lowast; ''e''₁ ''e''₁) (*&lowast; ''e''₃ ''e''₂))}}.

Position {{mvar|p}} is ''purely referential'' in expression {{mvar|e}} is defined by

: {{math|1=''e''₁ = ''e''₂}} implies {{math|1=''e''[''e''₁/''p''] = ''e''[''e''₂/''p'']}}, for all expressions {{mvarmath|{{var|e}}₁, {{mvarvar|e}}₂}}.

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 {{mvarmath|Ω}} is ''referentially transparent'' in place {{mvar|i}} is defined by

: {{mvar|p}} is purely referential in {{mvar|e_''i''}} implies {{math|''i''.''p''}} is purely referential in {{math|''e'' ≡ <''Ω'' ''e''₁ … ''e''_''i'' … ''e''_''n''>}}, for all positions {{mvar|p}} and expressions {{mvarmath|{{var|e}}₁, …, {{mvarvar|e}}_{{{mvarvar|n}}}}}.

Otherwise {{mvarmath|Ω}} 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''.

Line 94:

* [[Liskov substitution principle]]

* [[Rewrite rule]]

==Notes==

{{notelist}}

== References ==