🚀 go-pugleaf

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