diff --git a/k-distribution/k-tutorial/1_basic/07_side_conditions/README.md b/k-distribution/k-tutorial/1_basic/07_side_conditions/README.md index 3a0f729a6d4..4d7bdf8972c 100644 --- a/k-distribution/k-tutorial/1_basic/07_side_conditions/README.md +++ b/k-distribution/k-tutorial/1_basic/07_side_conditions/README.md @@ -4,24 +4,28 @@ copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved. # Lesson 1.7: Side Conditions and Rule Priority -The purpose of this lesson is to explain how to write conditional rules in K, -and to explain how to control the order in which rules are tried. +In this lesson you will learn how to write conditional rules in K and how to +control the order in which rules are tried. -## Side Conditions +## Side conditions -So far, all of the rules we have discussed have been **unconditional rules**. -If the left-hand side of the rule matches the arguments to the function, the -rule applies. However, there is another type of rule, a **conditional rule**. -A conditional rule consists of a **rule body** containing the patterns to -match, and a **side condition** representing a Boolean expression that must -evaluate to true in order for the rule to apply. +So far, all rules we have discussed have been **unconditional**: if the +left-hand side of the rule matches the arguments to the function, the +rule applies _always_. However, K allows to specify **conditional rules**, +which also apply when the left-hand side of the rule matches the function +arguments, but _only_ if the condition specified within is met. You can +think of **conditional rules** as cases of +[piecewise functions](https://en.wikipedia.org/wiki/Piecewise_function), or +[patterns](https://www.haskell.org/tutorial/patterns.html) in Haskell. +They consist of a **rule body** containing the patterns to match, and a +**side condition** representing a Boolean expression that must evaluate to +`true` in order for the rule to apply. -Side conditions in K are introduced via the `requires` keyword immediately -following the rule body. For example, here is a rule with a side condition -(`lesson-07-a.k`): +Consider the following definition (`lesson-07-a.k`): ```k module LESSON-07-A + imports BOOL imports INT @@ -33,57 +37,74 @@ module LESSON-07-A | gradeFromPercentile(Int) [function] rule gradeFromPercentile(I) => letter-A requires I >=Int 90 + endmodule ``` -In this case, the `gradeFromPercentile` function takes a single integer -argument. The function evaluates to `letter-A` if the argument passed is -greater than 90. Note that the side condition is allowed to refer to variables -that appear on the left-hand side of the rule. In the same manner as variables -appearing on the right-hand side, variables that appear in the side condition -evaluate to the value that was matched on the left-hand side. Then the -functions in the side condition are evaluated, which returns a term of sort -`Bool`. If the term is equal to `true`, then the rule applies. Bear in mind -that the side condition is only evaluated at all if the patterns on the -left-hand side of the rule match the term being evaluated. +In the code above, the `gradeFromPercentile` function takes a single integer +argument and evaluates to `letter-A` only if the argument passed is greater +than or equal to 90: side condition `I >=Int 90`. + +Side conditions in K are introduced via the `requires` keyword immediately +following the rule body. Recall from [Lesson 1.5](../05_modules/README.md) +that `requires` has an additional meaning when used within a module. + +As expected, the side condition is a Boolean expression on variables that +appear on the left-hand side of the rule. Additionally, variables appearing +in the side condition evaluate to the same value as variables appearing on +the right-hand side. There are no surprises in the way conditioned rules are +evaluated either: if the patterns on the left-hand side of the rule match the +term being evaluated _and_ if the function in the side condition evaluates to +`true`, then the rule applies. ### Exercise -Write a rule that evaluates `gradeFromPercentile` to `letter-B` if the argument -to the function is in the range [80,90). Test that the function correctly -evaluates various numbers between 80 and 100. - -## `owise` Rules - -So far, all the rules we have introduced have had the same **priority**. What -this means is that K does not necessarily enforce an order in which the rules -are tried. We have only discussed functions so far in K, so it is not -immediately clear why this choice was made, given that a function is not -considered well-defined if multiple rules for evaluating it are capable of -evaluating the same arguments to different results. However, in future lessons -we will discuss other types of rules in K, some of which can be -**non-deterministic**. What this means is that if more than one rule is capable -of matching, then K will explore both possible rules in parallel, and consider -each of their respective results when executing your program. Don't worry too -much about this right now, but just understand that because of the potential -later for nondeterminism, we don't enforce a total ordering on the order in -which rules are attempted to be applied. - -However, sometimes this is not practical; It can be very convenient to express -that a particular rule applies if no other rules for that function are -applicable. This can be expressed by adding the `owise` attribute to a rule. -What this means, in practice, is that this rule has lower priority than other -rules, and will only be tried to be applied after all the other, -higher-priority rules have been tried and they have failed. - -For example, in the above exercise, we had to add a side condition containing -two Boolean comparisons to the rule we wrote to handle `letter-B` grades. -However, in practice this meant that we compare the percentile to 90 twice. We -can more efficiently and more idiomatically write the `letter-B` case for the -`gradeFromPercentile` rule using the `owise` attribute (`lesson-07-b.k`): +Write a rule that evaluates `gradeFromPercentile` to `letter-B` if the +argument to the function is in the range [80,90). Test that the function +correctly evaluates various numbers between 80 and 100. + +## Rule priority + +By default, K does not enforce an order in which the rules of a function are +tried, as all are assigned internally the same **priority**. It might not +come yet obvious to why this is the case since we have only discussed +functions so far in K, and a function is considered not well-defined if +multiple rules for evaluating it are capable of evaluating the same arguments +to different results. Yet, there is a reasoning behind this. In future +lessons we will introduce other types of rules in K, some of which can be +**non-deterministic**. It is because of this potential for nondeterminism +that we don't enforce a strict order in which rules are attempted to be +applied. + +You may have noticed that this is different than how pattern matching is +done, e.g., in Haskell. There, function evaluation proceeds in the syntactic +order of the patterns. Patterns specified first are tried first. In K, this +is not the case, and in certain situations, we may want a similar behavior. +It is convenient to express an order on rule trial or even that a particular +rule applies if no other rules for that function are applicable. We do the +latter with `owise` rule attribute, and the former by setting rule priorities +through `priority` attribute. + +### `owise` attribute + +As we mentioned above, K assigns by default all rules the same priority. +That's why rules can be executed in any order and not in the syntactic order +they are introduced. However, by adding attribute `owise` to a rule, +we express the fact that that particular rule can apply if no other rules +could have been applied. Under the hood, K assigns `owise` rules a lower +priority and this makes them to be tried only after all the other, +higher-priority rules have been tried and failed. + +Take again the exercise above, handling `letter-B` grades. You probably +solved it by adding a side condition containing _two_ Boolean checks +`I >=Int 80` and `I letter-A requires I >=Int 90 rule gradeFromPercentile(I) => letter-B requires I >=Int 80 [owise] + endmodule ``` @@ -110,7 +132,7 @@ multiple higher-priority rules, or multiple `owise` rules. What this means in practice is that all of the non-`owise` rules are tried first, in any order, followed by all the `owise` rules, in any order. -### Exercise +#### Exercise The grades `D` and `F` correspond to the percentile ranges [60, 70) and [0, 60) respectively. Write another implementation of `gradeFromPercentile` which @@ -118,25 +140,27 @@ handles only these cases, and uses the `owise` attribute to avoid redundant Boolean comparisons. Test that various percentiles in the range [0, 70) are evaluated correctly. -## Rule Priority +### `priority` attribute As it happens, the `owise` attribute is a specific case of a more general -concept we call **rule priority**. In essence, each rule is assigned an integer -priority. Rules are tried in increasing order of priority, starting with a -rule with priority zero, and trying each increasing numerical value -successively. +concept we call **rule priority**. -By default, a rule is assigned a priority of 50. If the rule has the `owise` -attribute, it is instead given the priority 200. You can see why this will -cause `owise` rules to be tried after regular rules. +Priorities in K are assigned an integer value. By default, rules are assigned +priority 50. `owise` rules, which are a specific case of this concept we +call **rule priority**, are given priority 200. However, it is also possible +to directly assign a numerical priority to a rule via the `priority` +attribute, in which case any non-negative integer is valid. -However, it is also possible to directly assign a numerical priority to a rule -via the `priority` attribute. For example, here is an alternative way -we could express the same two rules in the `gradeFromPercentile` function -(`lesson-07-c.k`): +Rules are tried in _increasing_ order of priority, starting with a rule with +priority zero, and trying each increasing numerical value successively. + +Consider the code in `lesson-07-c.k` below depicting an alternative way of +expressing the same two rules in the `gradeFromPercentile` function by means +of `priority` atttribute: ```k module LESSON-07-C + imports BOOL imports INT @@ -149,15 +173,16 @@ module LESSON-07-C rule gradeFromPercentile(I) => letter-A requires I >=Int 90 [priority(50)] rule gradeFromPercentile(I) => letter-B requires I >=Int 80 [priority(200)] + endmodule ``` -We can, of course, assign a priority equal to any non-negative integer. For -example, here is a more complex example that handles the remaining grades +Similarly, we can handle all grades only by means of `priority` attribute (`lesson-07-d.k`): ```k module LESSON-07-D + imports BOOL imports INT @@ -173,19 +198,45 @@ module LESSON-07-D rule gradeFromPercentile(I) => letter-C requires I >=Int 70 [priority(52)] rule gradeFromPercentile(I) => letter-D requires I >=Int 60 [priority(53)] rule gradeFromPercentile(_) => letter-F [priority(54)] + endmodule ``` -Note that we have introduced a new piece of syntax here: `_`. This is actually -just a variable. However, as a special case, when a variable is named `_`, it -does not bind a value that can be used on the right-hand side of the rule, or -in a side condition. Effectively, `_` is a placeholder variable that means "I -don't care about this term." +or, by using `owise` as well: + +```k +module LESSON-07-E + + ... + + rule gradeFromPercentile(I) => letter-A requires I >=Int 90 [priority(50)] + rule gradeFromPercentile(I) => letter-B requires I >=Int 80 [priority(51)] + rule gradeFromPercentile(I) => letter-C requires I >=Int 70 [priority(52)] + rule gradeFromPercentile(I) => letter-D requires I >=Int 60 [priority(53)] + rule gradeFromPercentile(_) => letter-F [owise] + +endmodule +``` + +Note that we used `owise` without a side condition. As we said above, both +usages are allowed in K. + +Note also that we have introduced a new piece of syntax—variable placeholder +`_`. As in Haskell or other functional languages, `_` does not bind a value +that can be used on the right-hand side of the rule, or in a side condition, +it simply means "I don't care about this term." + +In module `LESSON-07-E`, we have explicitly expressed the order in which the +rules of function `gradeFromPercentile` are tried. Since they are tried in +increasing numerical priority, we first try the rule with priority 50, then +51, then 52, 53, and finally 54. -In this example, we have explicitly expressed the order in which the rules of -this function are tried. Since rules are tried in increasing numerical -priority, we first try the rule with priority 50, then 51, then 52, 53, and -finally 54. +Because the rules have explicit priorities, their syntactic order does not +matter, only the ascending order of their priority values. Also, priorities +with same value are tried in any order. E.g., if we have two rules with +priority 52, first rule with priority 50 is tried, then rule with priority +51, then any of the rules with priority 52, then the other rule with priority +52, and finally the other rules in ascending order of priorities. As a final note, remember that if you assign a rule a priority higher than 200, it will be tried **after** a rule with the `owise` attribute, and if you assign @@ -196,17 +247,19 @@ explicit priority. 1. Write a function `isEven` that returns whether an integer is an even number. Use two rules and one side condition. The right-hand side of the rules should -be Boolean literals. Refer back to +be Boolean literals. Refer to [domains.md](../../../include/kframework/builtin/domains.md) for the relevant integer operations. -2. Modify the calculator application from Lesson 1.6, Exercise 2, so that division -by zero will no longer make `krun` crash with a "Divison by zero" exception. -Instead, the `/` function should not match any of its rules if the denominator -is zero. +2. Modify the calculator application from Lesson 1.6, Exercise 2, so that +division by zero will no longer make `krun` crash with a "Divison by zero" +exception. Instead, make sure the `/` function does not match any of its rules +if the denominator is zero. -3. Write your own implementation of `==`, `<`, `<=`, `>`, `>=` for integers and modify your solution from Exercise 2 to use it. -You can use any arithmetic operations in the `INT` module, but do not use any built-in boolean functions for comparing integers. +3. Write your own implementation of `==`, `<`, `<=`, `>`, `>=` for integers and +modify your solution from Exercise 2 to use it. You can use any arithmetic +operations in the `INT` module, but do not use any built-in boolean functions +for comparing integers. Hint: Use pattern matching and recursive definitions with rule priorities.