Copenhagen Programming Language Seminar
A longstanding open problem is whether there exists a non-syntactical lambda-model (=model of the untyped lambda-calculus) M whose equational theory Eq(M) is exactly beta-conversion (or beta-eta).
I will adress here the more general question of whether the equational theory of a non syntactical lambda model can be r.e. (=recursively enumerable), and similarly for the order theory Ord(M) of the model when this makes sense. Note that if Ord(M) is r.e. then Eq(M) is also r.e.
Conjecture (BMS). No lambda-model living in Scott's continuous semantics, or in one of its refinements (e.g. the stable or the strongly stable semantics), has an r.e. equational (or order) theory.
I will present several results which all argue in favour of this conjecture, and which all follow from a few nice key facts . Most of these results, but not all, concern effective lambda-models, a notion which we introduce starting from that of effective domains. This is however enough to cover all the models which have been introduced "individually" in the literature and which live inthe semantics mentioned above.
By way of contrast, note that, concerning typed lambda-calculus, S. Berardi and myself proved that there exist many models M of Girard's System F living in the continous semantics and such that Eq(M)=beta eta conversion [MSCS 2002]; moreover many are effective in our sense, as it is easy to check. Note that these models have no analogue in the stable and in the strongly stable semantics.
(Joint work with A. Salibra and G. Manzonetto).
All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org