ezyang's research log

What I did today. High volume, low context. Sometimes nonsense. (Archive)

Robert Atkey - From Parametricity to Conservation Laws, via Noether’s Theorem

Polymorphically Typed Langrangians => (by parametricity) Invariance Properties => (by Noether’s theorem) Conservation Laws for Physical Systems

This is a point. (chuckles). We have coordinates for this point (completely arbitrary based on origin), but they are related by a change in origin (two different representations). The idea is to incorporate over the “change of origin” in the type system.

Here are two points, here are vectors from an origin; here is another origin; now if we subtract the two vectors, we get something independent from the choice of origin.

What’s the difference between a program that takes a pair of points (f) and a pair of vectors (g)? Well, in ML, they have the same type: ℝ² × ℝ² = ℝ (you might as well write Scheme). The key is that points vary in change of origin. So f should be invariant over change in origin.

Do it with types? Higher kinded types. Let ℝ² be indexed by a two dimensional transformation group; so now f quantifies over all transformation groups and g only allows zero. And the interpretation does the usual. (Anyway, this is last year’s paper.)

So what can we use these invariance properties for?

Let’s start with Lagrangian Mechanics, a branch of analytic mechanics, reformulating Newtonian mechanics. A Langrangian is a function of time and positions and velocities of all the particles. Typically, this is just the kinetic energy - the potential energy. An example of two particles connected by a spring, then L(t,x₁,x₂,ẋ₁,ẋ₂)… etc. Then in Lagrangian mechanics, we have an “action” which is the sum of the Lagrangian over time. Then the principle of stationery action: it says, well, choose a point, take the derivative S with respect to Q; we want to get a maximum or minimum. Imagine a point. Well, this is the case when some Euler-Lagrange equations form. The notation is confusing, but everything works out in the end. You get a system of ODEs and physically realisable paths, you get the initial positions and velocities, and you can figure out the system.

An interesting thing is Newton’s second law is derived.

Now, Noether’s theorem gives us conservation laws. This says that there are properties of a system which do not change over time. Noether’s says if there is a continuous symmetry, then there is a corresponding conservation law. So the key is these will be like FREE VARIABLES.

An action is invariant if, when we shove everything around by these two transformations, we get a new path by just doing something.

Going back to the type system:

My understanding of how Standard Model was ofrmed, was they

Q: It’s a dream of mine to study Noether’s theorem for years. Perhaps I’ll do it this way. I think there are couple of misconceptions of theapplication. You suggest that these symmetries were passive symmetries, arising from the coordinate system.

A: I did worry about that.

Q: Yes. Because if you reread that, the symmetry … I had seven more questions.

Q: You did everything with vector spaces, where really you should have done smooth manifolds.

A: It’s that case too, but I thought I didn’t have space to explain manifolds (it went smoothly in any case)

Q: (Neel) There is a lot of work on parametricity in the presence of effects. Does that get you conservation properties for not entirely conservative systems?

A: I don’t know. (I mean, non-(indistinct) Lagrangians). I don’t know how that relates to effects.

Q: I’m not a physicist, but it seems usually conservation properties are proved with symbolic evalution. What’s the relationship between the TT interpretation and the usual proofs?

A: Usually, they would just look at the Lagrangian and prove it by hand, or build it from standard parts (you knew they were invariant). In practice, when they prove these things, they do a lot of work to try to make it hard to write things that are wrong, using special notations. So informally, they are using type systems. Here, they write down the type before they start. (Are there benefits for modularity?) Maybe? In practice, they fit on a page.