Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!samsung!rex!fs
From: fs@rex.cs.tulane.edu (Frank Silbermann)
Newsgroups: comp.theory
Subject: Models of Lambda Calculus
Message-ID: <1773@rex.cs.tulane.edu>
Date: 10 Jan 90 16:43:35 GMT
Reply-To: fs@rex.UUCP (Frank Silbermann)
Organization: Computer Science Dept., Tulane Univ., New Orleans, LA
Lines: 26

Denotational semantics for LISP-like functional languages
(e.g. Scheme minus side-effects) typically map program syntax
to an expression in an extended lambda calculus.
Typical extensions include atoms, booleans, sequence constructors,
and delta-conversion rules.

It is understood that such an extended lambda calculus
can be encoded within the pure untyped lambda calculus,
which has as extensional model a domain isomorphic
to its own function space (i.e. the solution to domain
equation "D ~= D->D").

Nevertheless, has the extended lambda calculus ever
been studied in its own right?  For instance,
has anyone ever shown the domain
	D ~= (Atom + Bools + DxD + D->D)_bottom
to be an extensional model of an extended lambda calculus?

I am especially interested in extensions
to the _untyped_ lambda calculus,
which seems more appropriate for describing languages
like pure Scheme.

I would be grateful to receive references.

	Frank Silbermann	fs@rex.cs.tulane.edu