🚀 go-pugleaf

In article  <3940@rex.cs.tulane.edu> fs@rex.cs.tulane.edu (Frank Silbermann) writes:
]Some nonterminating programs in the lambda calculus
]do NOT denote bottom (e.g. the fixpoint operator).

My intepreter stops when it finds a head normal form.

]The language of denotational semantics
]is a much more realistic basis for functional programming
]than the pure untyped lambda calculus.

OK.

]...  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.

Why just for a student compiler?  Sounds to me like a generally good
thing to have.  (BTW, remind me to tell you the story sometime about
the progammer who told me he wrote a program to detect all infinite
loops in FORTRAN programs :-)

]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...
-- 
					David Gudeman
Department of Computer Science
The University of Arizona        gudeman@cs.arizona.edu
Tucson, AZ 85721                 noao!arizona!gudeman