Rules of lambda epsilon calculus

I updated the paper on lambda epsilon calculus.  See the link to the actual version (updated daily) or check the arxiv article, which will be updated as soon as a stable version will emerge.

Here are the rules of this calculus:

(beta *) $(x \lambda A) \varepsilon B= (y \lambda (A[x:=B])) \varepsilon B$ for any fresh variable $y$, (R1) (Reidemeister one) if $x \not \in FV(A)$ then $(x \lambda A) \varepsilon A = A$ (R2) (Reidemeister two) if $x \not \in FV(B)$ then $(x \lambda ( B \mu x)) \varepsilon A = B (\varepsilon \mu ) A$ (ext1) (extensionality one)  if $x \not \in FV(A)$ then $x \lambda (A 1 x) = A$ (ext2) (extensionality two) if $x \not \in FV(B)$ then $(x \lambda B) 1 A = B$ These are taken together with usual substitution and $\alpha$-conversion.

The relation between the operations from $\lambda \varepsilon$ calculus and emergent algebras is illustrated in the next figure. Lambda epsilon calculus, an attempt for a language of “computing with space”

Just posted on the arxiv the paper Lambda calculus combined with emergent algebras.   Also, I updated my page on emergent algebras and computing with space, taking into consideration what I try to do in the mentioned paper. Here are some excerpts (from the mentioned page) about what I think now “computing with space” may be:

 Let’s look at some examples of spaces, like: the real world or a virtual world of a game, as seen by a fly or by a human, “abstract” mathematical spaces as manifolds, fractals, symmetric spaces, groups, linear spaces. To know what a space is, to define it mathematically, is less interesting than to know what one can do in such a space. I try to look at spaces from a kind of a “computational viewpoint”. A model of such a computation could be the following process: Alice and Bob share a class of primitives of spaces (like a common language which Alice can use in order to communicate to Bob what she sees when exploring the unknown space). Alice explores an unknown territory and sends to Bob the operational content of the exploration (i.e. maps of what she sees and how she moves, expresses in the common language ). Then Bob, who is placed in a familiar space, tries to make sense of the maps received from Alice. Usually, he can’t put together in the familiar the received information (for example because there is a limit of accuracy of maps of the unknown territory into the familiar one). Instead, Bob tries to simulate the operational content of Alice exploration by interpreting the messages from Alice (remember, expressed in a language of primitives of space) in his space. A language of space primitives could be (or contain as a part) the emergent algebras. Ideally, such a language of primitives should be described by: A – a class of gates (operations), which represent the “map-making” relation, with an abstract scale parameter attached, maybe also with supplementary operations (like lambda abstraction?), B – a class of variables (names) which represent generic points of a space, and a small class of terms (words) expressed in terms of variables and gates from (A) (resembling to combinators in lambda calculus?). These are the “generators” of the space and they have the emergent algebras property, namely that as the scale goes to zero, uniformly with respect to the variables, the output converges to a new operation. C – a class of rewriting rules saying that some simple assemblies of generators of space have equivalent function, or saying that relations between those simple assemblies converge to relations of the space as the scale goes to zero.

The article on lambda epsilon calculus is a first for me in this field, I would be grateful for any comments and suggestions of improvements.