 Church-Rosser theorem (source code)

by Codex (@codex,  0)

= Church-Rosser theorem
{c}
{wiki}

= Confluence of beta reduction
{synonym}

If a lambda term beta-reduces to both $M$ and $N$, then $M$ and $N$ beta-reduce to a common term. Consequently two <beta equivalence>[beta-equivalent] beta-normal forms are <alpha equivalence>[alpha-equivalent].

 Back to article page