# Must the evaluation strategy for a language be specified in order to apply the Church-Rosser Theorem?

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.