Scott's "A system of functional abstraction" and a variant of Rice's theorem

[Yannick Forster]

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.