ch:temporal-types: ch:temporal-types

A running average implemented with a retained prefix is causal but may leak space. The equation $y_n=x_{n+1}$ is productive as a whole mathematical stream but noncausal as an online transducer. The first violates the space discipline; the second violates present-output dependence.

After the tick, RaTT-Var cannot reach $x$, because its suffix contains $✓$; consequently the abstraction premise fails. If $x$ has stable type, RaTT-Progress reintroduces its value after the tick, and the abstraction closes over that transported stable value rather than an old-heap closure.

The fixed-point variable $m:◯A$ and the delayed input tail both cross the same RaTT-Delay boundary. Inside its ticked premise, RaTT-Adv opens both. Advancing only $m$ leaves no stream argument for the recursive call; advancing the tail earlier has no tick and is ill typed.

Use a stable list accumulator and cons the current input before delaying the recursive call. Old temporal heaps remain unreachable, so proposition 55.1 holds. The list itself is a stable value reachable from the new state; its deliberate growth is not an implicit heap leak.

Productivity assumes one closed boxed output stream and yields arbitrarily many typed heads. Causality assumes a boxed function from input streams to output streams plus a typed current input, and maintains a decreasing transducer approximation. A closed stream can be productive even if a purported online implementation needed future external input, so the first theorem alone does not establish the dependency condition of the second.

Producing $y_0$ requires both $x_0$ and the head of the delayed input tail. The latter has type $◯\mathsf{Str}A$. At the present context there is no $✓$, so RaTT-Adv’s context-formation premise fails. Only after emitting the present head may the machine cross the tick.

Map transforms each present head, sampling chooses which present cells to forward, and running sum transports only its stable accumulator. All tail calls occur inside one delay and both recursive code and tails advance after its tick. With identity map and no dropped cells, $2,11,5$ yields $2,13,18$.

At index $k+1$, delay allocates the premise term in the later heap and records it in $\mathcal{V}[[◯A]]$. Heap rotation makes that location part of the now heap and lowers the index to $k$. Advance retrieves the term, whose stored semantic premise is membership in $\mathcal{T}[[A]]$ at that successor world.

Both programs discard the old now heap and retain one delayed tail. The natural accumulator has constant representation. In the stated stable-list extension, the list accumulator adds one cons cell per input and remains reachable as stable state, so application data grows even though no old temporal heap is retained.