From: Nick Hay (nickjhay@gmail.com)
Date: Thu Oct 18 2007 - 10:30:39 MDT
Here are some more precise observations.
A program of fixed complexity can prove that infinitely many systems
(coded as strings or sequences) satisfy some specification, e.g. that
they are a halting program, or encode a bridge design that does not
collapse under certain stresses, or that the program correctly
predicts a certain class of sequences.
Not all prediction specifications work. For example this doesn't work
for the class of all simple sequences, i.e. of complexity < K(n), but
it does for the class of all sequences pU(p) where U is a fixed TM
i.e. programs that first output their source code, then run it.
Perhaps it even works for the class of most sequences that will be
generated in this universe has a nice form (I don't have a precise
definition of this currently).
A simple precise specification that does work is the set of theorems
of some formal system paired with a proof of them. We can easily
generate proofs and theorems of arbitrary complexity, and easily
verify if a particular theorem/proof is valid.
A program of a fixed complexity can write understandable systems (i.e.
those it can predict fit some specification) of arbitrary complexity
(the above example works here). The arbitrarily complex bridge design
has a lot of features, e.g. tailoring traffic signal policies, shape
details, colouring, etc. But it is understandable e.g. because it is
sufficiently over designed that one can easily show, e.g. by
simulation, that it doesn't collapse under certain stresses. The
program can generate strings significantly more complex that itself
because it reads some complex sequence from the environment (its
input).
So systems of fixed complexity can both understand, and build
understandable, systems of greater complexity than themselves.
Not all specifications in general work. You can generalize Chaitin's
proof that a formal system can only prove sentences of the form K(x) <
n for finitely many n. Given a definable sequence C_n of classes of
strings (i.e there is a formula c(n,x) which is true iff x is a member
of C_n) which are each inhabited (i.e. for every n there is some x_n
such that you can prove c(n,x_n) holds), there is an algorithm which
produces on input n an element of C_n: just search the theorems of a
formal system until the find the right proof.
As a corollary, if we encode the number n in binary form before
passing it to the algorithm, there is a fixed k such that C_n has a
member of complexity k + 2log(n), for all n. This excludes P_n, the
class of programs which eventually predict all sequences of complexity
at most n, because by your adversary argument any element of P_n must
have complexity greater than n-k, for some fixed k, which grows faster
than log n. If we encode the number as a program which outputs n you
can replace k+2log(n) in the above with k + K(n).
What this means is if all the strings in C_n have complexity greater
than some computable function of n, then for some N we for all n>N we
cannot prove that any particular string is in C_n i.e. C_n is not
inhabited. We can prove that C_n is nonempty for all n, but that's a
different thing.
With regards to proving the Friendliness of a system, you would
probably not be able to prove your FAI successfully predicts all
systems of complexity at most n for some nice n, but you might be able
to prove that *if* it eventually predicts the particular sequence it
was given, then it is has a Friendly output. For example, the class
C_n = for all strings with K(x)=n, if the system eventually predicts x
then it has a Friendly output. This class doesn't suffer the above
proof, because C_n has simple programs in it for all n.
We probably want a class of designs that doesn't necessarily fail if
it can't predict its environment.
--- Nick
On 10/17/07, Shane Legg <shane@vetta.org> wrote:
> Could you make your claim more precise?
>
> What do you mean by a "bridge", or a nice form,
> and when you talk about proving correctness,
> correctness at doing what? Correctly predicting?
>
> Shane
>
>
>
> On 10/16/07, Nick Hay <nickjhay@gmail.com> wrote:
> >
> > That is, it doesn't exclude predicting some complex systems, maybe
> > many, and especially those of particularly nice forms (e.g. highly
> > complex but understandable bridges, complex programs with attached
> > proofs of correctness, etc).
> >
> > -- Nick
> >
>
>
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:58 MDT