# 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.