Advisors: Yannick Forster and Dominik Kirst
PCF (Programming Computable Functions) is an idealised functional programming language introduced by Plotkin in 1977. It has been inspired by work of Scott as well as Platek and has proved to be of great importance in practice by serving as basis for the design of functional programming languages such as standard ML and Haskell. Nevertheless, the full abstraction problem, posing the question whether there exists a fully abstract model for PCF that is both concrete and independent of syntax, has been open for decades.
In 2001, Loader provided a negative answer to this problem by proving contextual equivalence undecidable for a severely restricted version of PCF called PCF2. A solution of the full abstraction problem would entail the decidability of contextual equivalence on PCF - and in particular on PCF2, which is why Loader’s result excluded the existence of such a model. In Loader’s undecidability proof, which is well-known to be full of intricate technical arguments and contains barely any examples, the undecidability of contextual equivalence on PCF2 is deduced from that of string rewriting.
In this thesis, we point out that Loader’s arguments can be turned into a chain of four many-one reductions and mechanise part of it in the Coq proof assistant in the setting of synthetic undecidability. To be precise, we mechanise observational equivalence – an equivalence relation used in Loader’s proof agreeing with contextual equivalence, as well as all reductions but the first in the chain. Furthermore, we provide insightful examples and present nontrivial details that are left out in Loader’s paper, making the result more accessible to non-expert readers and laying a foundation for future work mechanising the remaing reduction.