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
Ix
Kxy
Sxyz
