I still don't know what this theorem add to common sense. I mean, what it add out of his universe of formalizations in order to better formalize the obvious.
In the other side, using the curry-howard isomorphism in which for each theorem there is a program: http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html This people found the type of a program in the haskell language that is isomorphic. The loeb formula: loeb :: Functor a => a (a x -> x) -> a x Which indeed can be used to compute spreadsheets using lazy evaluation. That is, to calculate/prove the value of a cell written as an expression that is a function of the values of other cells and so on. Compared with löb : □(□P→P)→□P in the formula 'a' means "the solution for". In this case 'a x' is a list of the values of the cells. and it tells that "if you give me a list of expressions , each one a function of the resulting values, I will return the list of resulting values. The above expression are the types of the parameters The complete formula is: loeb :: Functor a => a (a x -> x) -> a x loeb x = fmap (\a -> a (loeb x)) x where 'fmap' is a haskell function that match with the parameter types and loeb is called recursively. The expression was found almost experimentally, without knowing well what the final result was. I created a real spreadsheet-like program using haskell running in a web browser that uses the loeb expression and it works as expected: http://tryplayg.herokuapp.com/try/spreadsheet.hs/edit 2014-09-22 13:56 GMT+02:00 Telmo Menezes <[email protected]>: > > http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%83%C6%92%C3%86%E2%80%99%C3%83%E2%80%A0%C3%A2%E2%82%AC%E2%84%A2%C3%83%C6%92%C3%A2%E2%82%AC%C5%A1%C3%83%E2%80%9A%C3%82%C2%B6bs_theorem/ > > -- > 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/d/optout. > -- Alberto. -- 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/d/optout.
