![cover image](https://wikiwandv2-19431.kxcdn.com/_next/image?url=https://upload.wikimedia.org/wikipedia/commons/thumb/d/db/Confluence.svg/640px-Confluence.svg.png&w=640&q=50)
Church–Rosser theorem
Theorem in theoretical computer science / From Wikipedia, the free encyclopedia
Dear Wikiwand AI, let's keep it short by simply answering these key questions:
Can you list the top facts and stats about Church–Rosser theorem?
Summarize this article for a 10 year old
In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result.
![Thumb image](http://upload.wikimedia.org/wikipedia/commons/thumb/d/db/Confluence.svg/320px-Confluence.svg.png)
More precisely, if there are two distinct reductions or sequences of reductions that can be applied to the same term, then there exists a term that is reachable from both results, by applying (possibly empty) sequences of additional reductions.[1] The theorem was proved in 1936 by Alonzo Church and J. Barkley Rosser, after whom it is named.
The theorem is symbolized by the adjacent diagram: If term a can be reduced to both b and c, then there must be a further term d (possibly equal to either b or c) to which both b and c can be reduced. Viewing the lambda calculus as an abstract rewriting system, the Church–Rosser theorem states that the reduction rules of the lambda calculus are confluent. As a consequence of the theorem, a term in the lambda calculus has at most one normal form, justifying reference to "the normal form" of a given normalizable term.