Lesson 1.13: Basics of K Rewriting
The purpose of this lesson is to explain how rewrite rules that are not the definition of a function behave, and how, using these rules, you can construct a semantics of programs in a programming language in K.
Recap: Function rules in K
Recall from Lesson 1.2 that we have, thus far,
introduced two types of productions in K: constructors and functions.
A function is identified by the function attribute placed on the
production. As you may recall, when we write a rule with a function on the
left-hand side of the
=> operator, we are defining the meaning of that
function for inputs which match the patterns on the left-hand side of the rule.
If the argument to the function match the patterns, then the function is
evaluated to the value constructed by substituting the bindings for the
variables into the right-hand side of the rule.
However, function rules are not the only type of rule permissible in K, nor
even the most frequently used. K also has a concept of a
top-level rewrite rule. The simplest way to ensure that a rule is treated
as a top-level rule is for the left-hand side of the rule to mention one or
more cells. We will cover how cells work and are declared in more detail
in a later lesson, but for now, what you should know is that when we ran
in our very first example in Lesson 1.2 and got the following output:
<k> Yellow ( ) ~> . </k>
<k> is a cell, known by convention as the K cell. This cell is available
by default in any definition without needing to be explicitly declared.
The K cell contains a single term of sort
K is a predefined sort in K
with two constructors, that can be roughly represented by the following
syntax K ::= KItem "~>" K | "."
As a syntactic convenience, K allows you to treat
~> like it is an
associative list (i.e., as if it were defined as
syntax K ::= K "~>" K).
When a definition is compiled, it will automatically transform the rules you
write so that they treat the
K sort as a cons-list. Another syntactic
convenience is that, for disambiguation purposes, you can write
you would otherwise write
. and the meaning is identical.
Now, you may notice that the above grammar mentions the sort
KItem. This is
another built-in sort in K. For every sort
S declared in a definition (with
the exception of
KItem), K will implicitly insert the following
syntax KItem ::= S
In other words, every sort is a subsort of the sort
KItem, and thus a term
of any sort can be injected as an element of a term of sort
K, also called
a K sequence.
By default, when you
krun a program, the AST of the program is inserted as
the sole element of a K sequence into the
<k> cell. This explains why we
saw the output we did in Lesson 1.2.
With these preliminaries in mind, we can now explain how top-level rewrite
rules work in K. Put simply, any rule where there is a cell (such as the K
cell) at the top on the left-hand side will be a top-level rewrite rule. Once
the initial program has been inserted into the K cell, the resulting term,
called the configuration, will be matched against all the top-level
rewrite rules in the definition. If only one rule matches, the substitution
generated by the matching will be applied to the right-hand side of the rule
and the resulting term is rewritten to be the new configuration. Rewriting
proceeds by iteratively applying rules, also called taking steps, until
no top-level rewrite rule can be applied. At this point the configuration
becomes the final configuration and is output by
If more than one top-level rule applies, by default,
K will pick just one
of those rules, apply it, and continue rewriting. However, it is
non-deterministic which rule applies. In theory, it could be any of them.
By passing the
--search flag to
krun, you are able to tell
explore all possible non-deterministic choices, and generate a complete list of
all possible final configurations reachable by each nondeterminstic choice that
can be made. Note that the
--search flag to krun only works if you pass
--enable-search to kompile first.
Unlike top-level rewrite rules, function rules are not associated with any particular set of cells in the configuration (although they can contain cells in their function arguments and return value). While top-level rewrite rules apply to the entire term being rewritten, function rules apply anywhere a function application for that function appears, and are immediately rewritten to their return value in that position.
Another key distinction between top-level rules and function rules is that
function symbols, i.e., productions with the
function attribute, are
mathematical functions rather than constructors. While a constructor is
logically distinct from any other constructor of the same sort, and can be
matched against unconditionally, a function does not necessaraily have the
same restriction unless it happens to be an injective function. Thus, two
function symbols with different arguments may still ultimately produce the
same value and thus compare equal to one another. Due to this, concrete
execution (i.e., all K definitions introduced thus far; see Lesson 1.21)
introduces the restriction that you cannot match on a function symbol on the
left-hand side of a rule, except as the top symbol on the left-hand side of
a function rule. This restriction will be later lifted when we introduce the
Haskell Backend which performs symbolic execution.
Pass a program containing no functions to
krun. You can use a term of sort
LESSON-11-D. Observe the output and try to understand why you get
the output you do. Then write two rules that rewrite that program to another.
krun --search on that program and observe both results. Then add a third
rule that rewrites one of those results again. Test that that rule applies as
Using top-level rules to evaluate expressions
Thus far, we have focused primarily on defining functions over constructors in K. However, now that we have a basic understanding of top-level rules, it is possible to introduce a rewrite system to our definitions. A rewrite system is a collection of top-level rewrite rules which performs an organized transformation of a particular program into a result which expresses the meaning of that program. For example, we might rewrite an expression in a programming language into a value representing the result of evaluating that expression.
Recall in Lesson 1.11, we wrote a simple grammar of Boolean and integer
expressions that looked roughly like this (
module LESSON-13-A imports INT syntax Exp ::= Int | Bool | Exp "+" Exp | Exp "&&" Exp endmodule
In that lesson, we defined a function
eval which evaluated such expressions
to either an integer or Boolean.
However, it is more idiomatic to evaluate such expressions using top-level
rewrite rules. Here is how one might do so in K (
module LESSON-13-B-SYNTAX imports UNSIGNED-INT-SYNTAX imports BOOL-SYNTAX syntax Val ::= Int | Bool syntax Exp ::= Val > left: Exp "+" Exp > left: Exp "&&" Exp endmodule module LESSON-13-B imports LESSON-13-B-SYNTAX imports INT imports BOOL rule <k> I1:Int + I2:Int ~> K:K </k> => <k> I1 +Int I2 ~> K </k> rule <k> B1:Bool && B2:Bool ~> K:K </k> => <k> B1 andBool B2 ~> K </k> syntax KItem ::= freezer1(Val) | freezer2(Exp) | freezer3(Val) | freezer4(Exp) rule <k> E1:Val + E2:Exp ~> K:K </k> => <k> E2 ~> freezer1(E1) ~> K </k> [priority(51)] rule <k> E1:Exp + E2:Exp ~> K:K </k> => <k> E1 ~> freezer2(E2) ~> K </k> [priority(52)] rule <k> E1:Val && E2:Exp ~> K:K </k> => <k> E2 ~> freezer3(E1) ~> K </k> [priority(51)] rule <k> E1:Exp && E2:Exp ~> K:K </k> => <k> E1 ~> freezer4(E2) ~> K </k> [priority(52)] rule <k> E2:Val ~> freezer1(E1) ~> K:K </k> => <k> E1 + E2 ~> K </k> rule <k> E1:Val ~> freezer2(E2) ~> K:K </k> => <k> E1 + E2 ~> K </k> rule <k> E2:Val ~> freezer3(E1) ~> K:K </k> => <k> E1 && E2 ~> K </k> rule <k> E1:Val ~> freezer4(E2) ~> K:K </k> => <k> E1 && E2 ~> K </k> endmodule
This is of course rather cumbersome currently, but we will soon introduce
syntactic convenience which makes writing definitions of this type considerably
easier. For now, notice that there are roughly 3 types of rules here: the first
matches a K cell in which the first element of the K sequence is an
arguments are values, and rewrites the first element of the sequence to the
result of that expression. The second also matches a K cell with an
the first element of its K sequence, but it matches when one or both arguments
Exp are not values, and replaces the first element of the K sequence
with two new elements: one being an argument to evaluate, and the other being
a special constructor called a freezer. Finally, the third matches a K
sequence where a
Val is first, and a freezer is second, and replaces them
with a partially evaluated expression.
This general pattern is what is known as heating an expression, evaluating its arguments, cooling the arguments into the expression again, and evaluating the expression itself. By repeatedly performing this sequence of actions, we can evaluate an entire AST containing a complex expression down into its resulting value.
Write an addition expression with integers. Use
krun --depth 1 to see the
result of rewriting after applying a single top-level rule. Gradually increase
the value of
--depth to see successive states. Observe how this combination
of rules is eventually able to evaluate the entire expression.
Simplifying the evaluator: Local rewrites and cell ellipses
As you saw above, the definition we wrote is rather cumbersome. Over the
remainder of Lessons 1.13 and 1.14, we will greatly simplify it. The first step
in doing so is to teach a bit more about the rewrite operator,
=>. Thus far,
all the rules we have written look like
rule LHS => RHS. However, this is not
the only way the rewrite operator can be used. It is actually possible to place
a constructor or function at the very top of the rule, and place rewrite
operators inside that term. While a rewrite operator cannot appear nested
inside another rewrite operator, by doing this, we can express that some parts
of what we are matching are not changed by the rewrite operator. For
example, consider the following rule from above:
rule <k> I1:Int + I2:Int ~> K:K </k> => <k> I1 +Int I2 ~> K </k>
We can equivalently write it like following:
rule <k> (I1:Int + I2:Int => I1 +Int I2) ~> _:K </k>
When you put a rewrite inside a term like this, in essence, you are telling the rule to only rewrite part of the left-hand side to the right-hand side. In practice, this is implemented by lifting the rewrite operator to the top of the rule by means of duplicating the surrounding context.
There is a way that the above rule can be simplified further, however. K provides a special syntax for each cell containing a term of sort K, indicating that we want to match only on some prefix of the K sequence. For example, the above rule can be simplified further like so:
rule <k> I1:Int + I2:Int => I1 +Int I2 ...</k>
Here we have placed the symbol
... immediately prior to the
</k> which ends
the cell. What this tells the compiler is to take the contents of the cell,
treat it as the prefix of a K sequence, and insert an anonymous variable of
K at the end. Thus we can think of
... as a way of saying we
don't care about the part of the K sequence after the beginning, leaving
Putting all this together, we can rewrite
LESSON-13-B like so
module LESSON-13-C-SYNTAX imports UNSIGNED-INT-SYNTAX imports BOOL-SYNTAX syntax Val ::= Int | Bool syntax Exp ::= Val > left: Exp "+" Exp > left: Exp "&&" Exp endmodule module LESSON-13-C imports LESSON-13-C-SYNTAX imports INT imports BOOL rule <k> I1:Int + I2:Int => I1 +Int I2 ...</k> rule <k> B1:Bool && B2:Bool => B1 andBool B2 ...</k> syntax KItem ::= freezer1(Val) | freezer2(Exp) | freezer3(Val) | freezer4(Exp) rule <k> E1:Val + E2:Exp => E2 ~> freezer1(E1) ...</k> [priority(51)] rule <k> E1:Exp + E2:Exp => E1 ~> freezer2(E2) ...</k> [priority(52)] rule <k> E1:Val && E2:Exp => E2 ~> freezer3(E1) ...</k> [priority(51)] rule <k> E1:Exp && E2:Exp => E1 ~> freezer4(E2) ...</k> [priority(52)] rule <k> E2:Val ~> freezer1(E1) => E1 + E2 ...</k> rule <k> E1:Val ~> freezer2(E2) => E1 + E2 ...</k> rule <k> E2:Val ~> freezer3(E1) => E1 && E2 ...</k> rule <k> E1:Val ~> freezer4(E2) => E1 && E2 ...</k> endmodule
This is still rather cumbersome, but it is already greatly simplified. In the next lesson, we will see how additional features of K can be used to specify heating and cooling rules much more compactly.
LESSON-13-Cto add rules to evaluate integer subtraction.
Once you have completed the above exercises, you can continue to Lesson 1.14: Defining Evaluation Order.