One thing which is nice though, is how to prove Turing completeness. First, there's a somewhat trivial argument that the Dot notation and evaluation is Turing complete, since S and K are trivially expressible, and eager evaluation will, by the confluency theorem, normalize terminating computations.
But, I wonder, is that good enough? I am not sure I actually proved Turing completeness that manner since I only showed it then for terminating terms. It would be better to show that it is possible to restate S and K such, that the eager reduction of those will correspond to the lazy evaluation of the original symbols.
I.e., K can be expressed as [K x y] = [@ x] and S can be expressed as [S x y z] = [@ x z .] [@ y z]. It should be easy to restate them lazily, since it is well known how to defer evaluation in an eager language by abstracting terms and suspending evaluation until a dummy argument is supplied. So, I am looking at S' and K' which would do that, or possibly, by restating the evaluation of application to a lazy form.
Below, my funny thoughts using Blogger as a scratch pad. Don't read if you don't like hazy thoughts.
So, an initial thought, since lazy evaluation reduces the head of an expression, which should be equivalent to reducing the last term in the Dot notation, K' should become [K' x y d] = [@ x d], but what should S' be?
Tinkering further, A for lazy apply should become, [A x y d] = [@ . y d] [@ x d]? Hmm, shallow encoding doesn't work...? Tinkering along, see no reason shallowness shouldn't work, apply should do it... Maybe need a defer operator and express it in SKI directly? [D f d] = [@ f]?
Lemme see, I think I nailed it. First, I need to show that SKI can be translated to a deferred term such that when that term is applied to a dummy argument, we get the original term back. Second, I'll need to show that that term eager reduced is equivalent to lazy reducing the original term.
So, let A x y d = (let x' = (x d) in x' (y d)), making the evaluation order explicit, and let D f d = f. Then let the translation function T be defined as: T(K) = D K, T(S) = D S, and T(x y) is A (T(x)) (T(y)). Then, T(E) d = E, since:
- T(K) d = D K d = K
- T(S) d = D S d = S
- T(x y) d = A (T(x)) (T(y)) d = (let x' = (T(x) d) in x' (T(y) d)) = (T(x) d) (T(y) d), thus by induction is (x y).