**From:** Nick Hay (*nickjhay@gmail.com*)

**Date:** Thu Oct 18 2007 - 10:30:39 MDT

**Next message:**Bryan Bishop: "Re: Kolmogorov complexity and prediction"**Previous message:**CyTG: "Re: The Meaning That Immortality Gives to Life"**Next in thread:**Bryan Bishop: "Re: Kolmogorov complexity and prediction"**Reply:**Bryan Bishop: "Re: Kolmogorov complexity and prediction"**Reply:**Eliezer S. Yudkowsky: "Re: Kolmogorov complexity and prediction"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

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
*

*> >
*

*>
*

*>
*

**Next message:**Bryan Bishop: "Re: Kolmogorov complexity and prediction"**Previous message:**CyTG: "Re: The Meaning That Immortality Gives to Life"**Next in thread:**Bryan Bishop: "Re: Kolmogorov complexity and prediction"**Reply:**Bryan Bishop: "Re: Kolmogorov complexity and prediction"**Reply:**Eliezer S. Yudkowsky: "Re: Kolmogorov complexity and prediction"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

*
This archive was generated by hypermail 2.1.5
: Wed Jul 17 2013 - 04:00:58 MDT
*