Is the lambda calculus referentially transparent?

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?

• 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. Commented May 28, 2017 at 23:41

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.