🚀 go-pugleaf

>]		Some nonterminating programs in the lambda calculus
>]		do NOT denote bottom (e.g. the fixpoint operator).

David Gudeman:		<23574@megaron.cs.arizona.edu> gudeman@cs.arizona.edu 
>	My intepreter stops when it finds a head normal form.

That doesn't mean it has been fully computed.
Don't you find it frustrating to write a program
to prepare a list, only to find that the interpreter
will only say that the result is a kind of ordered pair,
without specifying its components?

The attempt to fully simplify (compute) an expression (program)
will often fail to nonterminate, not just when the result is bottom,
but when the result is only partially defined, or even infinite.

The idea that only terminating computations matter
is one of my pet peeves, actually.

>]		...  Though we cannot solve the halting problem,
>]		you _might_ want to build into a students' compiler
>]		routines to catch the most obvious form of infinite looping,
>]		and replace the bad subcomputation with the bottom symbol.
>]		Must the result be considered as a different language,
>]		just because the interpreter is _sometimes_ able
>]		to tell you that the program denotes bottom,
>]		instead of just letting it loop?

>	Well, if you are going to give the language a formal semantics
>	(an exercise of arguable value) then you might as well
>	give a formal semantics to the various program analyses
>	and transformations.  What's good for the goose is good
>	for the abstract interpretation I always say...

If you incorporate the effects of the optimizations
into your denotational semantics, you might as well
just give an operational semantics instead.
Denotational semantics is a _functional_ notation
for _declaratively_ describing a language's constructs.
If the words `declarative' and `functional'
don't ring a bell for you, I wonder why you are interested
in functional programming in the first place!

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