On Fri, Feb 14, 2014 at 09:30:52PM +0100, Bruno Marchal wrote: > > On 14 Feb 2014, at 05:42, meekerdb wrote: > > >On 2/13/2014 8:40 PM, Russell Standish wrote: > >>I had a look at your SANE paper, which is the main paper where > >>you describe > >>your work that you published since your thesis. I can sort of see you > >>saying something a bit like the above on page 11 "Now DU [sic - > >>should > >>be UD in English] is emulated platonistically by the verifiable > >>propositions of arithmetic. They are equivalent to sentences of the > >>form ``if exists n such that P(n)'' with P(n) decidable." > >> > >>That is actually rather confusing. Obviously a UD executes all proofs > >>of all true Sigma 1 sentences, but I think what you are trying > >>to say that > >>all programs executed by the UD correspond to a proof of some true > >>Sigma 1 sentence. Is that obvious? I didn't get that when I read > >>the SANE paper > >>originally, only got it in context of your statements above. > > > >How can that be? Many programs executed by the UD are non-halting, > >just loops. Can they be considered to correspond to a proof? > > Yes, like a failed proof. Like searching the first even prime number > bigger than 2. The search for ExP(x) when Ax~P(x), but you don't > know that. But for the probability calculus, you can limit yourself > on the finite pieces of computations, as the first person will glue > the infinities of them to experience their "consistent" infinite > union. > > Bruno >
I suspect its a little more subtle. Solomonoff's original formulation of the universal prior failed the axioms of probability theory, because it included all computation, even non-halting ones. This was fixed by Levin, who restricted the sum to range over halting computations only. I think this point needs further thought, as presumably the consistent computations passing through my state will be dominated by non-halting ones. -- ---------------------------------------------------------------------------- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics [email protected] University of New South Wales http://www.hpcoders.com.au ---------------------------------------------------------------------------- -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
