Adding Builtins; Side Conditions
We have already added the builtin identifiers (sort Id) to LAMBDA expressions,
but those had no operations on them. In this lesson we add integers and
Booleans to LAMBDA, and extend the builtin operations on them into
corresponding operations on LAMBDA expressions. We will also learn how to add
side conditions to rules, to limit the number of instances where they can
apply.
The K tool provides several builtins, which are automatically included in all definitions. These can be used in the languages that we define, typically by including them in the desired syntactic categories. You can also define your own builtins in case the provided ones are not suitable for your language (e.g., the provided builtin integers and operations on them are arbitrary precision).
For example, to add integers and Booleans as values to our LAMBDA, we have to add the productions
syntax Val ::= Int | Bool
Int and Bool are the nonterminals that correspond to these builtins.
To make use of these builtins, we have to add some arithmetic operation
constructs to our language. We prefer to use the conventional infix notation
for these, and the usual precedences (i.e., multiplication and division bind
tighter than addition, which binds tighter than relational operators).
Inspired from SDF, we use > instead of
| to state that all the previous constructs bind tighter than all the
subsequent ones. See lambda.k.
The only thing left is to link the LAMBDA arithmetic operations to the
corresponding builtin operations, when their arguments are evaluated.
This can be easily done using trivial rewrite rules, as shown in lambda.k.
In general, the K tool attempts to uniformly add the corresponding builtin
name as a suffix to all the operations over builtins. For example, the
addition over integers is an infix operation named +Int.
Compile the new lambda.k definition and evaluate some simple arithmetic
expressions. For example, if arithmetic.lambda is (1+2*3)/4 <= 1, then
krun arithmetic.lambda
yields, as expected, true. Note that the parser took the desired operation
precedence into account.
Let us now try to evaluate an expression which performs a wrong computation,
namely a division by zero. Consider the expression arithmetic-div-zero.lambda
which is 1/(2/3). Since division is strict and 2/3 evaluates to 0, this
expression reduces to 1/0, which further reduces to 1 /Int 0 by the rule for
division, which is now stuck (with the current back-end to the K tool).
In fact, depending upon the back-end that we use to execute K definitions and
in particular to evaluate expressions over builtins, 1 /Int 0 can evaluate to
anything. It just happens that the current back-end keeps it as an
irreducible term. Other K back-ends may reduce it to an explicit error
element, or issue a segmentation fault followed by a core dump, or throw an
exception, etc.
To avoid requesting the back-end to perform an illegal operation, we may use a side condition in the rule of division, to make sure it only applies when the denominator is non-zero.
Like in other operational formalisms, the role of the K side
conditions is to filter the number of instances of the rule. The notion
of a side condition comes from logics, where a sharp distinction is made
between a side condition (cheap) and a premise (expensive). Premises are
usually resolved using further (expensive) logical derivations, while side
conditions are simple (cheap) conditions over the rule meta-variables within
the underlying mathematical domains (which in K can be extended by the user,
as we will see in future lessons). Regarded as a logic, K derives rewrite
rules from other rewrite rules; therefore, the K side conditions cannot
contain other rewrites in them (using =>). This contrasts other rewrite
engines, for example Maude, which
allow conditional rules with rewrites in conditions.
The rationale behind this deliberate restriction in K is twofold:
- On the one hand, general conditional rules require a complex, and thus slower rewrite engine, which starts recursive (sometimes exhaustive) rewrite sessions to resolve the rewrites in conditions. In contrast, the side conditions in K can be evaluated efficiently by back-ends, for example by evaluating builtin expressions and/or by calling builtin functions.
- On the other hand, the semantic definitional philosophy of K is that rule premises are unnecessary, so there is no need to provide support for them.
Having builtin arithmetic is useful, but writing programs with just lambda
and arithmetic constructs is still a pain. In the next two lessons we will
add conditional (if_then_else) and binding (let and letrec) constructs,
which will allow us to write nicer programs.
Go to Lesson 6, LAMBDA: Selective Strictness; Anonymous Variables.