I learned how to reproduce the type inference system of the Calculus of Constructions in a (slight modification of) chemlambda . This comes with the previous caveats concerning untyped lambda beta calculus and chemlambda:
- (a) for any term (or type) there is a chemlambda molecule, but not for any chemlambda molecule there is a correspondent in CoC,
- (b) the inference rules are implemented as (compositions of) graph rewrites, but not all graph rewrites have a correspondent in the inference rules,
- (c) the reduction strategy (I think corresponding to the “tactics” from COQ) is an ingredient which has to be added in order to obtain a full model of computation,
- (d) all graph rewrites are local (i.e. there is an a priori bound on the number of nodes and arrows of the left and right pattern of graph rewrites, as well on the number of nodes and arrows needed to be taken into account in a condition in case the move has the form: if condition then replace left pattern by right pattern) ,
- (e) there is no correspondence between the reduction in chemlambda and reduction in CoC (in the sense that the reduction in chemlambda may pass by molecules which do not correspond to terms in CoC).
Some time is needed to eliminate possible bugs, but the task has become even bigger: a purely local version of COQ, based exclusively on graph rewrites, with “tactics” that never use values or names passing.
I have kept a distance, previously, from types because they seemed to me an added ingredient, not really needed, to the purity of a geometrical version of untyped lambda beta calculus. But slowly I understood that the initial try to mix emergent algebras (i.e. space as program) with lambda calculus. from http://arxiv.org/abs/1205.0139 , called “lambda-scale”, is a timid and a bit skew attempt for a type system.
Added over this is the fact that it’s hard, at least for me, to discern in the big literature on the subject, what holds for lambda beta, but not for any other “superior” version, because almost everywhere, if you don’t read carefully, extensionality is mixed in the pot by default, like in all famously well known category theory treatment of the matter.
Or, I have been forced from the beginning to exclude extensionality, because it appears as a non-local graph rewrite. That’s it, I have not made it on purpose, it turns out to be so. Without extensionality, no functions, so no functional style. Without terms and variable passing there is no evaluation, no call, lazy, by need, or otherwise.
There is something else happening here. I looked and found a (surprising) kind of historical precendent for this situation. At the beginning of chemistry, or even before the rigorous establishment of it, there has been a long and well looked functional period, when chemicals were identified with their function. (In popular thinking even now we speak or hear about the soothing quality of this herbal tea, say.) This was later called “vitalism”, and has been rejected on the grounds of the lack of enough explanatory power.
So I asked: regardless of the fashion of the moment, if you think that untyped lambda beta is Turing universal, then why use extension (or types btw)? What gives a geometrized version (and enlarged, in the sense (a, b, c, e) from the beginning of this post) version of untyped lambda beta?
At the surface, of one takes a lazy look at my drawings from a year ago, it looks like known facts, mixed with crazy statements. But if you care to look better and read it, then you see that this geometrical view is quite different, because basically has no name, from the previous mentioned reasons.
Now the task is even bigger, so I have to settle for picking some proof of principle bits, which can be attained in finite time by myself.
I tried to go a bit into programming, of course that it works, the limit being only my procrastination in front of so many possible choices.
Not quite, even with the small attempts contained in the chemlambda gui, a patch of awk, sh and js scripts, I am drowned in data.
The field is huge, probably will got bigger.