2

A simplistic method of creating effects in Lambda calculus is by adding constants: functions that create required effects. For example: we can add a rnd function which represents a random Church numeral, where for every j belonging to every natural number the following reduction rule, where Nj is the church numeral relating to j:

                   rnd -> Nj.

How would the presence of such an effect impact reduction strategies (normal order and lazy evaluation) and with confluence.

1 Answers1

1

Notation. $N_j$ is the Church numeral for the natural number $j$, i.e. $N_j = \lambda f. \lambda x. \underbrace{f (f ( \cdots (f}_{j \text{ times}}x) \cdots ))$.

Yes, adding a side effect such as $$ \mathsf{rnd} \to N_j \quad \text{for every } j \in \mathbb{N} $$ to the $\lambda$-calculus impacts on reduction strategies and confluence.

First, the resulting calculus is not confluent because, given $i \neq j \in \mathbb{N}$, $$ N_i \leftarrow \mathsf{rnd} \to N_j $$ where $N_i$ and $N_j$ are distinct normal forms and hence do not have a common term to reduce to. So, not only the calculus is not confluent, but it is even false that every term has at most one normal form.

Moreover, with such a side effect it is not even true that lazy evaluation produces the same results as normal order (this holds, instead, in the pure case without side effects). Indeed, consider the term

$$\tag{1} (\lambda x. xx) \, \mathsf{rnd} $$

According to normal order, the argument $\mathsf{rnd}$ is passed to the function $\lambda x.xx$ without being evaluated, so \begin{align} (\lambda x. xx) \, \mathsf{rnd} &\to_\beta \mathsf{rnd} \, \mathsf{rnd} \\ &\to N_1 \, \mathsf{rnd} \\ &= (\lambda f. \lambda x. fx) \, \mathsf{rnd} \\ &\to_\beta \lambda x. \mathsf{rnd} \, x \\ &\to \lambda x. N_0 x \\ &\to_\beta \lambda x. \lambda y .y \end{align}

According to lazy evaluation, the argument $\mathsf{rnd}$ is first evaluated and then passed to the function $\lambda x.xx$, so \begin{align} (\lambda x. xx) \, \mathsf{rnd} &\to_\beta (\lambda x. x \, x) N_0 \\ &\to (\lambda x. N_0 \,x) N_0 \\ &= (\lambda x.(\lambda f. \lambda y. y)x)N_0 \\ &\to_\beta (\lambda x. \lambda y. y) N_0 \\ &\to_\beta \lambda y .y \end{align}

Therefore, term $(1)$ may reduce to two different results (i.e. normal forms) depending on whether the evaluation is normal order or lazy.

Taroccoesbrocco
  • 16,964