Phisical computation was discovered by nature 4000 Million years BT (Before Turing) . And even before.
2014/1/12, Bruno Marchal <[email protected]>: > > On 11 Jan 2014, at 22:41, Alberto G. Corona wrote: > >> By the way, what about if you find a mathematical theory that show >> that: >> >> computer programs and matematical proofs are no longer something out >> of math, > > This is non sense. Computer programs have born in math. > > > > >> but mathematical structures and both are essentially the same >> thing: > > The computable is purely mathematical since birth (excepting Babbage, > but even Babbage discovered it was mathematical at the end of his > life, arguably, from a work due to Jacques Lafitte). > But the mathematical, classically conceived, is *much* larger than > the computable. > N^N is not enumerable. the computable restriction of N^N is enumerable. > > > >> both are paths from premises to conclussion in a space with >> topological properties > > That does not make them identical. > > > >> >> And the theory stablish topological relations between these paths so >> that proofs and computer algorithms are classified according with >> these relations. > > You might study the book by Szabo, on the category approach on the > algebra of proofs. > But proofs and computations are not equivalent concept at all. There > is a Church's thesis for computability, not for provability and > definability which are machines or theories dependent. > > > >> >> That is homotopy type theory. >> >> http://homotopytypetheory.org/ >> >> I´m starting to learn something about it, It is based on type theory, >> category theory and topology. > > That is very interesting, and category provides nice model for > constructive subpart of the computable, like typed lambda calculus. > But category becomes very hard on the complete algebra of computation. > the partial nature of the fiunctions involved makes hard to even > compute a co-product. > > > >> The book introduction is nice (HOTT link >> at the bottom of the page). It seems to be a foundation of computer >> science and math that unify both at a higher level, since proofs and >> programs become legitimate mathematical structures > > They are since Church thesis. That is all what computability or > recursion theory is all about. > The rest is semantics of languages, more useful in computing theory > than in computability theory, which is born, I insist, before we > implement physical computer. The computer have been disocvered by > mathematicians, in mathematics, indeed, in arithmetic. Those notions > are born mathematical. > > Only later, some physicists have tried to get, without any success, a > notion of physical computation. > >> >> The book: >> >> http://homotopytypetheory.org/2013/06/20/the-hott-book/ > > Guiseppe Longo wrote also nice book on that subject. It is a vast > field, but Gödel made "proof" into arithmetical objects well before, > as the notion of computations will follow soon after (if not before if > we take Post's unpublished anticipation into account). > > > Bruno > > > >> >> -- >> 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/groups/opt_out. > > http://iridia.ulb.ac.be/~marchal/ > > > > -- > 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. > -- 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/groups/opt_out.
