The Curry-Howard-Lambek correspondance is a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed category. Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs in logic (and vice versa). Reference: http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence
Bilski ruling renders all software unpatentable in the US because any method of manipulating information (i.e an algorithm) can be translated into a Haskell program, every Haskell function is a formula in the Typed Lambda Calculus, and all the variants of the Lambda Calculus are part of mathematics. Hence any algorithm can be reduced to a mathematical formula, which US patent law states is not patentable subject matter. The computer science community has tried to explain this to the patent industry, but these explanations have fallen on deaf ears. So I thought I would try a different tack. Reference: http://paulspontifications.blogspot.com/2011/04/patent-5893120-reduced-to-mathematical.html (Ruling) http://www.groklaw.net/pdf2/BilskiScotus08-964.pdf (Slashdot) http://bit.ly/mI2Oew This is a very interesting argument for software being unpatentable. Mathematics FTW! Chris Penn... -- "As we open our newspapers or watch our television screens, we seem to be continually assaulted by the fruits of Mankind's stupidity." -Roger Penrose _______________________________________________ LinuxUsers mailing list LinuxUsers@socallinux.org http://socallinux.org/cgi-bin/mailman/listinfo/linuxusers
