🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: comp.lang.functional
Article #315

Re: Term rewriting and denotation

#315
From: Chet Murthy
Date: Fri, 15 Jun 1990 16:10
46 lines
2976 bytes
yodaiken@freal.cs.umass.edu (victor yodaiken) writes:

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

The beef I have with just prim. rec. is not about nontermination.  If
every algorithm had to have a bound, I'd be happy.  But prim. rec.
does not encompass all recursive functions, or even all
computationally interesting recursive functions.

>>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?

But your bound might not be p.r.  You bound might be some ordinal
ABOVE epsilon_0.  Such a program would still be bounded, still be
terminating, still efficient for the average case, but not provably
p.r.  To exclude such algorithms simply because they can't be coded
using primitive recursion seems a bit extreme.
	--chet--
	murthy@cs.cornell.edu
Technical Details
Message-ID: <42267@cornell.UUCP>
Path: arc1-ca.pugleaf.net!utzoo!attcan!uunet!cs.utexas.edu!uwm.edu!rpi!batcomputer!cornell!murthy
References: <22132@megaron.cs.arizona.edu> <42209@cornell.UUCP> <15639@dime.cs.umass.edu>

Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!utzoo!attcan!uunet!cs.utexas.edu!uwm.edu!rpi!batcomputer!cornell!murthy
From: murthy@algron.cs.cornell.edu (Chet Murthy)
Newsgroups: comp.lang.functional
Subject: Re: Term rewriting and denotation
Message-ID: <42267@cornell.UUCP>
Date: 15 Jun 90 16:10:59 GMT
References: <22132@megaron.cs.arizona.edu> <42209@cornell.UUCP> <15639@dime.cs.umass.edu>
Sender: nobody@cornell.UUCP
Organization: Cornell Univ. CS Dept. Ithaca NY
Lines: 46