1
$\begingroup$

The Church-Rosser Theorem [0] states that the Lambda Calculus (LC) is confluent: between a source expression S and target expression T, the latter in normal form, for any given P, a sequence of permissible reductions that begins with S, there is some subsequent sequence of reductions Q (possibly the empty sequence) that can be applied after P to arrive at T. Thus, for all P, there exists Q such that Q(P(S)) = T.

Evaluation strategies [1], in this context, are rules for applying reductions to LC terms. These rules can include the order in which reduction are applied. Certain terms will diverge under strict evaluation strategies, that under lazy evaluation will successfully reach a normal form. For example, consider a constant C, and the Omega (M) and K combinators, M = ,\y.(y y)(,\y.(y y)), and K = ,\a.,\b.a. Under lazy evaluation, KMC = C - the K combinator discards M without evaluation. Under strict evaluation, KMC diverges because M diverges (in keeping with the definition of a strict function [2]).

How does this relate to the Church-Rosser Theorem, and the confluence property of LC? Is LC+Strict Evaluation not confluent? Are proofs which are dependent on the C-R Theorem sensitive to the evaluation strategy of the language to which they refer?

This is related to my question elsewhere [3] about the sensitivity of the computability classification of languages to their evaluation strategies.

[0] https://en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem

[1] https://en.wikipedia.org/wiki/Evaluation_strategy

[2] https://en.wikipedia.org/wiki/Strict_function

[3] Is there a hierarchy of computational expressivity that is sensitive to evaluation strategies?

$\endgroup$

1 Answer 1

2
$\begingroup$

The Church-Rosser theorem gives you the following guarantees:

  • A term has at most one normal form. That is, there aren't different normal forms depending on your choice of evaluation strategy.
  • If a term has a normal form, then no matter what evaluation strategy you use, the result of that evaluation strategy will be a term that can be further reduced (possibly in zero steps) to that normal form.

It does not guarantee that a particular evaluation strategy will find the normal form if it exists. But it does guarantee that your evaluation strategy won't transport you to a dead end from which the normal form can't be found by any strategy.

$\endgroup$
1
  • 1
    $\begingroup$ Thank you. I think the key is that C-R is defined with respect to particular reduction rules, i.e. "beta reduction is C-R" or "beta-eta reduction is C-R", and the definition of these rules leaves evaluation strategy unspecified. Thus, the existence of any normalizing reduction order is sufficient for confluence. However, a reduction rule which encoded a particular evaluation strategy may exclude one branch of the C-R diamond, and so not satisfy the prerequisites for possessing the diamond property. $\endgroup$
    – jpt4
    Aug 19, 2022 at 2:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.