Conservation laws for free!

In this year's POPL, Bob Atkey made a splash by showing how to get from parametricity to conservation laws, via Noether's theorem:

Invariance is of paramount importance in programming languages and in physics. In programming languages, John Reynolds’ theory of relational parametricity demonstrates that parametric polymorphic programs are invariant under change of data representation, a property that yields “free” theorems about programs just from their types. In physics, Emmy Noether showed that if the action of a physical system is invariant under change of coordinates, then the physical system has a conserved quantity: a quantity that remains constant for all time. Knowledge of conserved quantities can reveal deep properties of physical systems. For example, the conservation of energy, which by Noether’s theorem is a consequence of a system’s invariance under time-shifting.

In this paper, we link Reynolds’ relational parametricity with Noether’s theorem for deriving conserved quantities. We propose an extension of System Fω with new kinds, types and term constants for writing programs that describe classical mechanical systems in terms of their Lagrangians. We show, by constructing a relationally parametric model of our extension of Fω, that relational parametricity is enough to satisfy the hypotheses of Noether’s theorem, and so to derive conserved quantities for free, directly from the polymorphic types of Lagrangians expressed in our system.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


cool. Is anyone aware of work in the opposite (generating program invariants via traditionally physical means) direction? Example: the allocation field over the tetrahedron of the classic even/odd mutual recursion is irrotational, which suggests it can be compiled to run in constant space.


I skimmed the paper. I don't get it. (That's not saying much.) I saw that they had type systems for various physical simulations? Anybody take a stab at explaining with some bullet points what this is all cool for? :-)

tiger, tiger, for-all bright...

The cool part is that they didn't have type systems for physical simulations, they had type systems for physical equations. (which are applied in expressing physical laws[0])

A brief detour: Iverson's Turing Award lecture starts slowly[1], in order to introduce his notation. On p 447, we find De Morgan's law expressed as:

∧/B ↔ ~∨/~B

which is equivalent to

~∧/B ↔ ∨/~B

which, in a more common pseudocode notation, becomes

not(all(bs)) == any(map(not)(bs))

note the correspondence (on a purely formal, uninterpreted level), with

len(cat(ss)) == sum(map(len)(ss))

These types of equivalence all have something in common: list parametricity[2] (for instance, in the latter, we might use the typing len : ∀τ. List(τ) → Nat)

What Atkey is saying is that one can use the same kind of typing to formally express what physicists informally do when their work remains invariant under arbitrary smooth transformations, or mathematicians informally do when they reason "without loss of generality". For instance, it's fundamental to 'area' that it remain the same under translations and rotations, and so in their system a function which computed areas would also have an ∀τ syntax showing up in its type (where tau in this case would vary over geometric congruences, à la haskell's type class constraints?). So we'd get:

area(union(ps)) == sum(map(area)(ps))

where area may be taken under an arbitrary (fuzzed) congruence, to express that[3] we can move an object around, and measure it, or we can break it into pieces, move those —independently!— around, then sum the measurements; either way[4] we arrive at the same answer.

Now, I haven't even skimmed the paper yet, but my guess is that their examples are just rederivations of physical results: adding the types hasn't told us anything we didn't already know.

Where the formalization becomes interesting is the degree to which it can reduce an activity which previously required thought[5] to one of pushing symbols around. Noether demonstrated that symmetries and conservation laws[6] are related, and the promise of this work is that it should allow one to read symmetries (and hence the invariants) directly off the types.

[0] Einstein's revolution, under parallel transport to informatics concepts, becomes something like: "Obviously the UNCOL thing only works within small islands of adoption, so in general we should have some ways to couple physical measurements like garden hose--screw in another segment when it becomes when it becomes necessary to massage data in another way".
[1] by §4.3 p.458 his definitions D.3 and D.4 capture the essence of google's map-reduce; this correspondence should not be unexpected, as people have had accounting problems with a similar structure from well before the punched-card era.
[2] compare (Osborne) Reynold's Operators (aiding symbolic manipulation at the top of a symbol DAG, not down at the leaves of a particular representation) with (John) Reynold's Parametric Types (aiding symbolic manipulation at the top of a symbol DAG, not down at the leaves of a particular representation)
[3] at least for regular objects, pace Banach-Tarski
[4] applications to the military-industrial complex have also been long-standing: Galileo showed that in determining how much higher one should point a cannon barrel, it doesn't really matter in what direction it is facing.
[5] how much thought? do physicists also find this work interesting? or would they view it as abstract nonsense? cf Feynman's French Curve story...
[6] compare the adjoints used for the parlor trick in dual photography
(which shows that we can arbitrarily shuffle the transfer function of a scene in between illumination and measurement) with
deep and shallow embeddings (which shows that we can arbitrarily shuffle the interpretation of a data structure in between writing and reading)

[Edit: s/et. al. are/is/]

Atkey et al.

Bob didn't collaborate on this work, so he should get full credit for it :).

(Though this work did arise in the context of Atkey's collaboration with Johann and Kennedy about units of measurements in geometry.)

mea culpa

Oops — next time I should at least skim before replying! :-)