Derive a Consequence and Check a Requirement

In the last chapter the rules let us first establish a triangle’s existence, then tell whether it has a right angle. Now ask another question: are the derived properties consistent with each other? If one and the same figure is recognized as both right-angled and obtuse-angled, the fault lies in the model or in the source information.

Arxo provides a constraint for such a check. It tests information against a requirement and reports the result without deriving a new assertion. We will examine it in the same Euclid package, first with the original rules, then on a copy with a deliberate error.

Which properties we will compare

Besides the familiar orthogonion, the vocabulary contains two more relations: amblygonion means “the triangle is obtuse-angled”, and oxygonion means “the triangle is acute-angled”. Each relation, like orthogonion, takes a single argument of type Trigonon.

The rules recognize these properties by comparing the squares of the sides. For 3, 4, 5 we get a right-angled triangle. For 2, 3, 4 the sum of the squares of the smaller sides is 13, and the square of the largest is 16: the package derives obtuseness. For the triple 1, 1, 1 each square is less than the sum of the other two; acuteness follows.

The rules about the acute and obtuse angles refer to propositions II.12, II.13, and definition I.21. The package separately explains how the numerical tests were obtained from these fragments. They must not be mistaken for Euclid’s verbatim converse propositions[^chapter-6-model]. What matters for us is matching the results: an ordinary triangle belongs to one of three kinds, and the kinds exclude each other.

A requirement that derives nothing

Start with a pair of properties. If a triangle is recognized as right-angled, it must not at the same time be obtuse-angled. This requirement is recorded in the package as follows:

@source(STO_DEF21)
constraint OrthogonionKaiAmblygonionAsymbata {
    label grc unofficial "ἀδύνατον τὸ αὐτὸ τρίγωνον ὀρθογώνιόν τε εἶναι καὶ ἀμβλυγώνιον";
    label ru unofficial "инвариант §93.1: прямоугольный и тупоугольный — разные роды (определение I.21), и один треугольник не может быть обоими";
    for t: Trigonon;
    when orthogonion(t);
    require not amblygonion(t);
    severity error;
    message "треугольник признан и прямоугольным (I.48), и тупоугольным (II.12): при какой-то позиции квадрат стороны оказался и равен сумме квадратов двух других, и больше её";
}

After the constraint keyword stands the constraint’s name. The variable t and the when condition are familiar from rules: we check the properties of one object for which right-angledness is established. Instead of a then conclusion, a require clause is recorded here.

The line require not amblygonion(t) requires the negation of obtuseness. It does not itself create such a negative assertion. If information for the check is lacking, the constraint may remain undetermined. But if obtuseness is established, and there are no grounds against it, the requirement is violated.

severity error sets the diagnostic message’s level for a violation: an error. The message field holds an explanation that shows which properties proved incompatible. The words inside the message neither correct the source information nor change the rules.

Here the difference between the two constructs becomes visible. A rule adds a ground for its conclusion. A constraint checks a requirement against information already obtained, and stores the result of that check separately.

At least one of the three kinds

Another constraint checks the completeness of the classification: if the sides form a triangle, at least one of the three kinds must be established.

@source(STO_DEF21)
constraint TrichotomiaPliris {
    label grc unofficial "πᾶν τρίγωνον ἢ ὀρθογώνιον ἢ ἀμβλυγώνιον ἢ ὀξυγώνιόν ἐστιν";
    label ru unofficial "инвариант §93.1, ПОЛНОТА: всякий треугольник принадлежит одному из трёх родов — прямоугольному (I.48), тупоугольному (II.12) или остроугольному (II.13); четвёртого рода определение I.21 не знает";
    for t: Trigonon;
    when trigonon_estin(t);
    require orthogonion(t) or amblygonion(t) or oxygonion(t);
    severity error;
    message "тройка составляет треугольник, но не отнесена ни к одному из трёх родов: перечень I.21 перестал быть исчерпывающим, и обратные к II.12/II.13 лишились основания";
}

Here the requirement uses or for the first time. In the simple case without contradictions, establishing at least one of the listed properties suffices. The or itself does not require exactly one variant to hold. Other constraints cover the kinds’ incompatibility, including the one considered above.

The condition when trigonon_estin(t) is also essential. The triple 0, 3, 3 from the last chapter is not recognized as a triangle, so this requirement does not apply to it. The absence of a classification for such a triple does not violate the completeness of the triangle-kinds list.

No error does not mean every requirement is met

In the earlier scenarios we have already met the check:

expect issues_within(info);

It admits messages no higher than the informational level. This does not require the message list to be empty, nor does it confirm that every constraint is met. To see the latter, one must look at the result of the constraint’s check itself.

When the when condition is established without contradiction, four outcomes are possible:

These are the familiar four states applied to a requirement. The condition under which it is checked must be considered separately: the table concerns an established when[^chapter-6-constraint].

Look at triangle 3, 4, 5 in the source package. Right-angledness is established, so the completeness requirement TrichotomiaPliris is met: one of the three kinds is found. But amblygonion on this case has grounds neither for nor against. Its negation also has the state NEITHER. The constraint OrthogonionKaiAmblygonionAsymbata receives UNDETERMINED.

No contradiction is found here, but the negation of obtuseness is not established from this record. The constraint itself does not derive it. In the current execution UNDETERMINED produces no error message, so issues_within(info) passes. The absence of a reported error does not mean that the requirement is satisfied.

To see these results, one can print the explanation graph of the supplied scenario:

chapter6_graph=$(mktemp -d)
python3 reader_tools/prepare_question.py corpus/laws/doctrine/math/euclid-pythagoras/tests/01-aigyptiako-345.lawtest \
  --program corpus/clir/grc-euclid-pythagoras.lawir.json --imports \
  contexts/grc-euclid-pythagoras.json --out "$chapter6_graph"
law engine graph "$chapter6_graph" --json

The graph command shows nodes and links, and --json selects structured output. Search it for the constraint names, then find their constraint_check nodes. Each label contains the constraint’s name, the check result status, and the requirement’s requirementStatus. For OrthogonionKaiAmblygonionAsymbata, these are UNDETERMINED and NEITHER; for TrichotomiaPliris, they are SATISFIED and TRUE_ONLY. The rest of the graph can wait.

Prepare one check

To see a violation, change the rule on a separate copy of the package. We will introduce a deliberate error for the exercise: let the right-angledness test fire not only on the equality of the squares, but also when one square exceeds the sum of the other two.

Run all commands below from the reader companion directory in one terminal window: later commands use variables set by earlier ones. Create a temporary directory and copy the package and the supplied scenario about sides 2, 3, 4 into it:

chapter6_work=$(mktemp -d)
cp -R corpus/laws/doctrine/math/euclid-pythagoras "$chapter6_work/euclid-pythagoras"
cp corpus/laws/doctrine/math/euclid-pythagoras/tests/12-amblygonion-234.lawtest \
  "$chapter6_work/case234.lawtest"

The variable chapter6_work stores the working copy’s path. Open case234.lawtest in the created directory. Keep the header, context, and assertion about the sides as they are. Replace the question about obtuseness with a question about right-angledness and replace its expectations with the following. This is a change made for the exercise, not a verbatim excerpt from the corpus:

evaluate truth(grc.euclid.stoicheia_i::orthogonion(entity_ref("urn:case:eucl:trigonon")));
expect result_kind == PROPOSITION;
expect truth_status == NEITHER;
expect evaluation_status == COMPUTED;
expect issues_within(info);

For sides 2, 3, 4 the equality of the squares fails, so we expect exactly NEITHER for orthogonion. A separate relation about non-right-angledness in this package does not automatically create an explicit negation of orthogonion — the same manner of recording we examined in the last chapter.

First check the case against the original model:

law engine test "$chapter6_work/case234.lawtest" --program \
  corpus/clir/grc-euclid-pythagoras.lawir.json --imports \
  contexts/grc-euclid-pythagoras.json

All expectations hold. Now we have a baseline result against which to compare the effect of changing the rule.

Change the condition on the copy

In the working copy of the package, open the file 03-protasis-48.law. In the rule OrthogonionProsTritei find the line:

and (a * a + b * b == c * c);

Replace only that line with the following:

and (c * c >= a * a + b * b);

The sign >= means “greater than or equal”. The side c is moved to the left, so now the rule also covers the case in which its square exceeds the sum of the other two squares. That is exactly how things stand for the triple 2, 3, 4: 16 is greater than 13.

Until now we used the supplied model from corpus/clir. Editing a source rule does not change that prepared model: we must rebuild the copy. Refresh the copy’s compiled program and lock, then use pack to link its pinned dependencies. The final copy command selects the complete compiled model, including its dependencies, from that release:

mkdir -p "$chapter6_work/clir"
cp clir/grc-euclid-stoicheia-i.lawir.json "$chapter6_work/clir/"
law engine lower "$chapter6_work/euclid-pythagoras" \
  --imports contexts/grc-euclid-pythagoras.json \
  > "$chapter6_work/clir/grc-euclid-pythagoras.lawir.json"
law engine lock "$chapter6_work/euclid-pythagoras" --clir "$chapter6_work/clir" \
  --write
law pack --project "$chapter6_work/euclid-pythagoras" \
  --out "$chapter6_work/modified-release" --json
cp "$chapter6_work/modified-release/world.lawir.json" \
  "$chapter6_work/modified.lawir.json"
law engine test "$chapter6_work/case234.lawtest" --program \
  "$chapter6_work/modified.lawir.json" --imports contexts/grc-euclid-pythagoras.json

Three mismatches will appear in the check’s output:

  truth_status == NEITHER: в документе TRUE_ONLY
  evaluation_status == COMPUTED: в документе NON_EXECUTABLE
  issues_within(info): в документе CONSTRAINT_VIOLATED/error

Author’s paraphrase of the engine output above: instead of the expected NEITHER, the document gives TRUE_ONLY; instead of COMPUTED, NON_EXECUTABLE; and instead of messages within info, a CONSTRAINT_VIOLATED message of level error.

The first concerns the assertion: the changed rule gave orthogonion positive support, so TRUE_ONLY resulted instead of NEITHER. The second concerns execution: instead of COMPUTED, NON_EXECUTABLE was received. The third reports a constraint violation of level error.

We left the rules about obtuseness and non-right-angledness unchanged. They still apply to sides 2, 3, 4. So the mistaken right-angledness leads to two violations:

To find them in the graph for this same case, run:

chapter6_graph=$(mktemp -d)
python3 reader_tools/prepare_question.py "$chapter6_work/case234.lawtest" \
  --program "$chapter6_work/modified.lawir.json" --imports \
  contexts/grc-euclid-pythagoras.json --out "$chapter6_graph"
law engine graph "$chapter6_graph" --json

For the two named constraint_check nodes, status will carry the value VIOLATED. All assertions concern one object, urn:case:eucl:trigonon, for which the case states sides 2, 3, 4. The constraints found the results for this object incompatible. They do not say in which line we made the error, nor do they correct it.

Why one derivation’s explanation is not enough

The changed model can still show the path to right-angledness: the assertion about the sides, the existence rule’s application, the changed test’s application. That path helps reconstruct the derivation’s course, but it does not certify the recorded condition’s correctness.

An error-level violation is also reflected in the execution status[^chapter-6-outcome]. NON_EXECUTABLE in our trial does not mean that no step was computed: the grounds and the check results are present. It means that, because of a blocking error, the result did not receive the successful-execution status COMPUTED. Reading one TRUE_ONLY while ignoring this status would be an error.

A constraint can find a problem not only in a rule. If, under the source rules, right-angledness for sides 2, 3, 4 is recorded directly, the incompatibility will also arise. Both the rules and the source information must be checked. In this trial the cause is known in advance, because we changed one line ourselves.

Even satisfied constraints do not certify the whole model: they check only the stated requirements. In our problem this is a useful independent check of the consistency of several conclusions about one subject.

Try it yourself

1. Read TrichotomiaPliris in ordinary words. Explain why this constraint can be met even when the triangle is assigned two kinds. Which constraints must find such an incompatibility?
2. In the working copy, restore the original line with ==. Repeat the engine lock, pack, and copy commands above to rebuild modified.lawir.json, then run the same case234.lawtest against it. Predict which three mismatches will vanish, and check the result.
3. Compare the case with sides 0, 3, 3 from the last chapter with our changed model for 2, 3, 4. In which case does the rule lack an established premise, and in which did the rule apply and the resulting properties violate a requirement? Name the assertion’s state and the execution status separately.

Check your predictions

In the first exercise, at least one established kind suffices; the completeness of the list alone does not check mutual exclusion. In the second, after the rule is restored, NEITHER, COMPUTED, and no messages above level info will result again: the source check will pass. In the third, for sides 0, 3, 3 right-angledness has NEITHER with COMPUTED, while for the deliberately changed model for 2, 3, 4 it has TRUE_ONLY with NON_EXECUTABLE.

Now we can tell apart deriving a property, checking a requirement, and the success of execution. An undetermined requirement returns us to the question of completeness of information: when may the absence of an entry be taken to say something about the subject? That is the subject of the next chapter.

[^chapter-6-model]: The classification and constraints module: the opening comment accounts for deriving the numerical tests and the completeness role of the three kinds. Euclid’s fragments are pinned in sources.law. The English renderings of the propositions in this chapter are the translator’s own. [^chapter-6-constraint]: The Arxo specification, §§93.1–93.3: constraints, outcomes, and diagnostics. With a TRUE_ONLY condition, an unknown requirement yields UNDETERMINED; it produces no error message. [^chapter-6-outcome]: The Arxo specification, §181.2: result under a blocking diagnostic. An error-level error blocks COMPUTED; for a constraint violation NON_EXECUTABLE is used here.