Home > Uncategorized > Rules of lambda epsilon calculus

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

1. May 11, 2012 at 5:10 pm | #1
2. May 15, 2012 at 2:09 pm | #2
Sauropod Vertebra Picture of the Week #AcademicSpring

SV-POW! ... All sauropod vertebrae, except when we're talking about Open Access

Science to Grok

computing with space

isomorphismes

computing with space

Retraction Watch

Tracking retractions as a window into the scientific process

Shtetl-Optimized

computing with space

Not Even Wrong

computing with space

Theoretical Atlas

He had bought a large map representing the sea, / Without the least vestige of land: / And the crew were much pleased when they found it to be / A map they could all understand.

Gödel's Lost Letter and P=NP

a personal view of the theory of computation

Gowers's Weblog

Mathematics related discussions

Research and Lecture notes

by Fabrice Baudoin

Calculus VII

being boring

The "Putnam Program"

Language & Brains, Machines & Minds

What's new

Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Tao