Embracing the Laws of Physics: Three Reversible Models of Computation

The language they introduce, Π, is essentially a simple concatenative programming language where all of the primitive combinators happen to be reversible; the graphical depiction is essentially the same as graphical linear algebra¹, which is no coincidence. Concatenative combinator calculus is related to combinatory logic—specifically, it’s a variation that replaces application of combinators with composition, leading to a bunch of nice mathematical properties. Both of these logics have the nice feature that you can syntactically restrict the substructural rules of contraction (dropping), exchange (swapping), and weakening (copying): for example, a well-formed program that doesn’t use the K combinator to drop a value is guaranteed to be linear, i.e., not destroy any information. This isn’t true in ordinary lambda calculus, where you can use a variable zero or many times, so you need additional checks on the uses of a variable to determine whether a function is linear, affine, &c.

I like the theory of concatenative programming languages because they provide an elegant compositional/dataflow-oriented style of programming, have deep connections to linear logic, Hughes’ “arrows”, effects & coeffects, and quantum/reversible computation, while also admitting very efficient implementation on classical hardware.

I’m (very slowly) working on a statically typed low-level concatenative language that’s meant to provide all the nice high-level typed functional language features like higher-order functions, pipeline-style programming, and effects tracked in the types, while requiring no runtime support such as a tracing garbage collector—the ultimate goal is to allow a restricted subset that doesn’t even require a heap allocator, so you could use it to implement e.g. a kernel or device firmware. I hope that concatenative languages find their way to the mainstream as the basis for programming quantum and extremely low-power computing devices (which we will need in order to reduce emissions).

¹ https://graphicallinearalgebra.net/

>>Proposition IV. That axiom of metaphysicians which is termed the principle of contradiction, and which affirms that it is impossible for any being to possess a quality, and at the same time not to possess it, is a consequence of the fundamental law of thought, whose expression is x^2=x

>This “law” is reasonable in a classical world but is violated by the postulates of quantum mechanics

I think this might be a little bit of a stretch, if a particle is in a superposition of states it's not contradictory about which state it is in, it's just in a superposition of both. I think a good analogy for that would be your keyboard, which is located at the Q key as well as the M key.

The Feynman lectures on Computation provide good background on reversible computation from the perspective of a brilliant physicist.

https://www.scribd.com/doc/52657907/Feynman-Lectures-on-Comp...

for background:

https://en.wikipedia.org/wiki/Reversible_computing

https://en.wikipedia.org/wiki/Fredkin_gate

https://en.wikipedia.org/wiki/Toffoli_gate

Hmm would software like Nix function as a practical example of 'reversible computing'?

" both these fundamental physical theories imply that information is a conserved quantity of physical processes and hence of primitive computational operations."

No, actually they do not. Jayzus. Peer review is obviously dead.