Re: What is wrong with Ada?

[Markus E Leypold <development-2006-8ecbb5cc8aREMOVETHIS@ANDTHATm-e-leypold.de>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On Sat, 14 Apr 2007 12:48:12 +0200, Markus E Leypold wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> 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