Observational Equivalence

Two programs in the same programming language are called observationally equivalent whenever they are interchangeable in all observable contexts.

The same notion is also known by the name of (Morris-style) contextual equivalence. In fact, there may a subtle distinction between observational and contextual equivalence depending on the definition, but they often coincide.

A denotational semantics whose equality captures observational equivalence is called fully abstract.

Observable contexts

The above definition is intentionally underspecified: it fundamentally depends on the notion of observable context. Roughly, observable contexts are programs of the same language in which a term has been 'punched' out, and replaced by a hole. This hole can be 'filled' by a program fragment - possibly subject to certain subject restrictions - to obtain a complete program.

An observable context can be considered as an experimental apparatus: one may plug a program into that hole to obtain an actual program, and then evaluate that program to observe the result of the computation. Thus, the shape and the type of the observable contexts determine the kind of 'experiments' we are allowed to run on programs, which in turn determine what is observable.

Filling the hole in a context is crucially distinct from substituting for a variable in an open term for at least two reasons:

1. It is typically desirable for hole-filling to be capturing, rather than capture-avoiding. This is usually necessary in order to define observational equivalence for open terms—given two open terms, their free variables must be given meaning by the context they are inserted into in order for the overall program to produce an observable result.
2. Contexts typically have exactly one hole in them, while an open term may have zero or more than one occurrences of a given variable. This has less of an impact on the meaning of observational equivalence, but it makes induction over contexts a bit differently-shaped and has some influence on the flavor of proofs and definitions. It's also relevant in some other places where contexts are used, like contextual operational semantics.

Specific definitions

To give a concrete definition of observational equivalence, we need to fix the programming language/calculus, and the notions of a context and of an observation. Below we give several examples.

Typed \lambda-calculus with booleans

Consider a typed \lambda-calculus system with the type of booleans (for example, STLC).
A (typed) context C : (\Gamma, \tau) \to (\Gamma', \tau') is a program with a hole, such that if \Gamma \vdash t : \tau, then \Gamma' \vdash C[t] : \tau' (by C[t] we denote the 'filling' of the hole in C with a term t).
For example, (\lambda x. x\ \square) is a context that can be typed as (\Gamma, \tau_1) \to (\Gamma, (\tau_1 \to \tau_2) \to \tau_2).

Then, two term t_1 and t_2 are observationally equivalent at type \tau in a context \Gamma iff
for any C : (\Gamma, \tau) \to (\empty, \mathsf{bool}) it is the case

\forall v.\, C[t_1] \Downarrow v \iff C[t_2] \Downarrow v.

Under this definition, the context may observe the final value of the program (whether it evaluates to \mathsf{true} or \mathsf{false}), and the termination behavior of the program (whether it terminates or diverges).
In particular, this definition equates all diverging programs.
We can also formulate a different version of observational equivalence, that does not take termination behavior into account:

\forall v_1\, v_2.\, C[t_1] \Downarrow v_1 \wedge C[t_2] \Downarrow v_2 \implies v_1 = v_2

Leibniz equality

Leibniz equality can also be seen as an instance of observational equivalence.
In this setting, contexts are predicates, and observations are validity of those predicates.
Two terms t_1, t_2: A are Leibniz equivalent if for any predicate P : A \to \Omega it is the case that

P(t_1) \iff P(t_2)

Context lemma

Please expand.

A relational approach

Observational equivalence is normally defined through contexts, as explained above. However, there is an alternative approach to defining it, namely as the largest type-respecting binary relation that is a congruence, and also adequate. The observational aspect is encoded in adequacy: the relation R is adequate whenever t \mathbin{R} t' : \sigma and t \Downarrow v implies t' \Downarrow v.

This approach is due to Gordon 1988, and was used intensively by Lassen 1998. See also §7.5 of the tutorial chapter Pitts 2005.

References

The concept of observational equivalence is thought to have first arisen in James Morris' thesis. It was first applied to \beta\eta-normal forms of the untyped \lambda-calculus, and called extensional equivalence.

@phdthesis{morris_lambda-calculus_1969,
	type = {{PhD} thesis},
	title = {Lambda-calculus models of programming languages},
	url = {http://hdl.handle.net/1721.1/64850},
	school = {Massachusetts Institute of Technology},
	author = {Morris, James Hiram},
	year = {1969}
}

• The relational/coinductive approach to contextual equivalence is covered in

@incollection{pitts_2005,
	title = {Typed {Operational} {Reasoning}},
	booktitle = {Advanced {Topics} in {Types} and {Programming} {Languages}},
	publisher = {The MIT Press},
	author = {Pitts, A. M.},
	editor = {Pierce, B. C.},
	year = {2005},
	pages = {245--289}
}

@phdthesis{lassen_1998,
	type = {{PhD} dissertation},
	title = {Relational {Reasoning} about {Functions} and {Nondeterminism}},
	school = {Aarhus University},
	author = {Lassen, Søren},
	year = {1998},
	note = {BRICS Dissertation Series BRICS DS-98-2}
}

@incollection{gordon_1998,
	series = {Publications of the {Newton} {Institute}},
	title = {Operational equivalences for untyped and polymorphic object calculi},
	booktitle = {Higher {Order} {Operational} {Techniques} in {Semantics}},
	publisher = {Cambridge University Press},
	author = {Gordon, Andrew D.},
	editor = {Gordon, A. D. and Pitts, A. M.},
	year = {1998},
	pages = {9--54},
}