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 is by Noether's theorem a consequence of a system's invariance under timeshifting.
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.
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.
Original language  English 

Title of host publication  Proceedings of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages 
Editors  Peter Sewell 
Place of Publication  New York 
Pages  491502 
Number of pages  12 
DOIs  
Publication status  Published  Jan 2014 
Event  POPL 2014: 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages  San Diego, United States Duration: 22 Jan 2014 → 24 Jan 2014 http://popl.mpisws.org/2014/ 
Conference
Conference  POPL 2014: 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages 

Country/Territory  United States 
City  San Diego 
Period  22/01/14 → 24/01/14 
Internet address 
Keywords
 classical mechanics
 conservation laws
 higherkinded types
 invariance
 relational parametricity
Fingerprint
Dive into the research topics of 'From parametricity to conservation laws, via Noether's Theorem'. Together they form a unique fingerprint.Profiles

Bob Atkey
 Computer And Information Sciences  Senior Lecturer
 Mathematically Structured Programming
Person: Academic