🚀 go-pugleaf

fs@rex.cs.tulane.edu (Frank Silbermann) writes:


> <lots of good stuff, but then ...>

>For instance, the pure untyped lambda calculus is fully abstract
>w.r.t. a domain isomorphic to its own function space
>(i.e. a universe D isomorphic to the universe of
>computable unary functions over D).

Not so, I think. As you appreciate at the start of your letter,
parallel-or is only (untyped-)lambda-definable through some
complex encoding/interpretation. However, parallel-or exists in the
Scott domain. Hence, lambda-calc's not fully-abstract. The detailed
support for this comes from Mulmuley (1987) and Plotkin (1977). While
they're working with typed lambda-calc., I can't see how that affects
the issue (ie the semantic domain's got something in it that the
programming language hasn't). Anyhow, I look forward to being corrected
if appropriate.

REFERENCES

Mulmuley, K. ``Full Abstraction and Semantic Equivalence'' MIT Press 1987.

Plotkin, G.D. ``LCF Considered as a Programming Language'' TCS vol 5 pp 223-
	255 1977.

Paul Bailes
Dept Comp Sci
Uni of Queensland QLD 4072
AUSTRALIA