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 *) for any fresh variable ,

(R1) (Reidemeister one) if then

(R2) (Reidemeister two) if then

(ext1) (extensionality one) if then

(ext2) (extensionality two) if then

These are taken together with usual substitution and -conversion.

The relation between the operations from calculus and emergent algebras is illustrated in the next figure.

### Like this:

Like Loading...

*Related*

## 2 thoughts on “Rules of lambda epsilon calculus”