A hundred-step chain of “every A is a B”, with dead ends at every turn.
deep-taxonomy-100.py · output · proof · check · try it in the playground
A taxonomy is a classification: a dog is a mammal, a mammal is an animal, and so on.
Imagine one that is a hundred levels deep. One individual, ind, sits at
the top level n0. Is ind also of type n100, a hundred levels down?
The catch: at every level the path splits three ways, and only one way leads further.
One fact and 300 rules. The first few:
fact(type('ind', 'n0'))
implied_by(type(X, 'n1'), type(X, 'n0'))
implied_by(type(X, 'i1'), type(X, 'n0'))
implied_by(type(X, 'j1'), type(X, 'n0'))
implied_by(type(X, 'n2'), type(X, 'n1'))
# … the same pattern down to n100 …
query(type(X, 'n100'))
Anything of type n0 is also n1, i1 and j1. But only n1 leads on;
i1 and j1 are dead ends. The last line asks the question.
type('ind', 'n100')
Yes: ind is of type n100.
This is a well-known benchmark (a standard test of speed), from the WellnessRules work cited in the file. It checks that a reasoner can follow a long chain without getting lost in the side branches.
The proof is one long chain, read from the answer back to the fact:
ind is n100 — rule 299, because ind is n99;ind is n99 — rule 296, because ind is n98;ind is n1 — rule 2, because ind is n0;ind is n0 — fact 1.That is 101 steps: one per level, plus the starting fact. None of the dead ends appear; the proof contains only what the answer needs.
The checker walks all 101 steps against the program:
Verdict: checked. 101 steps, all verified, nothing taken on trust.
The same benchmark comes in four sizes:
| Example | Levels | Proof steps |
|---|---|---|
| deep-taxonomy-10 | 10 | 11 |
| deep-taxonomy-100 | 100 | 101 |
| deep-taxonomy-1000 | 1,000 | 1,001 |
| deep-taxonomy-10000 | 10,000 | 10,001 |
The cost grows in a straight line with the depth: each level costs exactly
one step. --stats reports 101 inferences for this one.
python -m peye examples/deep-taxonomy-100.py
python -m peye --stats examples/deep-taxonomy-100.py
Or open it in the playground.
Change the last line to query(type(X, 'n50')): the answer becomes
type('ind', 'n50'), and --stats drops to 51 inferences.
A long chain of simple reasons is still simple to check. However deep the taxonomy, the proof is exactly as long as the path, and every link in it can be verified.