Could a different choice of evaluation order change the **terminating result** of the program; note that this says nothing about whether or not particular evaluation order terminates.

## constituents

## requirements

A set of rewrite rules is *confluent* if for any expression \(E_0\), should \(E_0 \to^{* } E_1\) and \(E_0 \to^{* } E_2\), then there exists some \(E_3\) such that \(E_1 \to^{*} E_3\) and \(E_2 \to^{ *} E_3\)

Why this instead of saying we will end up at one state after all evaluations? Suppose a particular system never terminates, we have to specify a particular confluent state because otherwise the notion of `all`

is bad.

## additional information

### one-step diamond property

if for all \(A\), \(A\to B\) and \(A \to C\) implies that there exists some \(D\) such that \(B \to D\) and \(C \to D\), this system exhibit a one-step diamond property.

If some system has one-step diamond property, then that system is confluent. This is a **sufficient but not necessary** property.

Proof: induction

go build a grid using the one step diamond property

### SKI exhibits one-step diamond property

We can’t naively apply one-step diamond property.

We have to first define a new relation \(\gg\) for SKI Calculus, which deals with the fact that \(Sxyz \to (xz) (yz) \to (xz’) (yz’)\) isn’t one step because expanding \(z\) before and after results in a different number steps.

we define \(X \gg Y\), if…

- \(X \to Y\) via a rewrite at the root node
- \(X = A B, Y = A’ B’\) and \(A \gg A’\), \(B \gg B’\)

we allow multiple rewrites if they are in *independent subtrees*