Path: utzoo!attcan!uunet!zephyr.ens.tek.com!uw-beaver!mit-eddie!wuarchive!zaphod.mps.ohio-state.edu!samsung!crackers!m2c!umvlsi!dime!yodaiken
From: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Newsgroups: comp.specification
Subject: Re: Against executable specifications (Re: specifying OBJ in itself)
Message-ID: <21665@dime.cs.umass.edu>
Date: 23 Oct 90 12:39:01 GMT
References: <21500@dime.cs.umass.edu> <5321@uqcspe.cs.uq.oz.au> <21617@dime.cs.umass.edu> <40496@shemp.CS.UCLA.EDU>
Sender: news@dime.cs.umass.edu
Reply-To: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Organization: University of Massachusetts, Amherst
Lines: 31

In article <40496@shemp.CS.UCLA.EDU> chou@oahu.cs.ucla.edu (Ching-Tsun Chou) writes:
>In article <21617@dime.cs.umass.edu> yodaiken@chelm.cs.umass.edu (victor yodaiken) writes:
>
>[.....]
>
>>In a well defined executable notation, you should only be able to specify
>>systems that will not diverge. That is, construction of a specification
>>should itself constitute a proof that the specified system is non
>>divergent.
>
>
>Think about this:
>
>Can you design a programming language in which ALL and NOTHING BUT total 
>(in the sense of being convergent for all inputs) recursive functions
>can be described?


What is the purpose of a programming language? If it is to describe
"effective computations" in the mathematical sense, then you are correct.
If, on the other hand, the purpose of a programing language is to describe
computations that are feasable on digital computers, we have some immediate
constraints. There is an article by Parikh (Journal of Symbolic Logic 1977?)
which suggests that an arithmetic restricted to exponentially computable
functions might be sufficient. An earlier paper, by Cobham, argues that 
the polynomially computable functions are sufficient. Also, you might be
interested in Predicative Arithmetic  by Nelson. Nelson shows that it is
possible to derive a large chunk of number theory from an axiomatization
of arithmetic that is entirely devoid of impredicative methods.
Turing machines are models of *effective computation*, not feasable
computation.