MIRIxUW workshop report

[Sam Eisenstat]

Hi,

The MIRIx workshop was today. We had four people: myself, David, Tobias, and William. We looked over and discussed the three resources I mentioned in the announcement: A model of UDT with a concrete prior over logical statements (Fallenstein, 2012), Non-Omniscience, Probabilistic Inference, and Metamathematics (Christiano, 2014), and Logical Prior Probability (Demski

[Sam Eisenstat]

Hi,

The MIRIx workshop was today. We had four people: myself, David, Tobias, and William. We looked over and discussed the three resources I mentioned in the announcement: A model of UDT with a concrete prior over logical statements (Fallenstein, 2012), Non-Omniscience, Probabilistic Inference, and Metamathematics (Christiano, 2014), and Logical Prior Probability (Demski, 2012). We mostly focused on Non-Omniscience, reading through the paper and discussing things that we found to be interesting or confusing.

This work draws on many different fields: first-order logic, computability theory, algorithmic information theory, (standard) information theory, and semidefinite programming. It seems like first-order logic is the most important thing to learn here, since it pervades everything being done, rather than just being used in to accomplish a few things. I think it would be a good idea for MIRIxUW to help people learn logic, though I'm not sure what the best form for that to take is. Nate recommends the book Computability and Logic by Boolos et al., which does cover a good amount of, well, computability and logic. In his review of that text he says:

This book comes highly recommended, especially to people just getting interested in the fields of computability and logic. If you're interested in computation or logic, this book introduces some of the coolest results in both fields in a very approachable way.

This book excels at showing you the actual mechanisms behind results that are often mentioned but seldom exposed. Even if you know that the deduction problem is equivalent to the halting problem, it's illuminating to play directly with an encoding of Turing machines as logical theories.

I have read a few chapters of this (it's where I saw the result about dyadic logic that I mentioned today, but they were toward the end and, as Nate says,

Chapters 19-27 are optional. They're less polished and less motivated, and more likely to just dump a proof on you. Read the ones that seem interesting, but don't be afraid to skip the ones that seem boring.

so I can't really second this recommendation. Anyway, it's available in the UW library and on libgen if you're interested. I'm interested in feedback as to what people want to do. I can also lecture on logic and computability as a supplement to this.

A few points that we discussed at the workshop stand out:

Tobias noticed that the logic corresponding to Paul's definition of trivial equivalence is related to quantum logic, so it would be interesting to see whether quantum logic could be used instead in this context.

We worked through the definition of Bregman divergence, and figured out why it makes sense to use it as a quantity to optimize in the updating rule.

I explained why priors closely related to the one described in Concrete Prior over Logical Statements are dogmatic. I conjectured that Benja's original prior is dogmatic as well.

Tobias convinced me that it is worth looking into whether logical uncertainty can be better understood using type theory. David pointed me toward a series of lectures on Agda, a dependently-typed programming language, but I have not been able to find the lectures. I did watch this introduction though. Proving correctness is interesting, but it seems like a lot of work. It's cool that the stuff done in this blog post by Haskeller and LWer Twan van Laarhoven is possible, but it would be nice if it were about 1/4-1/3 as much work. Hopefully the library support will get to that point.

Best,
Sam

[David Rusu]

Hey Sam,
Thanks for organizing the event and writing this up
I was actually thinking of Idris, link:
http://www.reddit.com/r/haskell/comments/2ty27b/dependently_typed_functional_programming_in_idris/

--
You received this message because you are subscribed to the Google Groups "lesswrong waterloo" group.
To unsubscribe from this group and stop receiving emails from it, send an email to lesswrongwater...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Sandy Maguire]

Mad bummed I couldn't make it. Sounds awesome though. I'll make it to
the next one!

Thanks for the writeup, Sam!

On 2/9/15, David Rusu <dav...@gmail.com> wrote:
> Hey Sam,
> Thanks for organizing the event and writing this up
> I was actually thinking of Idris, link:
> http://www.reddit.com/r/haskell/comments/2ty27b/dependently_typed_functional_programming_in_idris/
>
>
> On Sun, Feb 8, 2015 at 12:48 AM, Sam Eisenstat <sam.e...@gmail.com>
> wrote:
>
>> Hi,
>>
>> The MIRIx workshop was today. We had four people: myself, David, Tobias,
>> and William. We looked over and discussed the three resources I mentioned
>> in the announcement: A model of UDT with a concrete prior over logical
>> statements

>> <http://lesswrong.com/lw/eaa/a_model_of_udt_with_a_concrete_prior_over_logical/>

>> (Fallenstein, 2012), Non-Omniscience, Probabilistic Inference, and

>> Metamathematics <https://intelligence.org/files/Non-Omniscience.pdf>

>> (Christiano, 2014), and Logical Prior Probability

>> <http://ict.usc.edu/pubs/Logical%20Prior%20Probability.pdf> (Demski,
>> 2012). We mostly focused on *Non-Omniscience*, reading through the paper

>> and discussing things that we found to be interesting or confusing.
>>
>> This work draws on many different fields: first-order logic,
>> computability
>> theory, algorithmic information theory, (standard) information theory,
>> and
>> semidefinite programming. It seems like first-order logic is the most
>> important thing to learn here, since it pervades everything being done,
>> rather than just being used in to accomplish a few things. I think it
>> would
>> be a good idea for MIRIxUW to help people learn logic, though I'm not
>> sure
>> what the best form for that to take is. Nate recommends

>> <http://lesswrong.com/lw/l7o/miri_research_guide/> the book Computability
>> and Logic
>> <http://smile.amazon.com/Computability-Logic-George-S-Boolos/dp/0521701465/>

>> by Boolos et al., which does cover a good amount of, well, computability
>> and logic. In his review of that text

>> <http://lesswrong.com/lw/j4r/book_review_computability_and_logic/> he

>> I explained why priors closely related to the one described in *Concrete
>> Prior over Logical Statements* are dogmatic. I conjectured that Benja's

>> original prior is dogmatic as well.
>>
>> Tobias convinced me that it is worth looking into whether logical
>> uncertainty can be better understood using type theory. David pointed me
>> toward a series of lectures on Agda, a dependently-typed programming
>> language, but I have not been able to find the lectures. I did watch this

>> introduction <http://vimeo.com/77168227> though. Proving correctness is

>> interesting, but it seems like a lot of work. It's cool that the stuff
>> done

>> in this blog post <http://twanvl.nl/blog/agda/sorting> by Haskeller and
>> LWer <http://lesswrong.com/user/twanvl/overview/> Twan van Laarhoven is