Silly Kotcha

I was writing some informal stuff on the Dot notation again, just to finally settle it and prove some invariant. It's pretty light-weight what I did, no real math as of yet, there doesn't seem a point in formalizing a lot of the arguments to the bone since it is trivial enough as it is.

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

Next step... This is a bit fuzzy, it would be better to write it down in normal arrow notation, but whatever. The only relevant case is the A definition. Since in the A definition the let variable, which is the translation of the function, is reduced first, and later applied to a reduced argument...? Hmm, it breaks here? Wrong A/translation? The argument should be reduced whenever it comes in head position, not earlier. Ah well, tinker away tomorrow again. Guess I need both a suspend/defer and an evaluate combinator.


Hmmm....