Weakening Cycles So That Turing Can Halt
I really like the &quot;delay&quot; datatype as a way to implement general recursion (i.e. Turing-completeness) in a non-general&#x2F;non-Turing-complete system like Coq or Agda.<p>We can think of &#x27;Delay&lt;T&gt;&#x27; as being a bit like &#x27;List&lt;T&gt;&#x27;. If we follow Lisp&#x27;s encoding, there are two forms of list: the empty list &#x27;Nil&#x27;, which doesn&#x27;t &quot;contain&quot; anything; and the pair &#x27;Cons(x, y)&#x27; which contains a value &#x27;x&#x27; (the &quot;head&quot; or &quot;car&quot; of the list) and another list &#x27;y&#x27; (the &quot;tail&quot; or &quot;cdr&quot;, which might be &#x27;Nil&#x27;).<p>&#x27;Delay&#x27; is the other way around: it is either &#x27;Now(x)&#x27;, which contains the value &#x27;x&#x27;, or it is &#x27;Later(y)&#x27; which contains another delay &#x27;y&#x27; (which might be a &#x27;Now&#x27;). We can imagine &#x27;Delay&lt;T&gt;&#x27; a bit like a list containing a single &#x27;T&#x27; value at the end, preceded by an arbitrary amount of NULL elements. I&#x27;ve gone into a bit more depth on such constructions (AKA &quot;initial algebras&quot;) in a blog post <a href="http:&#x2F;&#x2F;chriswarbo.net&#x2F;blog&#x2F;2014-12-04-Nat_like_types.html" rel="nofollow">http:&#x2F;&#x2F;chriswarbo.net&#x2F;blog&#x2F;2014-12-04-Nat_like_types.html</a><p>This gets interesting if our language allows <i>co-termination</i> (like Agda, Coq, Haskell, etc.). This is where we&#x27;re allowed to recurse &#x27;inside&#x27; our return value. For example, the following function doesn&#x27;t terminate, since it will always call itself recursively; yet it does co-terminate, since the recursion is happening &quot;inside&quot; the &#x27;Cons&#x27;. We don&#x27;t know what the full result will be, but at every stage we definitely know what the next part will be (a &#x27;Cons&#x27; list). We can reach any finite &quot;depth&quot; of the result within a finite amount of time. This is also known as being &quot;productive&quot;:<p><pre><code>    function countUpFrom(x) {
      return new Cons(x, countUpFrom(x+1));
    }
</code></pre>
The following function doesn&#x27;t co-terminate (whether it always terminates is currently unknown), since (in the non-1 case) we don&#x27;t &#x27;narrow down&#x27; the return value before recursing. As far as we know, this could keep &quot;passing the buck&quot; forever, and we&#x27;d never get any closer to knowing what any part of the result looks like:<p><pre><code>    function collatz(x) {
      return (x == 1)? 1
                     : collatz(even(x)? x &#x2F; 2
                                      : 3 * x + 1);
    }
</code></pre>
Implementing co-termination requires that the &quot;contents&quot; of a datastructure are calculated on-demand rather than straight away (AKA &#x27;lazily&#x27;). We can actually do this in any language with first-class functions by creating (and subsequently forcing) &quot;thunks&quot;, although it gets quite verbose, e.g.<p><pre><code>    function countUpFrom(x) {
      return new Cons(x, function() { return countUpFrom(x+1); });
    }
</code></pre>
I wrote a blog post which uses this to generate Fibonacci numbers in PHP: <a href="http:&#x2F;&#x2F;chriswarbo.net&#x2F;blog&#x2F;2014-07-23-fib.html" rel="nofollow">http:&#x2F;&#x2F;chriswarbo.net&#x2F;blog&#x2F;2014-07-23-fib.html</a><p>We can use co-termination to implement a Turing machine, or any other generally-recursive system, by simply making a list of each &quot;step&quot;:<p><pre><code>    function turingMachineList(tm) {
      return Cons(tm,
                  halted(tm)? Nil
                            : turingMachineList(step(tm)));
    }
</code></pre>
This will produce a list of each machine state, which might stop (if the machine reaches a halted state) or go on forever. Likewise we can implement a list of Collatz values:<p><pre><code>    function collatzList(x) {
      return Cons(x,
                  (x == 1)? Nil
                          : collatzList(even(x)? x &#x2F; 2
                                               : x * 3 + 1));
    }
</code></pre>
If we only care about the &quot;result&quot; then we can use &#x27;Delay&#x27; instead of &#x27;List&#x27;:<p><pre><code>    function turingMachineDelay(tm) {
      return halted(tm)? Now(tm)
                       : Later(turingMachineDelay(step(tm)));
    }

    function collatDelay(x) {
      return (x == 1)? Now(1)
                     : Later(collatzList(even(x)? x &#x2F; 2
                                                : x * 3 + 1));
    }
</code></pre>
These will return a value like &#x27;Later(Later(Later(...)))&#x27; which will either keep nesting forever, or (if the calculation has an answer) will eventually contain &#x27;Now(answer)&#x27;.<p>&#x27;Delay&#x27; is nice since we can write programs in pretty much the same way as normal. The only changes are mechanical and obvious:<p>- If a recursive call isn&#x27;t &quot;inside&quot; the return value, we wrap it in &#x27;Later(...)&#x27; so it is; and wrap any corresponding base-cases in &#x27;Now(...)&#x27;.<p>- If we need to perform some calculation on the result of a &#x27;Delay&#x27; (i.e. the value in its &#x27;Now&#x27;), we can&#x27;t do so directly, since there might not be a result (it could be &#x27;Later(Later(...))&#x27; forever); and even if there is, we don&#x27;t know how many &#x27;Later&#x27; wrappers to dig through. Instead, we use these values <i>indirectly</i>, by <i>mapping</i> our calculation over the &#x27;Delay&#x27; value. This isn&#x27;t hard: it&#x27;s exactly the same as mapping over the elements of a list, or over an optional value, etc. Here&#x27;s what &#x27;map&#x27; looks like for &#x27;Delay&#x27;:<p><pre><code>    function mapDelay(f, x) {
      return case x {
          Now(y):   Now(f(y));
        Later(y): Later(mapDelay(f, y));
      };
    }
</code></pre>
We can run such programs in two ways:<p>- We can remove (up to) some finite number of &#x27;Later&#x27; wrappers, which is equivalent to running with a timeout. We can always do this inside the total (terminating&#x2F;co-terminating) language. We might still end up with a &#x27;Later(...)&#x27;, unless we can prove that the computation will always finish before our timeout (i.e. if we have a termination proof).<p>- We can use an external program (in a Turing-complete language) as a clock to &#x27;tick&#x27; through each step; essentially playing the role of OS or VM (similar to using a trampoline for recursion, in languages which don&#x27;t eliminate tail-calls). In this sense, &#x27;Delay&#x27; is like a language-enforced version of cooperative multitasking, since we must always eventually yield, at which point the OS can pick another delayed value to tick. The ticks are also a convenient place for the user to interrupt&#x2F;cancel a program.<p>Of course, knowing that the next tick will be occur within a finite time doesn&#x27;t guarantee that it will be happen before the heat-death of the universe!<p>Note that we can also use co-termination to build datatypes which have <i>no</i> base-case, and hence every value must be infinite. This would be pretty useless for &#x27;Delay&#x27; (since there is only one infinite value, namely &#x27;Later(Later(...))&#x27; forever). The always-infinite equivalent of lists are called &quot;streams&quot;, and are defined as having a &#x27;Cons&#x27; form but no &#x27;Nil&#x27; form.<p>From the OS&#x2F;VM perspective above, this lets us write programs which are guaranteed to run forever (e.g. servers which never crash), although they may run out of memory, and responses might take a while (bounded by the busy beaver number for the server&#x27;s code size + the request size). The classic example is to represent input as an infinite stream, e.g. &#x27;Stream&lt;HTTPRequest&gt;&#x27;, have a function for constructing a response &#x27;respond : HTTPRequest -&gt; HTTPResponse&#x27;, and construct a server via &#x27;streamMap(respond, input) : Stream&lt;HTTPResponse&gt;&#x27;. If we want a stateful server we can include the new state with our reponse and have the server plumb it through:<p><pre><code>    respond : (State, HTTPRequest) -&gt; (State, HTTPResponse)

    server : (State, Stream&lt;HTTPRequest&gt;) -&gt; Stream&lt;HTTPResponse&gt;

    function server(currentState, stream) {
      return case stream {
        StreamCons(request, rest): case respond(currentState, request) {
          (nextState, response): StreamCons(response,
                                            server(nextState, rest));
        };
      };
    }</code></pre>