
COPLASCopenhagen Programming Language Seminar 
A longstanding open problem is whether there exists a nonsyntactical lambdamodel (=model of the untyped lambdacalculus) M whose equational theory Eq(M) is exactly betaconversion (or betaeta). 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 lambdamodel 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 lambdamodels, 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 lambdacalculus, 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). 
Scientific host:
Klaus Grue.
Administrative host:
Camilla TorpSmith.
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
proglangrequest@mail.itc.dk with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see
http://www.coplas.org