The Possible Irreducibility of Artificial Software Life - Bruce Edmonds
According to the above characterization "L is reducible" is interpreted as "There is a program p that computes L". This is not a constructive definition, it is sufficient that such a program exists, it does not mean that there would have to be any practical or systematic way of building such a program.
If whenever we could compute L (with a program p), we could also compute p from L, then the mere existence of such a program, p, would be sufficient - as we would also know that we could compute that program.
If, on the other hand, there were cases where there is a program p that computes L, but there is no way to compute that program p from L, then it is clear that it is, at the very least, highly misleading to say that "L is reducible". In such a case it may be possible to come across the program p by accident, but then we would still need to check that it was the correct program. Given the assumption above, this would not be even semi-decidable for if it were then we could use this to construct a program to compute L, which would contradict the assumption that L was not computable from p.
Below we show that, given plausible limitations on our programming ability, such cases do exist. Thus the above characterization of reducibility is too weak. Unless there is some calculating devices more powerful than a Turing machine, in order for L to reduce it, we (aided by computers etc.) must be able to find a program to compute it. If this is not to be the result of an unverifiable accident we must be able to somehow compute the program that computes L.
We can formalise the situation in the following way. L is a statement in some recursively axiomatized logic. So the statements in this logic can be effectively enumerated . Similarly enumerate the possible programs .
We then say, , or a theoretical reduction, if
Then define , or is an systematically realisable reduction if, in addition to condition (1),
The question then becomes, given any particular , encoding a systematic method of building a programs from statements in this language, "Are there pairs that are a theoretical reduction but not a systematically realisable reduction?". In other words Is there a difference between the normal criterion of computability and such "systematically realisable computability"? The answer to this is "Yes", as I now show
Theorem
Proof Outline
We consider a series of statements, indexed by the natural numbers, n, representing what I call the limited halting problem, i.e. "for all (fixed) program halts given input ". Call this , in contrast to the full halting predicate ("program halts given input w"). This is a finite function, hence it is computable in the sense that for each n there exists*1 a program that decides . Thus for each separate n, is theoretically reducible.
If for all n is a theoretical reduction then this would allow us to also decide , since by the s-n-m theorem (page 81 of [1]) there is a computable function, q, such that . Then would be decided by , and thus would be computable, which we know is not the case (Turing [7]).
Thus for any there is an , and a program q, but not .
Here, you have to be careful about the indexing. What the above theorem does not say is that there is a pair that is theoretically reducible but not intentionally reducible given any program . After all, given any particular pair one could simply add this as a special case in your plan represented by a program ' that would compute an index for a program to compute the first of the pair from the second. The point is that there is no systematic way of doing this short of adding special cases for all such cases (an infinite number of them). So if you are going to reduce all such theoretically reducible pairs, there must be some arbitrary or non-computable element. If it is arbitrary or non-computable one can not say that one intended its results. Thus at least some theoretically reducible statements are not systematically realisable reducible (as in "reduced as result of a deliberate plan to do so"). This is not very surprising given the string of uncomputability results this century, starting with Turing [7] and GÖdel [2].
What the above shows is that there is a real difference between was is theoretically reducible and what is systematically realisable reducible and that defining something as reducible if it is only theoretically reducible and not intentionally reducible is not sensible as there would be no guarantee that there was a practical way of performing this reduction*2. Thus just because a program exists does not mean that there is an systematic way of programming it. In a real sense there are programs that are unreachable using systematic means.
Generated with CERN WebMaker