You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Owen Lynch (Dec 01 2021 at 17:08):One thing that is bothering me about various approaches to thermodynamics that look at a state space of states is that when the system transitions from having 2 moles of hydrogen gas to 1 mole of hydrogen gas, that hydrogen gas HAS TO GO SOMEWHERE.
Owen Lynch (Dec 01 2021 at 17:09):This is a problem that, say, the lattice gas in statistical mechanics does not have.
Owen Lynch (Dec 01 2021 at 17:10):And is also a problem that classical mechanics does not have: if a ball rolls from one place to another, it might convert some potential energy into kinetic energy or vise versa, but it need not necessarily give anything to the outside world.
Owen Lynch (Dec 01 2021 at 17:14):Therefore, even when looking at quasistatic paths, we still must consider flows. When two thermodynamical systems are connected, they exchange mass, heat, etc. We need a formalism that takes into account that these quantities must be conserved.
John Baez (Dec 01 2021 at 20:25):One thing that is bothering me about various approaches to thermodynamics that look at a state space of states is that when the system transitions from having 2 moles of hydrogen gas to 1 mole of hydrogen gas, that hydrogen gas HAS TO GO SOMEWHERE.
Details, details. :upside_down:
What sort of transition are we talking about here? Hydrogen leaking out of a balloon? Going to the great big heat bath in the sky?
Owen Lynch (Dec 01 2021 at 20:55):It's a good question. My feeling is that system should have a boundary, and that we can use that boundary by either gluing together multiple systems along their boundary, or by imposing "boundary conditions" by fiat. In the first case, anything that leaves through a boundary must end up in another system. In the second case we might impose boundary conditions by fiat, and things can go in and out of the boundary into whatever.
Matteo Capucci (he/him) (Dec 03 2021 at 09:31):Owen Lynch said:
One thing that is bothering me about various approaches to thermodynamics that look at a state space of states is that when the system transitions from having 2 moles of hydrogen gas to 1 mole of hydrogen gas, that hydrogen gas HAS TO GO SOMEWHERE.
This smells a lot like a linearity condition, in the sense of [[linear types]].
In our work on cybernetics, we use biparametrised morphisms (see here) to do keep track of shared resource usage.
The rough, intuitive idea is that to string diagrams which describe your system, and we draw from left to right, you add a `vertical', top to bottom, direction representing shared global state. Incoming vertical wires are resources you take from the environment, outgoing vertical wires are resources you release to the environment. If the monoidal category you draw this diagrams for is not cartesian or affine, then you're forced by the linearity of its type system to always keep a balance of incoming and outgoing resources.
Owen Lynch (Dec 04 2021 at 16:52):Can linear types model continuous resources? Also, I'm realizing that there are actually quantities that we don't want to conserve. For instance, rotation is not conserved, because we can use a gearbox to step up the rate of turning while decreasing the torque, or vice versa. However "angular work" is conserved, which is torque times rotation.
Matteo Capucci (he/him) (Dec 06 2021 at 21:17):Owen Lynch said:
Can linear types model continuous resources?
I think you need quantitative type theories for that: http://www.t-news.cn/Floc2018/FLoC2018-pages/proceedings_paper_665.pdf
They generalise LTT in annotating terms with quantities taking values in arbitrary semirings (such as ).
I don't know much about categorical semantics of QTT, the paper above works out some models.
Owen Lynch said:
Also, I'm realizing that there are actually quantities that we don't want to conserve. For instance, rotation is not conserved, because we can use a gearbox to step up the rate of turning while decreasing the torque, or vice versa. However "angular work" is conserved, which is torque times rotation.
Linear is more general than non-linear (counterintuitive terminology here, but think of intuinitionistic/classical logic), so you can have non-linear (i.e. non-conserved) resources in a linear setting.