Path: utzoo!utgpu!news-server.csri.toronto.edu!rutgers!usc!samsung!rex!fs
From: fs@rex.cs.tulane.edu (Frank Silbermann)
Newsgroups: comp.lang.functional
Subject: Re: Laziness and Leftmost Rule
Message-ID: <3485@rex.cs.tulane.edu>
Date: 4 Jun 90 17:07:22 GMT
References: <BJORNL.90Jul30101627@tarpon.tds.kth.se> <3462@rex.cs.tulane.edu> <1990Jun2.123101.24421@sics.se>
Organization: Computer Science Dept., Tulane Univ., New Orleans, LA
Lines: 81


(my previous post)
>%	The theoretical justifications for purely leftmost evaluation
>%	were developed for in syntactic term-rewriting systems
>%	and also for the pure untyped lambda calculus.
>%	Many assume that the justifications carry over
>%	to more complicated languages.  This is not always true.

The pure untyped lambda calculus is Turing equivalent.
One can express and compute any computable function via this notation.

Through a very complicated encoding, one could represent
symmetric boolean operations (e.g. parallel-OR).
The pure LC object language program would encode
the source program via some sort of dove-tailing algorithm,
so that left-most reduction of the object program
would simulate parallel evaluation of the source program.

However, such an encoding would be very ugly
(so would implementation via Turing machines
or via arithmetic in a Godel-numbering scheme).
Such an exercise is not very interesting --
all it does is build one machine (the language evaluator)
on top of another (the pure lambda calculus).

To show that a "functional" program is not merely
a set of computer instructions, but simultaneously
a mathamatical statement of fact (declarative),
then we must answer the following questions:

1)  Upon what domain or domains of values are
    the function mappings defined?

2)  From a given program expression,
    how is the function mapping derived?

For these questions,
term-rewriting theory is irrelevant; denotational semantics
provides functional programming's theoretical basis.
Domain theory describes the appropriate domains.
Since beta reduction resembles function application,
it is natural to use lambda expressions to denote
the various elements.

Interpreting lambda expressions as functions is justified
when we prove that the relationship between lambda expressions
and domain elements is _fully abstract_, i.e.  that
two lambda expressions denote the same domain element
IFF in any context they yield equivalent results.

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).
This is not the domain most programmers have in mind.
We want functions as objects; but do we want _only_ functions?

We need a lambda calculus with different kinds
of expressions to represent different kinds of objects
(not just functions, but also integers, booleans and sequences).
This is called a _typed_ lambda calculus.
To define a language via denotational semantics,
we map program statements into a kernal lambda calculus
whose fully abstract interpretation is both appropriate
and well understood.

So far, there has been more progress with typed languages
like pure ML and LCF, and less progress with untyped languages
such as pure Scheme.
A common weakness is use of an "extended lambda calculus"
whose operational properties are convenient, but whose
denotational semantics (i.e. its fully abstract interpretation)
has never been worked out.

>%>	So, there's a problem with the very theoretical foundations
>%>	of functional programming!  /Bjorn Lisper

Of course, otherwise there would be no more work for theorists!

	Frank Silbermann	fs@rex.cs.tulane.edu
	Tulane University, New Orleans, Louisianna  USA