DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics.
Maxwell's Demon, 'a being whose faculties are so sharpened that he can follow every molecule in its course', has been the centre of much debate about its abilities to violate the second law of thermodynamics. Landauer's hypothesis, that the Demon must erase its memory and incur a...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2015-11-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1511.01566v1 |
| _version_ | 1818418174558732288 |
|---|---|
| author | Samson Abramsky Dominic Horsman |
| author_facet | Samson Abramsky Dominic Horsman |
| author_sort | Samson Abramsky |
| collection | DOAJ |
| description | Maxwell's Demon, 'a being whose faculties are so sharpened that he can follow every molecule in its course', has been the centre of much debate about its abilities to violate the second law of thermodynamics. Landauer's hypothesis, that the Demon must erase its memory and incur a thermodynamic cost, has become the standard response to Maxwell's dilemma, and its implications for the thermodynamics of computation reach into many areas of quantum and classical computing. It remains, however, still a hypothesis. Debate has often centred around simple toy models of a single particle in a box. Despite their simplicity, the ability of these systems to accurately represent thermodynamics (specifically to satisfy the second law) and whether or not they display Landauer Erasure, has been a matter of ongoing argument. The recent Norton-Ladyman controversy is one such example.
In this paper we introduce a programming language to describe these simple thermodynamic processes, and give a formal operational semantics and program logic as a basis for formal reasoning about thermodynamic systems. We formalise the basic single-particle operations as statements in the language, and then show that the second law must be satisfied by any composition of these basic operations. This is done by finding a computational invariant of the system. We show, furthermore, that this invariant requires an erasure cost to exist within the system, equal to kTln2 for a bit of information: Landauer Erasure becomes a theorem of the formal system. The Norton-Ladyman controversy can therefore be resolved in a rigorous fashion, and moreover the formalism we introduce gives a set of reasoning tools for further analysis of Landauer erasure, which are provably consistent with the second law of thermodynamics. |
| first_indexed | 2024-12-14T12:18:29Z |
| format | Article |
| id | doaj.art-2e1f02df5542451786e048976b061f79 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-14T12:18:29Z |
| publishDate | 2015-11-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-2e1f02df5542451786e048976b061f792022-12-21T23:01:34ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802015-11-01195Proc. QPL 201511610.4204/EPTCS.195.1:52DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics.Samson Abramsky0Dominic Horsman1 University of Oxford University of Oxford Maxwell's Demon, 'a being whose faculties are so sharpened that he can follow every molecule in its course', has been the centre of much debate about its abilities to violate the second law of thermodynamics. Landauer's hypothesis, that the Demon must erase its memory and incur a thermodynamic cost, has become the standard response to Maxwell's dilemma, and its implications for the thermodynamics of computation reach into many areas of quantum and classical computing. It remains, however, still a hypothesis. Debate has often centred around simple toy models of a single particle in a box. Despite their simplicity, the ability of these systems to accurately represent thermodynamics (specifically to satisfy the second law) and whether or not they display Landauer Erasure, has been a matter of ongoing argument. The recent Norton-Ladyman controversy is one such example. In this paper we introduce a programming language to describe these simple thermodynamic processes, and give a formal operational semantics and program logic as a basis for formal reasoning about thermodynamic systems. We formalise the basic single-particle operations as statements in the language, and then show that the second law must be satisfied by any composition of these basic operations. This is done by finding a computational invariant of the system. We show, furthermore, that this invariant requires an erasure cost to exist within the system, equal to kTln2 for a bit of information: Landauer Erasure becomes a theorem of the formal system. The Norton-Ladyman controversy can therefore be resolved in a rigorous fashion, and moreover the formalism we introduce gives a set of reasoning tools for further analysis of Landauer erasure, which are provably consistent with the second law of thermodynamics.http://arxiv.org/pdf/1511.01566v1 |
| spellingShingle | Samson Abramsky Dominic Horsman DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics. Electronic Proceedings in Theoretical Computer Science |
| title | DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics. |
| title_full | DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics. |
| title_fullStr | DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics. |
| title_full_unstemmed | DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics. |
| title_short | DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics. |
| title_sort | demonic programming a computational language for single particle equilibrium thermodynamics and its formal semantics |
| url | http://arxiv.org/pdf/1511.01566v1 |
| work_keys_str_mv | AT samsonabramsky demonicprogrammingacomputationallanguageforsingleparticleequilibriumthermodynamicsanditsformalsemantics AT dominichorsman demonicprogrammingacomputationallanguageforsingleparticleequilibriumthermodynamicsanditsformalsemantics |