Is the term $(\lambda x.x)(y y)$ a normal form in call-by-value reduction strategy?

Question

I am learning λ-calculus and I have some confusion about it.

Is the term $(\lambda x.x)(y y)$ a normal form in call by value reduction strategy? (where $y$ is a free variable)

From the wikipedia, it says:

Call by value

Only the outermost redexes are reduced: a redex is reduced only when its right hand side has reduced to a value (variable or abstraction).

Here the term $(\lambda x.x)(y y)$ is a beta redex, but the argument $(y y)$ is not a value.

So the term $(\lambda x.x)(y y)$ is a normal form, because there is no further beta reduction possible.

Is my understanding correct?

Very thanks.

---

Sorry for updated the question, because I just realized that there may be 2 questions behind:

1. In λ-calculus, does the terminology "normal form" depend on the evaluation strategy? i.e. When we say a term is a normal form or not, is there any evaluation strategy behind it? For example, CBV ⊢ (λx.x)(yy) be a normal form and CBN ⊢ (λx.x)(yy) be not a normal form?

2. When we say "a λ-calculus with call-by-value", is it equivalent to say "λ_v-calculus"? I am reading Sabry and Felleisen's paper "Reasoning about Programs in Continuation-Passing Style". That paper mentioned λ_v-calculus and in p.8 it says (λx.x)(yy) has no βv-redex.

Answer 1

After some research, I think I can answer this question by myself now.

Short answer

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.

Long answer

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

1. You can reduce a $\beta $-redex inside a $\lambda $-abstraction.
2. You can reduce the operand $\beta $-redex first and then reduce the operator $\beta $-redex.
3. 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:

1. I think reduction strategy and evaluation strategy mean the same thing.
2. 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:

1. In Plotkin's paper, "value" does not mean "has no β-redexes", but "not a combination" (A term of form $(MN)$ is a combination).
2. 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?

Answer:

1. 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.

2. 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)$.

1. $ \to (λy.z)((λx.xx) (λx.xx))$, then loop
2. $\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)$.

1. $ \to (λx.y) ((λx.xx) (λx.xx))$, then loop
2. $\to y $

Reference

Call-by-name, call-by-value and the λ-calculus

Reasoning about programs in continuation-passing style