Fengyun Liu

Referential transparency, definiteness and unfoldability

05 Oct 2016

Note: This is an exposition of the same name paper Referential transparency, definiteness and unfoldability by Harald Søndergaard and Peter Sestoft, published in Acta Informatica, 1990.

The paper by Søndergaard and Sestoft (1990) clarifies the important concept referential transparency in programming languages, which is usually taken granted by programmers and researchers.

Introduction

In philosophy, Quine initiated the concept referential transparency in Word and Object, though it can be traced back to Principia Mathematica. Usually, if two terms refer to the same object, then substituting one by the other in a sentence will not change the meaning of the original sentence. However, some systematic exceptions to the rule above aroused interests of philosophers and logicians, for example:

evening star = morning star
(1) 'evening star' contains the word 'evening'
(2) 'morning star' contains the word 'evening'

Bern = the capital of Switzerland
(3) Jim believes that Bern is a beautiful city
(4) Jim believes that the capital of Switzerland is a beautiful city

The sentence (1) and (2) are obviously different, while in (3) and (4), Jim may not know that Bern is the capital of Switzerland, thus the substitution changes the meaning of the sentence.

The computer scientist Stoy defines referential transparency as follows:

We use [referential transparency] to refer to the fact of mathematics which says: The only thing that matters about an expression is its value, and any sub-expression can be replaced by any other equal in value. Moreover, the value of an expression is, within certain limits, the same whenever it occurs. [Stoy, page 5]

This definition mentions three principles:

  • Principle of Extensionality
  • Principle of Definiteness
  • Leibniz’s Law (substitutivity of identity)

Extensionablity. The principle of extensionality says that the only thing that matters to an expression is its value. 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 it’s value.

Definiteness. It means that same variables have the same values, e.g., the x in the expression 3x^2 + 5x + 7 stands for the same thing. In the following imperative programs, the variable x is not definite, as they refer to different values:

x := x - 1; y := x;

However, mutation is not the only way to break definiteness, as we’ll see blow.

Leibniz’s Law (substitutivity of identity). It means that any expression can be replace by any other equal in value.

Unfoldability. In functional programming, there’s one further complication: substitutivity of identity doesn’t imply unfoldability. That is, (λ x. t) e and t [x → e] are not necessarily equivalent.

Stoy’s definition mixes several things together. For conceptual clarity, it’s suggested in the paper to follow the convention of philosophers to define referential transparency as substitutivity of identity, and distinguish it from other concepts, like extensionality, definiteness, unfoldability, etc.

A Simple Language

The language only has one variable x, in order to simplify the presentation.

t    ::=               0               constant
                       1               constant
                       x               variable
                       t - t           subtraction
                       @ t             number?
                       t | t           non-deterministic choice
                       f t             application
f    ::=               λ x. t          abstraction

Language Q0

D〚e〛= E〚e〛{#}
E〚0〛c = {0}
E〚1〛c = {1}
E〚x〛c = c
E〚e1 - e2〛c = { if v1 = # or v2 = # or v1 < v2 then #
                  else v1 - v2
                  |  v1 ∈ E〚e1〛c  and  v2 ∈ E〚e2〛c
                }
E〚@e〛c = if e ≡ 0 or e ≡ 1 then {1} else {0}
E〚e1 | e2〛c = E〚e1〛c ⋃ E〚e2〛c
E〚f e〛c = F〚f〛( E〚e〛c)
F〚λ x. e〛c = if c = {#] then {#} else (E〚e〛c) ⋃ ({#} ⋂ c)
  • This language is not referential transparent, due to the existence of the @ t operator, @1 - 0 ≠ @1.
  • Variables are not definite, as (λ x. x - x) (0 | 1) denotes {0, 1, #} rather than {0}.
  • Not unfoldable, as (λ x. 0) (0 - 1) denotes {#}, in contrast to {0} after unfolding.

Language Q1: Obtaining Referential Transparency

Make the following change to the denotational semantics:

E〚@e〛c = E〚e〛c

Now @1 - 0 and @1 have the same denotation.

Language Q2: Obtaining Unfoldability

Make the following change to the denotational semantics of Q1:

F〚λ x. e〛c = E〚e〛c

Now (λ x. 0) (0 - 1) denotes {0} both before and after unfolding.

Language Q3: Obtaining Definiteness at the Expense of Unfoldability

In presence of non-determinism, definiteness of variables and unfoldability cannot be satisfied at the same time. We can make the following change to the denotational semantics of Q2 to obtain definiteness at the expense of unfoldability :

F〚f e〛c = ⋃ {F〚f〛{v} where v ∈ E〚e〛c}

Now (λ x. x - x) (0 | 1) denotes {0}, instead of {0, 1, #}. However, unfold the term we get (0 | 1) - (0 | 1), which denotes {0, 1, #}, thus unfoldability doesn’t hold.

Language Q4: Obtaining both Definiteness and Unfoldability

Make the following change to the denotational semantics of Q3 to give up non-determinism:

E〚e1 | e2〛c = E〚e1〛c

References

  • Three Types of Referential Opacity, Richard Sharvy, Philosophy of Science, Vol. 39, No. 2 (Jun., 1972), pp. 153-161
  • What Is Referential Opacity?, J. M. Bell, Journal of Philosophical Logic, Vol. 2, No. 1 (Jan., 1973), pp. 155-180
  • Referential transparency, definiteness and unfoldability, H. Søndergaard, P. Sestoft - Acta Informatica, 1990
  • Denotational Semantics, Stoy J.E., MIT Press, 1977