Thread View: comp.lang.functional
2 messages
2 total messages
Started by David Gudeman
Fri, 27 Jul 1990 05:21
Re: BOTTOM !== NONTERMINATION
Author: David Gudeman
Date: Fri, 27 Jul 1990 05:21
Date: Fri, 27 Jul 1990 05:21
36 lines
1859 bytes
1859 bytes
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
Re: BOTTOM !== NONTERMINATION
Author: Frank Silbermann
Date: Fri, 27 Jul 1990 15:25
Date: Fri, 27 Jul 1990 15:25
46 lines
2406 bytes
2406 bytes
>] 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
Thread Navigation
This is a paginated view of messages in the thread with full content displayed inline.
Messages are displayed in chronological order, with the original post highlighted in green.
Use pagination controls to navigate through all messages in large threads.
Back to All Threads