Computations, Results, Strictness; Rules Involving Cells

In this lesson we will learn about the syntactic category K of computations, about how strictness attributes are in fact syntactic sugar for rewrite rules over computations, and why it is important to tell the tool which computations are results. We will also see a K rule that involves cells.

K Computations

Computation structures, or more simply computations, extend the abstract syntax of your language with a list structure using ~> (read followed by or and then, and written \curvearrowright in Latex) as a separator. K provides a distinguished sort, K, for computations. The extension of the abstract syntax of your language into computations is done automatically by the K tool when you declare constructs using the syntax keyword, so the K semantic rules can uniformly operate only on terms of sort K. The intuition for computation structures of the form

t1 ~> t2 ~> ... ~> tn

is that the listed tasks are to be processed in order. The initial computation typically contains the original program as its sole task, but rules can then modify it into task sequences, as seen shortly.

Strictness in Theory

The strictness attributes, used as annotations to language constructs, actually correspond to rules over computations. For example, the strict(2) attribute of the assignment statement corresponds to the following two opposite rules (X ranges over Id and A over AExp):

X=A; => A ~> X=[];
A ~> X=[]; => X=A;

The first rule pulls A from the syntactic context X=A; and schedules it for processing. The second rule plugs A back into its context. Inspired from the chemical abstract machine, we call rules of the first type above heating rules and rules of the second type cooling rules. Similar rules are generated for other arguments in which operations are strict. Iterative applications of heating rules eventually bring to the top of the computation atomic tasks, such as a variable lookup, or a builtin operation, which then make computational progress by means of other rules. Once progress is made, cooling rules can iteratively plug the result back into context, so that heating rules can pick another candidate for reduction, and so on and so forth.

When operations are strict only in some of their arguments, the corresponding positions of the arguments in which they are strict are explicitly enumerated in the argument of the strict attribute, e.g., strict(2) like above, or strict(2 3) for an operation strict in its second and third arguments, etc. If an operation is simply declared strict then it means that it is strict in all its arguments. For example, the strictness of addition yields:

A1+A2 => A1 ~> []+A2
A1 ~> []+A2 => A1+A2
A1+A2 => A2 ~> A1+[]
A2 ~> A1+[] => A1+A2

It can be seen that such heating/cooling rules can easily lead to non-determinism, since the same term may be heated many different ways; these different evaluation orders may lead to different behaviors in some languages (not in IMP, because its expressions do not have side effects, but we will experiment with non-determinism in its successor, IMP++).

A similar desugaring applies to sequential strictness, declared with the keyword seqstrict. While the order of arguments of strict is irrelevant, it matters in the case of seqstrict: they are to be evaluated in the specified order; if no arguments are given, then they are assumed by default to be evaluated from left-to-right. For example, the default heating/cooling rules associated to the sequentially strict <= construct above are (A1, A2 range over AExp and I1 over Int):

A1<=A2 => A1 ~> []<=A2
A1 ~> []<=A2 => A1<=A2
I1<=A2 => A2 ~> I1<=[]
A2 ~> I1<=[] => I1<=A2

In other words, A2 is only heated/cooled after A1 is already evaluated.

While the heating/cooling rules give us a nice and uniform means to define all the various allowable ways in which a program can evaluate, all based on rewriting, the fact that they are reversible comes with a serious practical problem: they make the K definitions unexecutable, because they lead to non-termination.

Strictness in Practice; K Results

To break the reversibility of the theoretical heating/cooling rules, and, moreover, to efficiently execute K definitions, the current implementation of the K tool relies on users giving explicit definitions of their languages' results.

The K tool provides a predicate isKResult, which is automatically defined as we add syntactic constructs to KResult (in fact the K tool defines such predicates for all syntactic categories, which are used, for example, as rule side conditions to check user-declared variable memberships, such as V:Val stating that V belongs to Val).

The kompile tool, depending upon what it is requested to do, changes the reversible heating/cooling rules corresponding to evaluation strategy definitions (e.g., those corresponding to strictness attributes) to avoid non-termination. For example, when one is interested in obtaining an executable model of the language (which is the default compilation mode of kompile), then heating is performed only when the to-be-pulled syntactic fragment is not a result, and the corresponding cooling only when the to-be-plugged fragment is a result. In this case, e.g., the heating/cooling rules for assignment are modified as follows:

X=A; => A ~> X=[];  requires notBool isKResult(A)
A ~> X=[]; => X=A;  requires isKResult(A)

Note that non-termination of heating/cooling is avoided now. The only thing lost is the number of possible behaviors that a program can manifest, but this is irrelevant when all we want is one behavior.

As will be discussed in the IMP++ tutorial, the heating/cooling rules are modified differently by kompile when we are interested in other aspects of the language definition, such us, for example, in a search-able model that comprises all program behaviors. This latter model is obviously more general from a theoretical perspective, but, in practice, it is also slower to execute. The kompile tool strives to give you the best model of the language for the task you are interested in.

Can't Results be Inferred Automatically?

This is a long story, but the short answer is: No!. Maybe in some cases it is possible, but we prefer to not attempt it in the K tool. For example, you most likely do not want any stuck computation to count as a result, since some of them can happen simply because you forgot a semantic rule that could have further reduce it! Besides, in our experience with defining large languages, it is quite useful to take your time and think of what the results of your language's computations are. This fact in itself may help you improve your overall language design. We typically do it at the same time with defining the evaluation strategies of our languages. Although in theory K could infer the results of your language as the stuck computations, based on the above we have deliberately decided to not provide this feature, in spite of requests from some users. So you currently do have to explicitly define your K results if you want to effectively use the K tool. Note, however, that theoretical definitions, not meant to be executed, need not worry about defining results (that's because in theory semantic rules apply modulo the reversible heating/cooling rules, so results are not necessary).

A K Rule Involving Cells

All our K rules so far in the tutorial were of the form

rule left => right requires condition

where left and right were syntactic, or more generally computation, terms.

Here is our first K rule explicitly involving cells:

rule <k> X:Id => I ...</k> <state>... X |-> I ...</state>

Recall that the k cell holds computations, which are sequences of tasks separated by ~>. Also, the state cell holds a map, which is a set of bindings, each binding being a pair of computations (currently, the K builtin data-structures, like maps, are untyped; or, said differently, they are all over the type of computations, K).

Therefore, the two cells mentioned in the rule above hold collections of things, ordered or not. The ...s, which we also call cell frames, stand for more stuff there, which we do not care about.

The rewrite relation => is allowed in K to appear anywhere in a term, its meaning being that the corresponding subterm is rewritten as indicated in the shown context. We say that K's rewriting is local.

The rule above says that if the identifier X is the first task in the k cell, and if X is bound to I somewhere in the state, then X rewrites to I locally in the k cell. Therefore, IMP variables need to be already declared when looked up.

Of course, the K rule above can be translated into an ordinary rewrite rule of the form

rule <k> X ~> Rest </k> <state> Before (X |-> I) After </state>
  => <k> I ~> Rest </k> <state> Before (X |-> I) After </state>

Besides being more verbose and thus tedious to write, this ordinary rule is also more error-prone; for example, we may forget the Rest variable in the right-hand-side, etc. Moreover, the concurrent semantics of K allows for its rules to be interpreted as concurrent transactions, where the context is the read-only component of the transaction, while the subterms which are rewritten are read/write component of the transaction; thus, K rule instances can apply concurrently if they only overlap on read-only parts, while they cannot if regarded as ordinary rewrite logic rules. Note: our current implementation of the K tool is not concurrent, so K rules are in fact desugared as normal rewrite rules in the K tool.

Kompile imp.k using a documentation option and check out how the K rule looks in the generated document. The ... frames are displayed as cell tears, metaphorically implying that those parts of the cells that we do not care about are torn away. The rewrite relation is replaced by a horizontal line: specifically, the subterm which rewrites, X, is underlined, and its replacement is written underneath the line.

In the next lesson we define the complete K semantics of IMP and run the programs we parsed in the first lesson.

Go to Lesson 4, IMP: Configuration Abstraction, Part 1; Types of Rules.

MOVIE (out of date) [10'30"]