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

Hmmm....

## No comments:

## Post a Comment