Rewrite systems are a general approach for modeling discrete computations and logics. A set of rewrite rules are applied to a term (or graph, or string, etc.) repeatedly until no further rewrites are possible. Rewriting is distinct from functional programming in that the `fixpoint` reduction (repeated application) is implicit, whereas functional expression of the same model would require explicit recursion. Modeling functional programming in a term rewrite system would involve expressing `apply f x` as a term to be reduced, which allows developers to control the number of applications.
I am interested in term rewrite systems (TRS) as a potential discrete state model for reactive demand programming (RDP). Term rewriting is a generalization of state transition systems, which I have already explored as useful state models [1][2]. I mean `animated` and `reactive` in the same sense (and for similar reasons) that I desire them for animated, reactive state transition.
- reactive: the set of rewrite rules may change over time based on influence from the external environment. Rewriting is logically applied at every instant, thus changes in rewrite rules apply immediately. State effectively `reacts` to conditions.
- animated: it is possible to model time-varying state with a fixed set of rewrite rules, making it easy to `control` or animate external systems over time even when external conditions are stable. A simple example would be incrementing a number once a second.
Term rewriting is very expressive compared to state transition, i.e. there is a huge difference in what you can express with a finite set of rewrite rules vs. a finite set of transition rules. In context of RDP, where there are at most a finite set of rules at any given instant, this difference in expressiveness corresponds very directly to a difference in computational power and flexibility. However, such power has a cost: rewriting can easily diverge even with a finite number of rules (whereas state transition can only cycle), and it is much more difficult to control computation costs.
Like state transition, term rewriting may be indeterministic. I will assume some (possibly arbitrary or heuristic, based on structure) strict ordering can be applied to the rewrite rules because determinism is a property I desire for RDP.
A basic reactive term rewriting` state model (without animation) would have the following elements:
- One term register carries state as a complex term.
- A capability to influence a term register by imposing a rewrite rules in the demand value:
(s Rules) ~> (s ()), for some discrete-varying signal type `s`. At any given instant, a finite number of rewrite rules are influencing the term register. - A capability to read the term register:
(s ()) ~> (s Term). - A discovery mechanism, allowing developers to pretend term registers are eternal (and orthogonally persistent). This is necessary since there is nothing new in RDP. Also, ability to reset the register.
Whenever observed, the term is always stable. Rewrite rules may change from one instant to the next, and the term is instantaneously reduced to a new stable state. Change in the term only occurs as a consequence of change in the rewrite rules.
I was extremely unsatisfied with this basic Reactive Term Rewriting model. First, there are the unpredictable costs and divergence concerns. Second, it seems too difficult to model useful behaviors, such as an integer that increments periodically – i.e. you cannot ever express a rule of the form `X => X+1` since that would diverge, but expressing rules of the form (3 => 4) (and switching to a new rule when conditions change) does not leverage the full extent of term rewriting.
Animated reactive state transition added a couple extra registers to expire and change state, allowing state to change over time even when the influence rules are constant. Naturally, I considered animating reactive state transition as part of that. A simple approach would be to use the same expiration technique: a rewrite rule may have two stages, allowing a further rewrite after some time has passed if no other rule applied in between. But that still has the problems with divergence, unpredictable costs, etc.
More recently, I’ve found a model that seems more promising for my goals – based on modeling costs directly. In this model:
- Each term register is accompanied by an `time debt` register, whose range is >= 0.0.
- Each rewrite rule is labeled with two positive, real-valued attributes: maximum time debt, and time cost.
- When a rule is applied, the time cost is added to the time debt register.
- A rule may not be applied unless the time debt starts less than or equal to maximum specified for that rule.
- Rules are always applied favoring those of the highest `maximum time debt`. This ensures that rule selection is independent of the initial time debt, and thus makes the model much easier to predict. (One might call this the `path of least resistance` rule.)
- Time debt reduces toward 0.0 at a constant, continuous rate of 1.0 per second.
Effectively, developers model how long each rewrite rule takes (logically). Since debt is allowed to build, it is possible to model bursty or cascading computations. Animated behavior is easy. Consider a term rewrite model with just one rule and an enumerable term. While the rule is {rule:X => X+1, time-cost:1.0, time-debt-max:0.0}, the term would simply increment once per second. Even though the rewrite rule is active at every instant, the time debt is most of the time too high for the rule to apply. Effectively, divergence becomes animation.
There is no absolute cap for time debt, but at any given instant the maximum debt the model can reach is a simple function of the rewrite rules. Since developers can easily cap the amount of computation that occurs in any given period, this animated reactive term rewriting model is suitable for real-time applications.
Awelon Blue 
You imply as much, but I’ll just emphasize that, rather than seeing it as a controlled divergence, you can also view it as modifying the antecedent to include your time metrics and meta-rules for matching against the model of time in your term register. So, by explicitly modeling time, the system is convergent.
The main thing that is formally missing is a sort of self-awareness of rewriting. e.g. that rewriting takes time.
True. I can formally model the rewriting by wrapping each term with information about current time and time-debt. Reactive rules are modeled by labeling every rewrite rule with validity and expiration data. Animated rules are modeled by time-debt within each instant and time between instants. Convergence is by computation `up to` the current instant.
Real-time Maude (built using Maude reflection) has some similar properties.
This seems much more elegant than RST and Animated RST! In fact, were I programming for RDP right now, I’d be tempted to shove all my discrete state needs into this state model and ignore those others. What would I lose by doing that?
I’m pretty sure there’s something, but you’ll probably be able to come up with a better answer to this than I can.
Possible reasons to favor RST: bounded memory, bounded processing, stable animation behavior (explicit intermediate states; timeout+goto less history-dependent than time-debt), and easy to reason about all reachable and observable states. Also, the state transition rules are very simple compared to possible rewrite rules. All this comes at a rather high cost to expression and power, of course.
Animated reactive term rewriting is a very big hammer for discrete-state and animation problems, capable of smashing pegs of many shapes into square holes. Unless the task involves mission-critical or hard-real-time systems, or perhaps for developing intermediate frameworks, it is likely not be worth importing and learning a second animated state and animation model. I expect many people would feel exactly as you do.