April 25th, 2008

beartato phd

(no subject)

Reading a couple things jccw pointed me to the other day; A Dependent Type Theory with Names and Binding by Schöpp and Stark, and some slides of Swierstra's about version control. Turns out Darcs is a relatively principled VCS.

My categorical intuition tells me that most of what is going on there is really a category C whose objects are pieces of data, whose arrows are patches, equipped with a functor to a group G which is the "names" of those patches. That is, when I have a square
 A  / \  B
   /   \
  v     v
   \   /
 B  \ / A

Clearly the two copies of A (resp. two copies of B) are not the *same* change, but they have the same intention. The idea would be that the functor maps these down to the same group element.

neelk was talking to me for a bit about his attacking of separation logic with a labelled sequent calculus. Funny how (I → I) * A does entail (I → I) ^ A in that system, but (apparently) not in bunched logic. His axiomatization of the nontrival equality theory that involves hypothetical equalities doesn't permit the unificationesque decompositions that would allow you to infer a * b = a * c |- b * c, but I can't come up with a raw proposition that would lead to such an equational test.