goodmath
goodmath | July 31, 2006Today we'll finally get to building the categories that provide the model for
the multiplicative linear logic. Before we jump into that, I want to explain why it is that we separate out the multiplicative part.
Remember from the simply typed lambda calculus, that [we showed that the type system was precisely a subset of intuitionistic logic][lambda-type], and that programs in the lambda calculus corresponded to proofs in the type system. In particular, it was propositional intuitionistic logic using only the "→" operation. Similarly, if you build up a more interesting typed lambda calculus…
goodmath | July 26, 2006In the comments on [my post mocking Granville Sewell's dreadful article][sewell], one of the commenters asked me to write something about why evolution is frequently modeled as a search process: since there is no goal or objective in evolution, search seems like a strange approach. It's a very good question, and so I'm going to do my best to give you a very good answer.
As I've said before, math is all about *abstraction*: taking something, stripping it to its bare-bones essentials, and seeing what it means: for example category theory, which I've been writing about for the last month, is…
goodmath | July 26, 2006Things are a bit busy at work on my real job lately, and I don't have time to put together as detailed a post for today as I'd like. Frankly, looking at it, my cat theory post yesterday was half-baked at best; I should have held off until I could polish it a bit and make it more comprehensible.
So I'm going to avoid that error today. Since we've had an interesting discussion focusing on the number zero, I thought it would be fun to show what zero means in category theory.
There are two zeros it category theory: the zero object, and the zero arrow.
Zero Objects
--------------
The zero object…
goodmath | July 25, 2006So, we're still working towards showing the relationship between linear logic and category theory. As I've already hinted, linear logic has something to do with certain monoidal categories. So today, we'll get one step closer, by talking about just what kind of monoidal category. As I keep complaining, the problem with category theory is that anytime you want to do something interesting, you have to wade through a bunch of definitions to set up your structures. I'll do my best to keep it short and sweet; as short as it is, it'll probably take a bit of time to sink in.
First, we need a…
goodmath | July 21, 2006Back during the DonorsChoose fundraiser, I promised a donor that I'd write an article about the math of zero. I haven't done it yet, because zero is actually a suprisingly deep subject, and I haven't really had time to do the research to do it justice. But in light of the comment thread that got started around [this post][fspog] yesterday, I think it's a good time to do it with whatever I've accumulated now.
History
---------
We'll start with a bit of history. Yes, there's an actual history to zero!
In general, most early number systems didn't have any concept of "zero". Numbers, in early…
goodmath | July 19, 2006Time to come back to category theory from out side-trip. Category theory provides a good framework for defining linear logic - and for building a Curry-Howard style type system for describing computations with *state* that evolves over time. Linear logic provides a way of defining a valid *model* for part of linear logic (the multiplicative operators) that aren't tractable using other modeling techniques.
I'm going to show you the relationship between models for linear logic and category theory. It's going to take a couple of days to go through the whole shebang, but even the parts that we…
goodmath | July 17, 2006*(This post has been modified to correct some errors and add some clarifications in response to comments from alert readers. Thanks for the corrections!)*
Today, we're going to take a brief diversion from category theory to play with
some logic. There are some really neat connections between variant logics and category theory. I'm planning on showing a bit about the connections between category theory and one of those, called *linear logic* . But the easiest way to present things like linear logic is using a mechanism based on sequent calculus.
Sequent calculus is a deduction system for…
goodmath | July 14, 2006Via [Migrations][migrations], I've found out about a really beautiful computational biology paper that very elegantly demonstrates how, contrary to the [assertions of bozos like Dembski][dembski-nfl], an evolutionary process can adapt to a fitness landscape. The paper was published in the PLOS journal "Computational Biology", and it titled ["Evolutionary Potential of a Duplicated Repressor-Operator Pair: Simulating Pathways Using Mutation Data"][plos].
Here's their synopsis of the paper:
>The evolution of a new trait critically depends on the existence of a path of
>viable intermediates…
goodmath | July 12, 2006One of the questions that a ton of people sent me when I said I was going to write about category theory was "Oh, good, can you please explain what the heck a *monad* is?"
The short version is: a monad is a category with a functor to itself. The way that this works in a programming language is that you can view many things in programming languages in terms of monads. In particular, you can take things that involve *mutable state*, and magically hide the state.
How? Well - the state (the set of bindings of variables to values) is an object in a category, State. The monad is a functor from…
goodmath | July 11, 2006So, at last, we can get to Yoneda's lemma, as I [promised earlier][yoneda-promise]. What Yoneda's lemma does is show us how for many categories (in fact, most of the ones that are interesting) we can take the category C, and understand it using a structure formed from the functors from C to the category of sets. (From now on, we'll call the category of sets **Set**.)
So why is that such a big deal? Because the functors from C to the **Set** define a *structure* formed from sets that represents the properties of C. Since we have a good intuitive understanding of sets, that means that Yoneda's…
goodmath | July 10, 2006Today's contribution on category theory is going to be short and sweet. It's an example of why we really care about [natural transformations][nt]. Remember the trouble we went through working up to define [cartesian categories and cartesian closed categories][ccc]?
As a reminder: a [functor][functor] is a structure preserving mapping between categories. (Functors are the morphisms of the category of small categories); natural transformations are structure-preserving mappings between functors (and are morphisms in the category of functors).
Since we know that the natural transformation can…
goodmath | July 6, 2006We're almost at the end of this run of category definitions. We need to get to the point of talking about something called a *pullback*. A pullback is a way of describing a kind of equivalence of arrows, which gets used a lot in things like interesting natural transformations. But, before we get to pullbacks, it helps to understand the equalizer of a pair of morphisms, which is a weaker notion of arrow equivalence.
We'll start with sets and functions again to get an intuition; and then we'll work our way back to categories and categorical equalizers.
Suppose we have two functions mapping from…
goodmath | July 4, 2006What's a subset? That's easy: if we have two sets A and B, A is a subset of B if every member of A is also a member of B.
What's a subgroup? If we have two groups A and B, and the values in group A are a subset of the values in group B, then A is a subgroup of B.
For any kind of thing **X**, what does it mean to be a sub-X? Category theory gives us a way of answering that in a generic way. It's a bit hard to grasp at first, so let's start by looking at the basic construction in terms of sets and subsets.
The most generic way of defining subsets is using functions. Suppose we have a set, A.…
goodmath | June 27, 2006Before I dive into the depths of todays post, I want to clarify something. Last time, I defined categorical products. Alas, I neglected to mention one important point, which led to a bit of confusion in the comments, so I'll restate the important omission here.
The definition of categorical product defines what the product looks like *if it's in the category*. There is no requirement that a category include the products for all, or indeed for any, of its members. Categories are *not closed* with respect to categorical product.
That point leads up to the main topic of this post. There's a…
goodmath | June 26, 2006On my way home from picking up my kids from school, I heard a story on NPR that included a line from one of the editors of the New England Journal of Medicine, which I thought was worth repeating here.
They were discussing an article in this month's NEJM about [vioxx/rofecoxib][nejm]. The article is a correction to an earlier NEJM article that concluded that the cardiac risks of Vioxx were not really significant until around 18 months of continued use. With more data available, it appears that the 18 month was just an artifact, not a real phenomenon, and the data appears to show that the…
goodmath | June 25, 2006In the comments to one of my earlier [Demsbki][demsbki-info-theory] posts, I was responding to a comment by a poster, and realized that what we were discussing was probably interesting enough to promote up to a front-page post.
A poster named [Garote][garote] said:
>I think PaulC said exactly what needs to be said, that grants us all
>hearty permission to ignore Dembski's work. I think it bears repeating:
>
>"If I am betting on coin flips and notice any kind of algorithmic pattern then
>there are legitimate reasons to conclude that the person flipping coins is not
>playing…
goodmath | June 24, 2006Back when I first started this blog on blogspot, one of the first things I did was write an introduction to information theory. It's not super deep, but it was a decent overview - enough, I thought, to give people a good idea of what it's about, and to help understand why the common citations of it are almost always misusing its terms to create bizzare conclusions, like some ["law of conservation of information",][conservation]
[conservation]: http://en.wikipedia.org/wiki/Law_of_conservation_of_information "wikipedia on Dembski's law of CoI"
This is a slight revision of that introduction. For…
goodmath | June 22, 2006 Sorry, but I actually jumped the gun a bit on Yoneda's lemma.
As I've mentioned, one of the things that I don't like about category theory is how definition-heavy it is. So I've been trying to minimize the number of definitions at any time, and show interesting results of using the techniques of category theory as soon as I can.
Well, there are some important definitions which I haven't talked about yet. And for Yoneda's lemma to make sense, you really need to see some more examples of how categories express structure. And to be able to show how category theory lets you talk about…
goodmath | June 21, 2006Harald Hanche-Olsen, in the comments on my earlier post about the Principia Mathematica, has pointed out that this months issue of the Notices of the American Mathematical Society is a special issue in honor of the 100th anniversary of Kurt Gödels birth. The entire issue is available for free online
I haven't read much of the journal yet; but Martin Davis's article The Incompleteness Theorem is a really great overview of the theorem abnd the proof, how it works, and what it means.
goodmath | June 19, 2006The thing that I think is most interesting about category theory is that what it's really fundamentally about is structure. The abstractions of category theory let you talk about structures in an elegant way; and category diagrams let you illustrate structures in a simple visual way. Morphisms express the structure of a category; functors are higher level morphisms that express the structure of relationships between categories.
In my last category theory post, one of the things I mentioned was how category theory lets you explain the idea of symmetry and group actions - which are a kind of…