From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,93a8020cc980d113 X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Newsgroups: comp.lang.ada Subject: Re: What is wrong with Ada? References: <1176150704.130880.248080@l77g2000hsb.googlegroups.com> <461B52A6.20102@obry.net> <461BA892.3090002@obry.net> <82dgve.spf.ln@hunter.axlog.fr> <1176226291.589741.257600@q75g2000hsh.googlegroups.com> <4eaive.6p9.ln@hunter.axlog.fr> <1rbtw92apxpl1.1ednvo8v6oiq8$.dlg@40tude.net> <13tcswu59l28h.zxb26cabf9a0.dlg@40tude.net> From: Markus E Leypold Organization: N/A Date: Sun, 15 Apr 2007 18:01:10 +0200 Message-ID: User-Agent: Some cool user agent (SCUG) Cancel-Lock: sha1:WZJOntf5RHTVIh9FMJpY6k5kl20= MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii NNTP-Posting-Host: 88.72.204.228 X-Trace: news.arcor-ip.de 1176652420 88.72.204.228 (15 Apr 2007 17:53:40 +0200) X-Complaints-To: abuse@arcor-ip.de Path: g2news1.google.com!news1.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!newsfeed.freenet.de!news.unit0.net!newsfeed.arcor-ip.de!news.arcor-ip.de!not-for-mail Xref: g2news1.google.com comp.lang.ada:15045 Date: 2007-04-15T18:01:10+02:00 List-Id: "Dmitry A. Kazakov" writes: > On Sat, 14 Apr 2007 12:48:12 +0200, Markus E Leypold wrote: > >> "Dmitry A. Kazakov" writes: >> >>> What I meant is that we cannot write a correct program running on a finite >>> machine which would non-trivially processes an infinite input. [ <=> >>> uncountable sets cannot be enumerated. ] >> >> That is, excuse me, wrong. I thought that you had fallen for that >> fallacy. Let me explain: >> >> The machine itself might go only through a finite number of >> states. But the user input might be a sequence of key presses that >> might terminate arbitrarily late. The input is finite, but the >> "processing state space" and the output space are only finite. This is >> possible: Imagein a "machine" that only counts/indicates wether the >> number of keypresses entered in a sequence from power-on to the end of >> sequence mark are odd or even: Finite program, finite states (rather >> easy indeed). But the set of all "legal" input sequences is >> infinite. Nonetheless the program is correct. > > Which is an example of trivial processing. > >>> Consider a program P that counts the number of key presses. This program is >>> necessarily incorrect. Because a correct P would have an infinite number of >>> states. >> >> In this case yes. But see above. Logically an example that shows an >> attempt to produce an artefact with property X (your program) that >> fails, does not prove its impossible. > > Hmm, that counting infinite sequences is incomputable in DFA barely > requires a formal proof... > >> I've shown that your proposition >> doesn't hold (except if you define "non-trivially" as requiring an >> infinete number of "processing states". > > Yes I do. Trivial means that the set of all possible input states could be Fine. You just messed your argument up completely. If you need infinite processing states, no real machine (only finite amount of internal state) can execute a nontrivial program. > broken into a finite set of classes of equivalent states. In your case into > just two sets of odd and even sequences of key presses. Trivial infiniies > are fake ones. > BTW, your example could be made non-trivial, see Thomson's lamp. Which No, I don't want to see Thompson's lamp. What I want, is that you prove your assertion. As a preparation, let me give some definitions: a) The model: We have a machine M that reads a sequence of input symbols from the set S. The machine is powered up and loaded with an initial state P (we call that program). The we start inputting. We have a method to decide when the the input is complete (either by feedback from the machine, effectively saying "you have entered enough of this") or by something the input operator does (entering the end of input symbol). After entering the complete input the machine somehow indicates that processing is done (or fails to indicate, which is a failure). Then we read out the result R. R comes from a set OUT (the set of all possible outputs dependent on the machines output equipment). b) We are now talking about specifications. As specification SP somehow specifies (i) an input set IN, which is the set of all sequences from seq[S] that should be considered "legal" in the context of SP. IN might be inifinite (at least as far as SP is concerned), e.g. the set of all sequences of arbitrary length that end with the end of input symbol). (b) for every input sequence s \in IN an output r \in OUT which is to be considered the "correct" output for this input. The (partial) function s -> r (which I now name F[SP]) might be called the definige function (or semantics) of the specfication. c) Observe that for every initial state P in the state of the machine, the machine performs a mapping from seq[S] to OUT as well. That is what the program computes. This function C[P]: seq[S] => OUT is the functionality of the program. d) A P conforms to a specification if, within the range of the specfication, i.e. for every input s from IN[SP], it produces the required output F[SP](s). P conforms to SP <=> \forall s \in IN[SP] : C[P](s) = F[SP](s) (A program P conform to a specfication SP, if for every input element that has to be considered legal in the context of SP, the computed output element C[P](s) is the required/specified output element). The model can certainly be refined (i.e. modelling programs as equivalence classes of state), but I think is captures the essence of what we are talking about here. The goal is now, to prove or refute your assertions within that framework. You asserted that \forall SP with NON-TRIVIAL(SP) and I[SP] infinite : \not \exists P : P conforms SP. I have alread shown (by counterexample, which is a valid refutation for \not\exists in this case), that your assertion would be not true just for all SP (i.e. NON-TRIVIAL is constantly FALSE. But "non trivial" is not yet defined (I don't think it makes sense as a formal concept). Now I'd like you to close this loophole for arbitrary hand waving and define NON-TRIVIAL in a way suitable to you purposes (but keep it convincing, still -- defining it to FALSE won't wash with me) and perhaps try to prove the central assertion above. Thank you -- Markus