Movatterモバイル変換


[0]ホーム

URL:


Jump to content
WikipediaThe Free Encyclopedia
Search

Referential transparency

From Wikipedia, the free encyclopedia
Whether a program behaves differently if expressions and their values are interchanged
This article is about referential transparency in programming language theory. For its use in linguistics and philosophy, seeOpaque context.

Inanalytic philosophy andcomputer science,referential transparency andreferential opacity are properties of linguistic constructions,[a] and by extension of languages. A linguistic construction is calledreferentially transparent when for any expression built from it,replacing a subexpression with another one thatdenotes the same value[b] does not change the value of the expression.[1][2] Otherwise, it is calledreferentially 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.[3] For example, the linguistic construction ‘_ was wise’ is referentially transparent (e.g.,Socrates was wise is equivalent toThe founder of Western philosophy was wise) but ‘_ said _’ is referentially opaque (e.g.,Xenophon said ‘Socrates was wise’ is not equivalent toXenophon said ‘The founder of Western philosophy was wise’).

Referential transparency, in programming languages, depends on semantic equivalences among denotations of expressions, or oncontextual equivalence of expressions themselves. That is, referential transparency depends on the semantics of the language. So, bothdeclarative languages andimperative languages can have referentially transparent positions, referentially opaque positions, or (usually) both, according to the semantics they are given.

The importance of referentially transparent positions is that they allow theprogrammer and thecompiler to reason about program behavior as arewrite system at those positions. This can help in provingcorrectness, simplifying analgorithm, assisting in modifying code without breaking it, oroptimizing code by means ofmemoization,common subexpression elimination,lazy evaluation, orparallelization.

History

[edit]

The concept originated inAlfred North Whitehead andBertrand Russell'sPrincipia 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. It is the proposition considered factually that occurs in such statements as “A believesp“ and “p is aboutA.”

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.

When an assertion occurs, it is made by means of a particular fact, which is an instance of the proposition asserted. But this particular fact is, so to speak, “transparent”; nothing is said about it, but by means of it something is said about something else. It is this “transparent” quality that belongs to propositions as they occur in truth-functions. This belongs top whenp is asserted, but not when we say “p is true.”

It was adopted in analytic philosophy inWillard Van Orman Quine'sWord and Object (1960):[1]

When a singular term is used in a sentence purely to specify its object, and the sentence is true of the object, then certainly the sentence will stay true when any other singular term is substituted that designates the same object. Here we have a criterion for what may be calledpurely referential position: the position must be subject to thesubstitutivity of identity.

[…]

Referential transparency has to do with constructions (§ 11); modes of containment, more specifically, of singular terms or sentences in singular terms or sentences. I call a mode of containmentφ referentially transparent if, whenever an occurrence of a singular termt is purely referential in a term or sentenceψ(t), it is purely referential also in the containing term or sentenceφ(ψ(t)).

The term appeared in its contemporary computer science usage in the discussion ofvariables inprogramming languages inChristopher Strachey's seminal set of lecture notesFundamental Concepts in Programming Languages (1967):[2]

One of the most useful properties of expressions is that called by Quine [4]referential transparency. In essence this means that if we wish to find the value of an expression which contains a sub-expression, the only thing we need to know about the sub-expression is its value. 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.

Formal definitions

[edit]

There are three fundamental properties concerning substitutivity in formal languages: referential transparency, definiteness, and unfoldability.[4]

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

Referential transparency

[edit]

Aposition 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(+ (∗e1e1) (∗e2e2)) is the place occupied by the first occurrence ofe2.

Expressionewith expressione′inserted at positionp is denoted bye[e′/p] and defined by

e[e′/ε] ≡e′
e[e′/i.p] ≡ <Ωe1ei[e′/p] …en> ife ≡ <Ωe1eien> else undefined, for all operatorsΩ and expressionse1, …,en.

Example. — Ife ≡ (+ (∗e1e1) (∗e2e2)) thene[e3/2.1] ≡ (+ (∗e1e1) (∗e3e2)).

Positionp ispurely referential in expressione is defined by

e1 =e2 impliese[e1/p] =e[e2/p], for all expressionse1,e2.

In other words, a position is purely referential in an expression if and only if it is subject to the substitutivity of equals.ε is purely referential in all expressions.

OperatorΩ isreferentially transparent in placei is defined by

p is purely referential inei impliesi.p is purely referential ine ≡ <Ωe1eien>, for all positionsp and expressionse1, …,en.

OtherwiseΩ isreferentially opaque in placei.

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

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

Example. — The ‘_ lives in _’ operator is referentially transparent:

She lives in London.

Indeed, the second position is purely referential in the assertion because substitutingThe capital of the United Kingdom forLondon 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 substitutingThe capital of the United Kingdom forLondon 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 substitutingThe capital of the United Kingdom forLondon 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

[edit]

A formal language isdefinite is defined by all the occurrences of a variable within its scope denote the same value.

Example. — Mathematics is definite:

3x2 + 2x + 17.

Indeed, the two occurrences ofx denote the same value.

Unfoldability

[edit]

A formal language isunfoldable is defined by all expressions areβ-reducible.

Example. — Thelambda calculus is unfoldable:

((λx.x + 1) 3).

Indeed,((λx.x + 1) 3) = (x + 1)[3/x].

Relations between the properties

[edit]

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.

See also

[edit]

Notes

[edit]
  1. ^A linguistic construction (also called mode of containment, context, or operator) is an expression with holes.
  2. ^Here a value is the denotation (also called meaning, object, or referent) of an expression, not theresult of the evaluation process.

References

[edit]
  1. ^abQuine, Willard Van Orman (1960).Word and Object (1st ed.). Cambridge, Massachusetts: MIT Press. p. 144.ISBN 978-0-262-17001-7.{{cite book}}:ISBN / Date incompatibility (help)
  2. ^abStrachey, Christopher (1967).Fundamental Concepts in Programming Languages (Technical report). Lecture notes for the International Summer School in Computer Programming at Copenhagen. Also:Strachey, Christopher (2000)."Fundamental Concepts in Programming Languages".Higher-Order and Symbolic Computation.13 (1–2):11–49.doi:10.1023/A:1010000313106.S2CID 14124601.
  3. ^abWhitehead, Alfred North;Russell, Bertrand (1927).Principia Mathematica. Vol. 1 (2nd ed.). Cambridge: Cambridge University Press. p. 665.ISBN 978-0-521-06791-1.{{cite book}}:ISBN / Date incompatibility (help)
  4. ^Søndergaard, Harald; Sestoft, Peter (1990)."Referential Transparency, Definiteness and Unfoldability"(PDF).Acta Informatica.27 (6):505–517.doi:10.1007/bf00277387.

External links

[edit]
Retrieved from "https://en.wikipedia.org/w/index.php?title=Referential_transparency&oldid=1292073897"
Category:
Hidden categories:

[8]ページ先頭

©2009-2025 Movatter.jp