🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: comp.lang.functional
Article #311

Re: Term rewriting and denotation

#311
From: victor yodaiken
Date: Fri, 15 Jun 1990 05:08
61 lines
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!yodaiken
References: <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