The richer a programming language is, the more discriminating power program contexts have and hence the less observational equivalences hold in the language. For example, the beta law
(λx.t) v ≃ t[v/x]is regarded as the fundamental observational equivalence in functional programming. However, it can be violated in the presence of a memory inspection feature like the one provided by the OCaml garbage-collection (Gc) module. A function that returns the size of a given program enables contexts to distinguish (λx.0) 100 from 0, for example. The fragility of observational equivalence extends to its proof methodologies. There have been studies of the impact that language features have on semantics and hence on proof methodologies for observational equivalence.
The development of game semantics made it possible to give:
-
such state and control, e.g. the so-called “Abramsky cube” Abr97 Ghi23, or to replace the syntactic notion of context by an abstracted adversary GT12. A classification DNB12 and characterisation DNRB10 of language features and their impact on reasoning has also been undertaken using logical relations. Applicative bisimilarity has been enriched to handle effects such as algebraic effects, local state, names and continuations SKS07, KLS11, DGL17, SV18.