Greg,
Full abstraction: there is junk in the standard denotational domains,
in particular a parallel or function (por). We can write two new
functions f1 and f2, such that f1 por = 1 and f2 por = 2, (and both
give bottom for other boolean functions of the correct type).
So: does f1 = f2? Using an extensional definition of function equality
(applying the functions to the same argument gives the same answer),
we conclude that denotationally f1 /= f2, and operationally f1 = f2.
(Because por is not a sequentially definable function it doesn't appear
in the operational domain.)
Using Ong and Abramskys' fully abstract model of the lazy lambda
calculus will circumvent this problem (by equating f1 and f2) at `some
minor conceptual inconvenience'.
The destruction of the congruence arises because the proof makes
explicit use of the extensional definition of equality of functions.
A fudge is possible if we restrict attention at output to non-function
values.
See: Part I of my DPhil thesis, PRG-73, Oxford [1]; or JE Stoy,
"Congruence of two programming language definitions", TCS 13(2), 1981.
---
David Lester, Informationsbehandling, Chalmers TH, 412-96 Goteborg, Sweden.
[but usually: CS Department, Manchester University, Manchester M13 9PL, UK.]
[1] In case anyone is interested, for FPCA this year, Sava Mintchev and
I ran my congruence proof through Isabelle, and concluded that the
inductions for the proofs of Lemmata 3.18 and 3.19 are mutual, not
seperate.
The embarrassment of theorem provers!
