From parametricity to conservation laws, via Noether's Theorem
Atkey, Robert; Sewell, Peter, ed. (2014) From parametricity to conservation laws, via Noether's Theorem. In: Proceedings of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. ACM, USA, pp. 491502. ISBN 9781450325448 (https://doi.org/10.1145/2535838.2535867)
Preview 
Text.
Filename: Atkey_POPL2014_From_parametricity_to_conservation_laws_via_noethers_theorem.pdf
Accepted Author Manuscript Download (304kB) Preview 
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.
ORCID iDs
Atkey, Robert ORCID: https://orcid.org/0000000244145047; Sewell, Peter

Item type: Book Section ID code: 53504 Dates: DateEventJanuary 2014PublishedKeywords: classical mechanics, conservation laws, higherkinded types, invariance, relational parametricity, Electronic computers. Computer science, Computational Theory and Mathematics Subjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 26 Jun 2015 15:08 Last modified: 23 Nov 2021 02:01 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/53504