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.

About these ads

2 thoughts on “Rules of lambda epsilon calculus”

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s