Time for some code (Coq?)

The proofs for em start to be difficult to follow for a human, it happens like when I got into more complex chemlambda molecules, only this time

  • I don’t have code to verify/run them
  • I try to stick as much as possible to classical ways and notations

So I’d appreciate some help or advice, what to use? Haskell? Some proof assistants? Help needed here, this could turn into a fun code project.

UPDATE: Coq would be great.

UPDATE 2: Yes differential geometry can be formalized in Coq, CoC, etc. Hamiltonian mechanics for sure, QM almost sure, statistical thermodynamics is within reach. Only patience is needed. But for what? A pat on the back? A team would do this in 5 years, I’m not sure I’m willing to do this rewrite for reasons which suck. Probably will do it though for fun and fuck you. /

Here are some things I’d like to try with the help of code:

  • have all the proofs from the em paper written and verified
  • program in em REPL style
  • the trees notation I use are very close to writing, they are like forrests of trees, so a side effect of the notation is that it shortens considerably the exposition of the proofs (of course that trees are nice, if they are not too big, then even this tree notation does not fit on page). Some visual trick/code to help?
  • exploration of CONICAL the category of conical groups and the smaller CARNOT category. These are (severely) not compact symmetric monoidal categories, even if FinHilb can be made into a subcategory of CARNOT, FinVect too. Explain concretely why things break in interesting ways for CONICAL. Discover some new category stuff in the process.
  • btw why not make some categorical QM translation from FinHilb into CONICAL? Everything should work nice, just use the embedding. I don’t know what gives though, but it does use (Pansu) differentiability arguments instead of scalar products structures, hm.
  • this would really really interest me: build something which correspond to Gleason and Montgomery-Zippin, afaik their solution of the Hilbert 5th problem was not formalized.
  • naturals and booleans in em (which I keep private until everything before them works well) are very geometrical, so what does a program (ie an em term)  execution looks like in a particular geometry?
  • geometry of manifolds: alpha renaming in em
  • when the naturals (except 0) are invertible then we get two calculi, commutative and non-commutative, the non-comm looking down at the comm calculus (as Semmes would write). So we get to the frame of coherent projections for free (but in the same formal sense which replaces un iform convergence and continuity). Formalize sub-riemannian geometry, looks feasible.
  • or just forget all this math and write another semantics in terms of paths on maps. For this (written on paper) I need people who know deeply and rigorously the internet.

Probably some of these will happen and some not, because, with code available, 100X crazier ideas emerge.

And we’ll get from em to chemlambda, but there’s a lot of ground to cover.

Where? What to use? How to use?

Let me know, I’d appreciate.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s