How is runtime termination guarenteed?

[Kyle Blake]

I have been working on my own language that is very similar to Awelon for a Uni project, which is turning out to be an excellent way to solidify my understanding of the underlying concepts. However, something I have noticed is that there doesn't seem to be anything stopping e.g. a while loop from depending on a runtime value in such a way that it would never terminate. I was under the impression that your goals were fast-and-loose termination reasoning for compiling time, but non-termination being impossible at runtime. Possibly relevant is that my mental model has the AO program being a signal in itself, and so e.g. a number == a constant signal.

[David Barbour]

The AO and ABC languages do not guarantee termination. It is not difficult to write a divergent loop (e.g. `[dup inline] dup inline`). I've recently implemented a 7-word fixpoint function based on the Z-combinator `[swap dup bind composeLeft] bind dup apply`.  (That one tied my mind in knots for a week. :)

I do plan to perform termination analysis. Naturally, any such analysis will be partial: there will be some programs for which I cannot decide termination, and I'll just apply some limited computational effort towards such analysis. But termination analysis can improve over time, and meanwhile it also serves a useful purpose of regularly reminding developers that programs should terminate, and encouraging alternative models for long-running processes - e.g. incremental processes or continuous reactive behaviors. 

What "fast and loose reasoning" does is relax the burden of proof, e.g. for purpose of refactoring, rewriting, optimization, or partial evaluation. We don't need to prove termination. We're free to assume it, and any violation of the assumption is a bug. 

Anyhow, while AO/ABC don't guarantee termination, the RDP effects model does make it pretty easy to enforce termination because of how it tracks latencies. For example, I could provide a powerblock that is only good for a reactive latency of at most 3 seconds (i.e. such that it takes at most 3 seconds for bits twiddled at one location to wag values at another).  A problematic program will be halted pretty easily, and the same constraints can simplify static analysis.

Re: the AO program being a signal in itself, and so e.g. a number == a constant signal

This is the model I've been pursuing. There have been a few difficulties - e.g.  what are the spatial-temporal properties (location and latency) for a literal number? But I've managed to design around them. Program-as-a-signal works really well for a live programming context. Widgets, in a sense, can be expressed as directly manipulating code. I have an idea for an AO/RDP-based spreadsheet that seems pretty cool in my head, but it will be a while before I can implement it.

Best,

Dave

On Thu, Jan 23, 2014 at 10:30 PM, Kyle Blake <klkb...@gmail.com> wrote:

I have been working on my own language that is very similar to Awelon for a Uni project, which is turning out to be an excellent way to solidify my understanding of the underlying concepts. However, something I have noticed is that there doesn't seem to be anything stopping e.g. a while loop from depending on a runtime value in such a way that it would never terminate. I was under the impression that your goals were fast-and-loose termination reasoning for compiling time, but non-termination being impossible at runtime. Possibly relevant is that my mental model has the AO program being a signal in itself, and so e.g. a number == a constant signal.

--
You received this message because you are subscribed to the Google Groups "reactive-demand" group.
To unsubscribe from this group and stop receiving emails from it, send an email to reactive-dema...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

[Kyle Blake]

Hmm. I think I don't understand how the latency tracking is supposed to work. I was under the impression that latency was introduced manually by a "delay" word (or "sync"), and propagated statically, but this would make propagating across potentially non-terminating loops not much easier than deciding termination. A dynamic latency check on powerblock usage would be enough to detect finite loops that are too large (but not so large that they might as well be infinite, unless you inserted the check in each loop). While I'm asking about latencies, am I correct in thinking that the general purpose of latencies is to determine how much to shift the calculation back by in order to have the result arrive on time?

[David Barbour]

Yes, latency tracking works by modeling delays statically. I originally used a 'delay' word (1).  If I were to allow unlimited delay, then deciding delay would have the same problems as deciding termination. 

However, it is desirable to constrain latencies, especially in a reactive model. If my maximum allowed observable latency for a subprogram is, for example, one hundred milliseconds then I don't need to prove "terminates some day" but rather "terminates before it consumes one hundred milliseconds of latency". And while the latter isn't especially easy to prove, it is more amenable than the former to brute force proof techniques, discovery of refined inputs that would ensure the goal, and dynamic enforcement. 

Of course, none of this will help if you express the loop as having zero delay. So, don't do that for ad-hoc loops. :)

Regarding 'the purpose of latencies' - latencies were introduced primarily to simplify reasoning about behavior. In RDP, latencies allow me to ensure a 'duration coupling' property, which requires synchronizing outputs - e.g. of different effects and observations - so they correspond to input stimuli. Latencies can also model synchronizing of effects, and can interact in very nice ways with a scheduler. 

(1) I now use a logical clock (or a set thereof) to model delays. Each clock has a hidden time. We can delay a signal to match the time on a clock, delay a clock to match a signal, or create a new clock whose logical time is greater by some rational number. The resulting model has nice idempotence properties compared to direct 'delay' of a signal, and (critically) interacts well with literal numbers and text.  But the differences aren't especially germane to the current discussion.

--