NetNews Usenet Archive 1992 #27/NN_1992_27.iso/spool/comp/specific/545

Internet Message Format | 1992-11-20 | 3.2 KB

Path: sparky!uunet!noc.near.net!nic.umass.edu!dime!chelm.cs.umass.edu!yodaiken
From: [e-mail] (victor yodaiken)
Newsgroups: comp.specification
Subject: Re: "Algebra": and Re: Semantic definition style
Keywords: structural operational semantics, denotational semantics
Message-ID: <[e-mail]>
Date: 20 Nov 92 21:47:40 GMT
References: <[e-mail]> <[e-mail]> <[e-mail]>
Sender: [e-mail]
Organization: University of Massachusetts, Amherst
Lines: 59

In article <[e-mail]> [e-mail] (William F Ogden) writes:
>In article <[e-mail]> [e-mail] (victor yodaiken) writes:
>   ...
>>In any event, I've never been able to understand the virtue of working
>>within a mathematical model of computation which permits description of
>>processes that cannot be carried out, even in principle, by any physical
>>computing device. What is it that one intends to learn by application of
>>these methods?
>
>If you look at recursion theory, you'll find that it has developed some
>rather interesting results about degrees of unsolvability by just such an
>approach.

You've misunderstood my point, perhaps I relied too much on the context.
I was responding to a post which argued that first order equational logic
was too restricted to allow description of programs. So, I assumed that
we were discussing the subject of the specification and verification of
computer programs and devices. In this field, it seems inexplicable to
demand, on grounds of generality, that one permit description of physically
impossible computations.

>From this work we know, for example, that natural numbers, a mathematical
>domain which we often use to model computations, permit the description of
>computations that can certainly not be carried out. In fact, in almost
>every domain within which we can describe those computations that could be
>carried out on a physical computing device, we can also describe processes
>which could not. We don't have a choice here, the power to describe the
>uncomputable just comes with the language that allows us to describe the
>computable.

I don't see how we learn this from the study of higher degrees of
unsolvability or from general recursion. It's quite obvious that we can
describe impossible *finite* computations --- e.g. one requiring
Ackermann(100000,100000000000) steps. And, the standard results on
uncomputability can be derived without recourse to transfinite recursion,
oracles, ....
In any case, if someone advances a language L in which we can specify
programs, say: why would it be a flaw if L could only represent all
Turing computable programs, or even all  exponential time computable programs?
Surely any feasable computation will fall within these domains. And, of
course, it is incorrect to confuse the language for specification with
the domain of mathematics available to us. For example, it seems perfectly
reasonable that one could specify a program in language L and prove a
property of the program using some theorem which could not be derived
within L itself.

>
>
>
>--
>
>/Bill


--


[e-mail]