This has nothing to do with typed vs. untyped lambda calculus. If you want to write a type signature for emulate, it would be State⊗Integer → State⊗Integer. In general, typed lambda calculus is

**less** expressive than untyped lambda calculus, since the latter can obviously express any well-typed expression. In this case, the typedness of the lambda calculus you're using has nothing to do with this.

No values are changing at all. He's expressing an algorithm by recursion. At cycle zero, the machine is in a known initial state. To this we apply the emulation operation which maps the old state to a new state and increments the number of cycles. If you wanted to expand this out, you'd have:

emulate(emulate(emulate(...emulate(initial_state, 0))...)))

alternatively, in a language like C, you'd have:

cycle_count = 0;

state = initial_state;

while(1) state = emulate(state, &cycle_count)); // emulate increments cycle_count

These are completely equivalent computations. In both cases, there's a serial data dependency: you can't compute the next state until you know the current state. Expressing this in lambda calculus or a purely functional style does not in any way remove this fundamental computational property. It would be like claiming that Fermat's last theorem is true in a base-12 number system but not in base-10: it's a mathematical property that's completely independent of a particular representation.

If you claim to have a faster-than-serial way to solve this emulation problem, congratulations, you've solved the halting problem and disproved one of the most fundamental theorems in computer science.

Quad, I respect you for your ability to find interesting info. I'm not sure if you're trolling or just confused, but you need to give this up.