Lesson 1.18: Term Equality and the Ternary Operator
The purpose of this lesson is to introduce how to compare equality of terms in K, and how to put conditional expressions directly into the righthand side of rules.
Term Equality
One major way you can compare whether two terms are equal in K is to simply
match both terms with a variable with the same name. This will only succeed
in matching if the two terms are equal structurally. However, sometimes this
is impractical, and it is useful to have access to a way to actually compare
whether two terms in K are equal. The operator for this is found in
domains.md in the KEQUAL
module. The operator is ==K
and takes two terms of sort K
and returns a
Bool
. It returns true if they are equal. This includes equality over builtin
types such as Map
and Set
where equality is not purely structural in
nature. However, it does not include any notion of semantic equality over
userdefined syntax. The inverse symbol for inequality is =/=K
.
Ternary Operator
One way to introduce conditional logic in K is to have two separate rules,
each with a side condition (or one rule with a side condition and another with
the owise
attribute). However, sometimes it is useful to explicitly write
a conditional expression directly in the righthand side of a rule. For this
purpose, K defines one more operator in the KEQUAL
module, which corresponds
to the usual ternary operator found in many languages. Here is an example of its
usage (lesson18.k
):
kmodule LESSON18 imports INT imports BOOL imports KEQUAL syntax Exp ::= Int  Bool  "if" "(" Exp ")" Exp "else" Exp [strict(1)] syntax Bool ::= isKResult(K) [function, symbol] rule isKResult(_:Int) => true rule isKResult(_:Bool) => true rule if (B:Bool) E1:Exp else E2:Exp => #if B #then E1 #else E2 #fi endmodule
Note the symbol on the righthand side of the final rule. This symbol is
polymorphic: B
must be of sort Bool
, but E1
and E2
could have been
any sort so long as both were of the same sort, and the sort of the entire
expression becomes equal to that sort. K supports polymorphic builtin
operators, but does not yet allow users to write their own polymorphic
productions.
The behavior of this function is to evaluate the Boolean expression to a Boolean, then pick one of the two children and return it based on whether the Boolean is true or false. Please note that it is not a good idea to use this symbol in cases where one or both of the children is potentially undefined (for example, an integer expression that divides by zero). While the default implementation is smart enough to only evaluate the branch that happens to be picked, this will not be true when we begin to do program verification. If you need short circuiting behavior, it is better to use a side condition.
Exercises

Write a function in K that takes two terms of sort
K
and returns anInt
: theInt
should be 0 if the terms are equal and 1 if the terms are unequal. 
Modify your solution to Lesson 1.16, Exercise 1 and introduce an
if
Stmt
to the syntax of the language, then implement it using the#if
symbol. Make sure to write tests for the resulting interpreter.
Next lesson
Once you have completed the above exercises, you can continue to Lesson 1.19: Debugging with GDB.