-
Notifications
You must be signed in to change notification settings - Fork 61
Rewriting Strategies
NOTE: this guide is outdated
Rewriting strategies provide a way to restrict the execution of a rewrite system to particular paths. There are several possible approaches implemented in various systems, more notably ELAN, Maude, and Stratego.
The approach proposed for K is different in the sense that it encodes the rewriting strategies entirely in the rewriting system itself. K's configuration abstraction mechanism makes this both possible and practical. We believe this approach is powerful enough to express very various uses of a rewrite system, from execution, including symbolic execution, to search, to debugging.
So, for a very simple program, the configuration might look like this at the start of the execution:
<t>
<k> a + b </k>
<env> a -> 1, b-> 2 </env>
</t>
Let's assume our start rewrite system has the following rules:
rule heat1: A + B => A ~> [] + B when !isResult(A)
rule heat2: A + B => B -> A + [] when !isResult(B)
rule cool1: A ~> [] + B => A + B when isResult(A)
rule cool1: B ~> A + [] => A + B when isResult(B)
rule eval: A + B => A +Int B when isResult(A) /\ isResult(B)
The way this semantics is currently is executed by K is to simply execute any rule that could possibly apply in any order repeatedly, or, for optimization, hardwire (in Java) that certain rules must apply before others (e.g., all heating before the evaluation rule followed by all the cooling rule). This makes the system hard to change when we want a slightly different behavior, or want to customize the current behavior.
The core idea of the proposal approach is to implement the rewrite strategy directly in K, and make it behave just like any other K semantic. The rewrite strategy for a particular program lives in a specially-designated top-level cell called <s>, which is added the the regular program configuration.
In the proposal approach, this program above starts with the following configuration:
<t>
<k> a + b </k>
<env> a -> 1, b-> 2 </env>
<s> ((heat1 | heat2)* ; eval ; (cool1 | cool2)*)* (#start) <s>
</t>
#start is simply the initial configuration given above (a reference to itself, if you like). No point in describe in words what the other operators above do as their syntax and semantics is also given in K. I'm giving here my view for execution strategies but others can devise their completely different approaches.
// The following sorts and functions are hardwired (everything else is configurable in K):
syntax Rule
syntax Term ::= ... a disjunction of ground configurations, or a symbolic term ...
syntax Term ::= "#execute" "(" Rule "," Term ")" [hooked to executing the rule on the state]
// From here on, everything is simply one possible strategy semantics. Users can choose their own.
// My strategy semantics has two main sorts: Value and Strategy
syntax Strategy // which is essentially a function from a State to a set of States
syntax Value ::= Term | App
syntax App ::= Strategy "(" Term ")"
syntax Strategy ::= Rule
syntax Strategy ::= Strategy "|" Strategy
syntax Strategy ::= Strategy "*"
syntax Strategy ::= Strategy ";" Strategy
syntax Value ::= Value "|" Value
rule <s> (A | B)(T) => A(T) | B(T) </s>
rule <s> A | B => A ~> [] | B </s> when !isTerm(A)
rule <s> A | B => B </s> when !isTerm(B) /\ isFalse(A)
rule <s> A | B => A </s> when isTerm(A) /\ !isFalse(A)
rule <s> A* => A | A* </s>
rule <s> (A ; B)(T) => B(first(A(T))) </s>
syntax Term ::= "first" "(" Term ")" [ hooked to selecting just one of the results ]
rule <s> first(A) => A ~> first([]) </s> when !isTerm(A)
rule <s> A(B(R)) => B(R) ~> A([]) </s>
rule <s> T ~> B(T) </s> when isTerm(T)
rule <s> A(T) => #execute(A, T) </s> when isRule(A) /\ isTerm(T)
For those of you familiar with the previous discussions on implementing strategies, you will notice that this approach lacks even the notion of #blocked. #blocked was an attribute which was usually false and because true only when no rule could be applied. It is not needed anymore as execution is now made explicit by #execute. If the rule cannot be executed on the given term, the function returns an empty set (or an empty Or for the symbolic engine).
The strategy rules above, coupled with the strategy expression in the initial configuration, give exactly the superheating/supercooling semantics currently hardcoded in the engine.
Furthermore, there is no need for a first class search anymore. It becomes just one particular strategy. The strategy semantics above is for execution, but we can easily adapt it to do search. We just replace a few of the semantic rules:
rule <s> A | B => A ~> [] | B </s> when !isTerm(A)
rule <s> A | B => B ~> A | [] </s> when !isTerm(B)
rule <s> A ~> [] | B => A | B </s> when isTerm(A)
rule <s> B ~> A | [] => A | B </s> when isTerm(B)
rule <s> A | B => Or(A, B) </s> when isTerm(A) /\ isTerm(B)
rule <s> (A ; B)(T) => B(A(T)) </s>
Going beyond search, note that the above extends seamlessly to symbolic execution. The terms are not necessarily disjunctions of ground configuration, they can be disjunctions (or even not necessarily disjunctions) of symbolic configurations.
In the same way, debugging becomes simply one application of strategies. The debugger can have full control over the rewrite engine by altering the <s> cell. E.g., to try to execute the heat1 rule above specifically, it can simply populate the <s> cell with heat1(#start). Furthermore, using K's IO capabilities, and entire complex interactive rewriter could be designed this way.
The debugger would also need a #match hooked function to return a specific substitution, which would still be represented in K.
I've intentionally overlooked some details about how the initial strategy is generated in practice, but we can easily assume we have helper functions to select particular rules for execution, e.g. tag(heat) reduce | would generate a | of all the rules tagged with heat.