After some research, I think I can answer this question by myself now.
Wikipedia is correct, that is
If the $\lambda $-calculus uses call by value reduction strategy, the term $(\lambda x.x)(y y)$ is a normal form.
Standard $\lambda $-calculus does not distinguish reduction strategies. It only gives you some Reduction Rules (e.g. $\beta $-rule). You searching for a β-redex in a given term, as long as you find a β-redex, you can reduce one step.
This means that
- You can reduce a $\beta $-redex inside a $\lambda $-abstraction.
- You can reduce the operand $\beta $-redex first and then reduce the operator $\beta $-redex.
- At any step, you can use either call-by-value or call-by-name reduction strategy.
Church–Rosser Theorem tells us that the outcome of $\lambda $-calculus (if it exists) is independent of the order in which the calculations are executed.
The benefit of Church–Rosser Theorem is that we can define an Equational Theory at top of the Reduction Rules.
Note that in the description above, I used extremely imprecise terminology, i.e. reduction strategy. Now i will fix this impreciseness:
- I think reduction strategy and evaluation strategy mean the same thing.
- For now, we cannot use the term "evaluation" because we have not yet defined an Evaluation Theory.
Unfortunately, there is very little literature describe how to define the Evaluation Theory for standard $\lambda $-calculus. The reason may be that:
In general, to define the Evaluation Theory, we need an abstract machine, but the use of an abstract machine means a fixed evaluation strategy, but standard $\lambda $-calculus does not depend on the evaluation strategy!
Therefore standard $\lambda $-calculus has no corresponding Evaluation Theory is logical.
OK, so far so good.
However the standard $\lambda $-calculus is not suitable to reason about programming languages. For example, Scheme/SML use call-by-value evaluation strategy, Haskell use call-by-name (or more precisely call-by-need) evaluation strategy.
To reason about these programming languages, a new $\lambda $-calculus needs to be devised. For example, Plotkin's call-by-value $\lambda $-calculus ($\lambda_v$ for short).
As standard $\lambda $-calculus, we now need to devise Reduction Rules, Equational theory and Evaluation theory for $\lambda_v$. I won't repeat Plotkin's formula here, but give two key points:
- In Plotkin's paper, "value" does not mean "has no β-redexes", but "not a combination" (A term of form $(MN)$ is a combination).
- Equational theory must satisfy Church–Rosser Theorem (for $\lambda_v$ version).
Back to the original question:
Is the term $(\lambda x.x)(y y)$ a normal form in call by value reduction strategy?
The question involved "normal form" and "reduction strategy" (which is another name of evaluation strategy). It doesn't make sense, because one refers to an Equational Theory and the other refers to an Evaluation Theory.
The question involved "call by value", we can fix this ill-question by assuming the calculus to be $\lambda_v$ and since the question also involved "normal form" and $(\lambda x.x)(y y)$ is not a closed term, we use Equational theory of $\lambda_v$.
The answer is:
$(\lambda x.x)(y y)$ has been a normal form, because $(y y)$ is not a value but a combination.
$(\lambda x.M)N = [N/x]M$ (if $N$ is a value) ($\beta$ -rule)
You may argue that why $(y y)$ is not a value?
Can I define my own $\lambda_v$-calculus and let a normal form (e.g. $(y y)$) a value?
The answer is no.
For example, suppose that a normal form can be a value, then there are two ways to normal the term $(λx.(λy.z) (x (λx.xx))) (λx.xx)$.
- $ \to (λy.z)((λx.xx) (λx.xx))$, then loop
- $\to (λx.z)(λx.xx) \to z$
This make Church-Rosser theorem fail.
Similarly, adding $\eta$ rule also makes Church-Rosser theorem fail.
For example, suppose that we add $\eta$ rule, then there are two ways to normal the term $ (λx.y) (λx.((λx.xx) (λx.xx))x)$.
- $ \to (λx.y) ((λx.xx) (λx.xx))$, then loop
- $\to y $
Call-by-name, call-by-value and the λ-calculus
Reasoning about programs in continuation-passing style