1. Must Sing Rule Example¶
See the L4 code for this ‘Must Sing’ example
This example gives an overview of how to write a simple rule in L4 using the simple rule: “Every person who walks and eats or drinks must sing”.
We thank Matthew Waddington for originally authoring the case from which this example is drawn.
This chapter begins with a very simple rule, which is the input and is the contract we want to formalise:
“Every person who walks and eats or drinks must sing”.
Notice that there is ambiguity in thie sentence. We could mean:
Every person who walks and (eats or drinks) must sing.
Every person who (walks and eats) or drinks must sing.
The brackets disambiguate the sentence.
In interpretation 1, people who walk and people who eat or drink must sing. This is the interpretation shown in the google spreadsheet example.
We write interpretation 1 in L4 like this:
EVERY |
Person |
|
WHO |
walks |
|
AND |
eats |
|
OR |
drinks |
|
MUST |
sing |
In interpretation 2, people who walk and eat or people who drink must sing.
We write interpretation 2 in L4 like this:
EVERY |
Person |
|
WHO |
walks |
|
AND |
eats |
|
OR |
drinks |
|
MUST |
sing |
We transformed the rule into L4 with the following method:
Break the rule up into subclauses separated by keywords like EVERY, WHO, and AND.
Write down the nouns (“Person”) and verbs (“walks”, “eats”, “drinks”) in the cell to the right of the keywords.
We use indentation to disambiguate the sentence. An indentation is when the cells next to and below a keyword are blank.