Put and . Then . Unlike the Curry fixed-point combinator, every finite reduct retains a closed subterm . Contracting this subterm recreates one; every other generated redex substitutes a variable and preserves it. The Church-Rosser theorem therefore proves .
Articles by others on the same topic
There are currently no matching articles.