Curry-Howard correspondence

Discussions worth keeping around later.
Post Reply
rotting bones
Avisaru
Avisaru
Posts: 409
Joined: Thu Sep 07, 2006 12:25 pm

Curry-Howard correspondence

Post by rotting bones »

People with hippocampal brain damage often have unreliable memory, an obsession with philosophy, and graphomania. Since I suffer from all these symptoms, I've embarked on my next useless project.

According to the Curry-Howard correspondence, propositions are types and proofs are programs. The most common type theories in use today seem to be intensional type theory, extensional type theory, and the current subject of research, homotopy type theory.

The research world seems to be moving in the direction of ideal math, but as an adherent of naturalism, I want to be able to say that a proof or a program is any consistent generalization of a physical process. In that interpretation, propositions or types seem to include the physical states undergoing processing, as it were, and their consistent generalizations. I noticed that substituting the known laws of nature in formalizations of causality like this and this in Agda allows me to obtain an expression corresponding to the set of valid programs within the framework of naturalism mapped to their currently known implementations.

To that end, I'm maniacally collecting every known law of nature expressed at the causal level. Just to be clear: Apart from being a plot point in the story set in my conworld, this enterprise has no practical applications I can think of at the moment. Anyway, this requires me to ignore physical laws that are beautiful in their simplicity in favor of nasty, lower level, nuts-and-bolts type equations. Does anyone know of a comprehensive list of such equations? Thanks!

PS. An example might be helpful. If F=ma and you could determine the F and the m while measuring the a, then that process would function as a divider. But that is only one possible abstraction of a real process to which that would be an applicable equation. The idea is to apply this principle to all the laws of physics strung together in every relevant permutation. Wonder if I'll get far enough to have the computer stop working. Any help would be welcome.
If you hold a cat by the tail you learn things you cannot learn any other way. - Mark Twain

In reality, our greatest blessings come to us by way of madness, which indeed is a divine gift. - Socrates

Post Reply