Scott's "A system of functional abstraction" and a variant of Rice's theorem
Yannick Forster
forster at ps.uni-saarland.de
Tue Jun 1 04:10:10 EDT 2021
Dear FOM readers,
in 1962/63 Dana Scott gave a lecture at Berkeley, called "A system of
functional abstraction". The corresponding lecture notes are widely
cited as the origin of Scott encodings, but also contain a theorem
similar to Rice's theorem, just formulated for the lambda-calculus
(found e.g. as Theorem 6.6.2 in Barendregt's "The Lambda Calculus - Its
Syntax and Semantics").
I am especially interested in the latter. In text books, Rice's theorem
is usually proved by at least implicitly establishing a many-one
reduction from an undecidable set to either the set in question or its
complement. But there is also a direct proof without having established
an undecidable set before, using a fixed-point theorem or Kleene's
recursion theorem. For all I know, Scott might have been the first to
use this direct proof technique.
I would be very interested in
(1) pointers to early direct proofs of Rice's theorem based on
fixed-point or recursion theorems
(2) pointers where I can find notes for Scott's 1962/63 lectures (full
citation below), possibly as a scan
Many thanks in advance for any help
Yannick
-- PhD student at Saarland University
https://www.ps.uni-saarland.de/~forster
------------------------------------------------------------------
In Curry, Hindley, and Seldin's "Combinatory Logic" Vol 1, Scott's
lecture notes are cited as
Dana Scott, A system of functional abstraction. Lectures delivered at
University of California, Berkeley, Cal., 1962/63. Photocopy of a
preliminary version, issued by Stanford University, September 1963,
furnished by author in 1968.
More information about the FOM
mailing list