Math and science::Theory of Computation::Lambda calculus

Confluence

Let $M$ be a lambda term. If $M ↠_{β} N_{1}$ and $M ↠_{β} N_{2}$ for some lambda terms $N_{1}$ and $N_{2}$ , then there exists [...] such that [...].

Confluence is also called the Church-Rosser theorem.

There are three corollaries of the confluence theorem listed on the back side. Can you remember them?

18.08.2021