Groups are numbers (3). Axiom (convex)

This post will be updated as long as the em draft will progress. Don’t just look, ask and contribute.

UPDATE 3: Released: arXiv:1807.02058.

UPDATE 2: Soon to release. I found something so beautiful that I took two days off, just to cool down. Wish I release this first em-convex article in a week, because it does not modify the story told in that article. Another useful side-effect of writing this is that I found a wrong proof in arXiv:0804.0135 so I’ll update that too.

UPDATE: Don’t mind too much my rants, I have this problem, that what I am talking about is in the future with respect to what I show. For example I tried to say it several times, badly! that chemlambda may be indeed related to linear logic, because both are too commutative. Chemlambda is as commutative as linear logic because in chemlambda we can do the shuffle. Or the shuffle is equivalent with commutativity, that’s what I tried to explain last time in Groups are numbers (1). There is another, more elaborate point of view, a non-commutative version of chemlambda, in the making. In the process though, I went “oh, shiny thing, what’s that” several times and now I (humbly try to) retrace the correct steps, again, in a form which can be communicated easily. So don’t mind my bad manners, I don’t do it to look smart./

The axiom (convex) is the key of the Groups are numbers (1) (2) thread. Look at this (as it unfolds) as if this is a combination of:

  • the construction of the field of numbers in projective geometry and
  • the Gleason and Montgomery-Zippin solution to the Hilbert 5th problem

I think I’ll leave the (sym) axiom and the construction of coherent projections for another article.

Not in the draft available there are about 20 pages about the category of conical groups, why it is not compact symmetric monoidal (so goodbye linear logic) but it has as a sub-category Hilb. Probably will make another article.

I sincerely doubt that the article form will be enough. I can already imagine anonymous peer reviews where clueless people will ask me (again and again) why I don’t do linear logic or categorical logic (not that it is useless, but it is in the present form heavily influenced by a commutative point of view, is a fake generalization from a too particular particular case).

A validation tool would be great. Will the chemlambda story repeat, i.e. will I have to make, alone, some mesmerizing programs to prove what I say works? I hope not.

But who knows? Very few people deserve to be part of the Invisible College. People who have the programming skills (the easy part) and the lack of prejudices needed to question linear logic (the hard, hacker part).

 

Advertisements

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.

Three interesting points

Because I’m not sure if I’m going to use Github in the future, instead of contributing to the em repository, I attach here the actual version of the em rewrite system paper. You know how it is: more you write, less goes into the final result.

The goal is to build a lambda calculus style version of emergent algebras, so that emergent algebras become a semantic for this system. One of the problems is that emergent algebras are partly algebraic and partly topological, involving uniform convergence and uniform continuity. But on the other side all this topological frame is not really needed, hence let’s pass it to the semantic side and see what we really have: the em.

The paper is not finished, it still needs developments:

  • booleans and naturals encodings
  • the sym rewrite and symmetric space like naturals
  • the sym and the convex rewrites are a fork for two kinds of numbers, this needs to be explored more [update: no, I proved that (convex) implies (sym) and that (convex) is far more rigid than (sym) because it leads only to commutative stuff, but it’s nice to know, because it gives a sort of axiomatization of FinVect and classical calculus starting from rewrites on trees, no modules, no fields, everything gets constructed from trees.]

_______________________________________

Another interesting thing is Victor Maia absal-ex repository. He continues his abstract algorithm explorations. The rewrites are close but not the same as mine, on the contrary his buffer representation of graphs is essentially what I do in needs, see also chemlambda strings for non tehnical explanations. I have the needs algorithm (libraries not public in needs repository) and the theoretical treatment, as a permutation rewrite machine, since a year, maybe one day I’ll post them if you are interested and motivate me to do it. Victor has superb programming skills and I wish him the best in his independent research work, looking forward to see how the abstract algorithm develops further.

_______________________________________

And I’m really curious what King is cooking in the   RKoD-web   repository. He’s the guy who did chemlambda-hask version in Haskell of chemlambda, he’s highly gifted and very young, watch him doing stuff!

_______________________________________

“Hey Mr. Gates”

The last paragraph of the premonitory post from 2011 We need a Github for science reads:

Hey Mr. Gates

It may be that the activation energy required to initiate changes won’t arise within the system. In that case, an outside push might do the job, and the best place for this push to come from may be a nimble funding agency. For example, a request for proposals could specify that phase II funding decisions would be based on the impact of online resources developed in phase I, as measured by specific metrics developed with community feedback. Nothing makes a scientist contemplate change faster than a new source of grant money, and the only thing better than a faculty applicant with a paper in Science may be one bringing in a multimillion dollar grant.”

Don’t believe this anymore. I made the same mistake several times, for example:

The news about Github show how naive that is.

We do need a Github for science. (One strong candidate is Zenodo, which does not offer AFAIK anything comparable with a github.io page where I can mix explanations with js scripts.) We also need a Google for science,  academic research management for science, etc.