On Wed, Jun 22, 2011 at 12:06 AM, Arnaud Bailly <arnaud.oq...@gmail.com>wrote:
> Thanks Sebastien, > This paper has passed in my radar's field but I must confess that > although I think I grasped the idea, I was quickly lost in the > profusion of symbols and notations. I am no mathematician, only a > simple developer, although I am fascinated by several topics in > mathematics so my attention tend to drop sharply when confronted with > more or less complex proofs and layers of defintions and mappings. > Please read http://en.wikipedia.org/wiki/Abstract_interpretation . Keep in mind that it applies to /all/ formal languages, including programming languages and the languages of mathematics. There are two hard phases of becoming a mathematician: understanding the symbolism, and understanding when/how to skip over new symbolism/notation. After all, every mathematician is taught a slightly different version of mathematics. If we are to communicate with each other, we have to elide the differences. "Abstract interpretation" is a formal method of doing that for computer languages. It also helps when you understand the relationships between theorems, free functions, free structures, and so on. (I.e., they are the same things seen from different points of view, and always can be skipped when trying to interpret/understand, because they are always "true") If you're looking for books on the subject, take a look at Topoi: The Categorical Analysis of Logic. It isn't a book /about/ category theory (it has a decent introduction), but it builds up various logics using categorical constructs. It aims to show that Category theory can become a "foundation" for mathematics. But since every constructive logic *is a* programming language, it builds up the theory of computation in a very general way. Also, I would suggest drawing diagrams to represent your programs during the design phase. Use your own notation if you don't know the 'standard' notation for an idea. A fair bit of category theory is "refactoring" these ad hoc diagrams into pieces that each express a single idea, at least to get the intuition behind the single ideas taken together.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
