In an answer of this Reddit discussion somebody defines referential transparency (RT) as "a context $K[ ]$ is RT if, for all $M$ and $N$ s.t. $M = N$, then $K[M] = K[N]$". Based on this definition, Lambda Calculus (LC) (and any other language with binding constructs) is non-RT.

For example, let $\Omega = (\lambda w.ww)(\lambda w.ww)$. In the expressions $(\lambda x.K[x]) \Omega$ and $(\lambda x.K[\Omega])\Omega$, we have $x = \Omega$, so given any RT context $K[]$ both expressions must evaluate to $\bot$. However, if we define $K[] = (\lambda x. [])(\lambda y.y)$, the first expression terminates while the second does not, proving that LC is non-RT.

Is this definition of RT wrong or LC is really a non-RT language?

  • $\begingroup$ I don't understand your definition or your example. You define RT of a context, then you characterize a language as RT. How do you define RT of a language? And what is your example supposed to illustrate? The two expressions you give are not involved in the definition of RT. $\endgroup$ – Gilles 'SO- stop being evil' May 28 '17 at 23:41

Quoting the paper referenced in that thread, i.e. What is a Purely Functional Language by Amr Sabry:

Finally, two informal definitions of purity: referential transparency and independence of order of evaluation, do not have universally agreed-upon definitions and are not considered any further. (See, however, the treatment of referential transparency by Søndergaard and Sestoft (1990).)

This refers to the paper Referential Transparency, Definiteness, and Unfoldability by Harald Søndergaard and Peter Sestoft.

So, first off, there is no "right" definition of referential transparency (especially of an entire language as opposed to a single context) to which to contrast to "wrong" definitions. Secondly, the devil is in the details, which is part of why there is no universally agreed-upon definition. Probably the main factor as alluded to by the original Reddit post is: what notion of equality should we use? Obviously using contextual equivalence would be an absurd choice for this purpose. It would make all contexts referentially transparent tautologically. Another factor is what is the domain of things we're considering plugging into the context: raw terms, $\alpha$-equivalence classes of terms, terms-in-context, closed terms? To extend referential transparency to a whole language further requires specifying what exactly the set of contexts is. Finally, often the term "referential transparency" refers (at least roughly) to what Søndergaard and Sestoft call "unfoldability". This is the ability to replace a variable with what it is bound to without changing meaning. For the pure untyped lambda calculus, this just means the full $\beta$ rule holds which is true for call-by-name but not call-by-value.

In their paper, Søndergaard and Sestoft essentially answer the above questions as follows (extrapolating to the untyped lambda calculus): equality is denotational equality with respect to a given semantics; the domain is raw terms (or perhaps $\alpha$-equivalence classes of terms, whichever the semantics operates over); contexts are as follows: $$\mathcal{K}[\_] ::= \_\mid (\mathcal{K}[\_]) E \mid E (\mathcal{K}[\_]) \mid \lambda x.(\mathcal{K}[\_])$$ where $x$ stands for any variable. At any rate, the upshot of these choices is that your example and psygnisfive's example fail to demonstrate a violation of referential transparency (in this sense) because the terms you are plugging in to the context are not denotationally equal in the first place. In fact, any compositional denotational semantics will guarantee that all contexts are referentially transparent in this sense. Indeed, the example from the paper of a non-referentially-transparent language also has a non-compositional denotational semantics which is "fixed" by making it compositional.

The issue with this definition for more elaborate languages, particularly languages with side-effects, is that we can almost always give a compositional semantics to a programming language. Certainly we can for the lambda calculus extended with mutable state, for example. This leads to the notion not having much bite. The lambda calculus with mutable state equipped with a compositional denotational semantics will be referentially transparent in the above sense because two expressions that have potentially different side-effects won't be considered equal in the first place.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.