From parametricity to conservation laws, via Noether's Theorem

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

1 Citation (Scopus)

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 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.
LanguageEnglish
Title of host publicationProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
EditorsPeter Sewell
Place of PublicationNew York
Pages491-502
Number of pages12
DOIs
Publication statusPublished - Jan 2014
EventPOPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - San Diego, United States
Duration: 22 Jan 201424 Jan 2014
http://popl.mpi-sws.org/2014/

Conference

ConferencePOPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
CountryUnited States
CitySan Diego
Period22/01/1424/01/14
Internet address

Fingerprint

Invariance
Computer programming languages
Conservation
Physics

Keywords

  • classical mechanics
  • conservation laws
  • higher-kinded types
  • invariance
  • relational parametricity

Cite this

Atkey, R. (2014). From parametricity to conservation laws, via Noether's Theorem. In P. Sewell (Ed.), Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 491-502). New York. https://doi.org/10.1145/2535838.2535867
Atkey, Robert. / From parametricity to conservation laws, via Noether's Theorem. Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. editor / Peter Sewell. New York, 2014. pp. 491-502
@inproceedings{547ac90da00040e5b6f4927d9a3acf5c,
title = "From parametricity to conservation laws, via Noether's Theorem",
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 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.",
keywords = "classical mechanics, conservation laws, higher-kinded types, invariance, relational parametricity",
author = "Robert Atkey",
year = "2014",
month = "1",
doi = "10.1145/2535838.2535867",
language = "English",
isbn = "9781450325448",
pages = "491--502",
editor = "Peter Sewell",
booktitle = "Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",

}

Atkey, R 2014, From parametricity to conservation laws, via Noether's Theorem. in P Sewell (ed.), Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, pp. 491-502, POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, United States, 22/01/14. https://doi.org/10.1145/2535838.2535867

From parametricity to conservation laws, via Noether's Theorem. / Atkey, Robert.

Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ed. / Peter Sewell. New York, 2014. p. 491-502.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - From parametricity to conservation laws, via Noether's Theorem

AU - Atkey, Robert

PY - 2014/1

Y1 - 2014/1

N2 - 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 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.

AB - 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 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.

KW - classical mechanics

KW - conservation laws

KW - higher-kinded types

KW - invariance

KW - relational parametricity

UR - http://bentnib.org/conservation-laws.html

UR - http://popl.mpi-sws.org/2014/

U2 - 10.1145/2535838.2535867

DO - 10.1145/2535838.2535867

M3 - Conference contribution book

SN - 9781450325448

SP - 491

EP - 502

BT - Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

A2 - Sewell, Peter

CY - New York

ER -

Atkey R. From parametricity to conservation laws, via Noether's Theorem. In Sewell P, editor, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York. 2014. p. 491-502 https://doi.org/10.1145/2535838.2535867