Article View: comp.lang.functional
Article #311Re: Term rewriting and denotation
From: victor yodaiken
Date: Fri, 15 Jun 1990 05:08
Date: Fri, 15 Jun 1990 05:08
61 lines
3762 bytes
3762 bytes
In article <42209@cornell.UUCP> murthy@algron.cs.cornell.edu (Chet Murthy) writes: >There are lots of examples of algorithms that depend for their >termination upon the well-ordered-ness of ordinals of greater height >than epsilon_0, and the fact that every primitive recursive function >sits properly below epsilon_0 tells us that we cannot hope to do all >programming just with p.r. functions. > >--chet-- And In article <10838@medusa.cs.purdue.edu> gb@cs.purdue.edu (Gerald Baumgartner) writes: >Since there is still `term rewriting' in the subject: take the >Knuth-Bendix algorithm for transforming rewrite rule systems into a >canonical form. It is a straightforward algorithm if you write it with >a while-loop or with recursion. You'll have trouble writing it with PR >constructs since no general bound is known. > I'm not arguing that one can dispense with all but p.r. mathematics. I'm questioning the need for anything beyond p.r. functions in a *programming language*. Since, programming languages are usually intended as aids in describing computations that we desire a digital computer to perform, it is not clear to me why we need to be able to describe computations that are not feasible. One can write a p.r. function which computes a bounded Knuth-Bendix algorithm say KB(r,p,q), where "r" bounds the number of steps. Suppose we write a program in a language which allows expression of unbounded algorithms and have an unbounded version of knuth bendix KB'(p,q). What is the formal semantics of this function? Is it that the algorithm will be executed until termination? If so, the program is not intended for any existing or proposed digital computer that I know of. If KB'(p,q) is intended for the class of mundane digital computers than the proposed semantics is incorrect --- a programmer who believes the formal semantics will be deceived, his/her program will behave in a manner not matching the formal semantics. The p.r. version provides the programmer with a better grasp of the actual nature of digital computation. The programmer is forced to consider the case where time runs out. >This Groebner basis algorithm has a similar structure as the >Knuth-Bendix algorithm (Knuth-Bendix can be simulated by Groebner >basis algorithm, probably vice versa). The Groebner basis algorithm >runs in doubly exponential time (double exp. in the degree of the >polynomials and exponential in the number of polys or so) and still it >is useful (at least many mathematicians are using it). BTW, I'm sure you know that double exponential functions are p.r. >The algorithm >is around since 1967, it took some 10 years until a bound was >discovered for the case of polys of degree at most 2. There is still >no bound known for the general case. Without a bound for the running >time you cannot program this algorithm using PR constructs. > But when you compute the algorithm on a real computer, you do have bounds on time and storage. Thus, even without a known bound, you implicitly program the algorithm in a bounded way. Why is it better to use implicit bounds? [more, similar examples deleted].
Technical Details
Message-ID:
<15639@dime.cs.umass.edu>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!tut.cis.ohio-state.edu!snorkelwacker!bu.edu!xylogics!transfer!crackers!m2c!umvlsi!dime!yodaikenReferences:
<22132@megaron.cs.arizona.edu> <42209@cornell.UUCP>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!tut.cis.ohio-state.edu!snorkelwacker!bu.edu!xylogics!transfer!crackers!m2c!umvlsi!dime!yodaiken From: yodaiken@freal.cs.umass.edu (victor yodaiken) Newsgroups: comp.lang.functional Subject: Re: Term rewriting and denotation Message-ID: <15639@dime.cs.umass.edu> Date: 15 Jun 90 05:08:17 GMT References: <22132@megaron.cs.arizona.edu> <42209@cornell.UUCP> Sender: news@dime.cs.umass.edu Reply-To: yodaiken@freal.cs.umass.edu (victor yodaiken) Organization: University of Massachusetts, Amherst Lines: 61