# From Parametricity to Conservation Laws, via Noether's Theorem

## Publication Information

Robert Atkey.

*From Parametricity to Conservation Laws, via Noether's Theorem*. In

*Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014)*. 2014.

DOI:

10.1145/2535838.2535867## Abstract

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.