Went to Philippa Gardner's talk on local Hoare reasoning about DOM manipulations. It was the most reasonable talk about that nasty stuff you typically do with javascript I've ever heard. Turns out separation logic generalizes nicely to a situation where the separating conjunction is replaced by the noncommutative relationship between a tree-with-hole and a subtree that goes in that hole.

After we all went to the new, not-on-fire Harris Grill. I had actually never been in its previous incarnation, but the place seems pretty nice on a first impression. Burgers there: tasty, if a bit expensive. Not sure how excited I'd be going there if the department wasn't footing the bill, but I ought to give Bacon Night a chance.

Attacked "Gauge Fields, Knots, and Gravity" some more. Hadn't looked at it for many months. Turns out it makes a little more sense now. There's a central beauty in differential geometry where the exterior derivative generalizes gradient (a map from 0-forms to 1-forms) curl (a map from 1-forms to 2-forms) and divergence (a map from 2-forms to 3-forms) in 3 dimensions, in a way that is usually hidden because we are taught to blithely hodge-star everything in sight, ignoring the difference between 1-forms and 2-forms, and between 0-forms and 3-forms.

And so I think I got another little bit of insight into what gauge invariance is, and it really is analogous to the very mundane sort of indifference Nature has to what you puny humans choose to call "zero volts" or "zero joules potential energy". These things tend to come from trying to assign notions of scalar potential to (co)vector fields like how we relate electric potential to conservative electric fields for instance. If we add a constant to the electric potential, the gradient operator doesn't give a shit, and gives us the same field out.

Likewise, if we have a vector potential A that gives a bivector field (like the magnetic field B for instance) then adding certain functions to A won't matter when deriving B as dA. In full generality these are the closed forms by definition, but the exact forms — those that arise as df for some 0-form f — are also closed by the pervasive feature of (co)chain complexes that d2 = 0. So our gauge freedom includes at the very least the addition of any gradient vector field to A. For n-forms with n greater than 1, we can add entire squiggly bizarre functions (as long as they are at least kinda well-behaved) and these additions are somehow not essentially different from how we can add a constant to all voltages or potential energies without changing the real physics going on. This I find pretty remarkable!

Also beginning to dimly see why physicists care about representation theory. Somehow the fact that U(1)'s representations are naturally indexed by natural numbers means that electric charge comes in discrete units, and SU(2)'s representations of dimension 2n+1 have something to with spin-n particles. Does this mean that spin is the canonical notion of "charge" for the weak force? The book didn't really seem to come out and say this in so many words.

---
The Baker-Campbell-Hausdorff formula seems eerily familiar...
Tags:
• #### (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• #### (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• #### (no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic