Deep Taxonomy 100000

A hundred thousand steps of reasoning, every one written down and checked.

deep-taxonomy-100000.js · output · proof · check · try it in the playground

The question

A taxonomy is a tree of categories: a robin is a bird, a bird is an animal, and so on. Here the tree is a hundred thousand levels deep, and at every level it also splits into two side branches that go nowhere.

We know one thing: an individual, 'ind', is in the top category 'n0'.

Is 'ind' in category 'n100000', at the very bottom? And can the computer show all hundred thousand steps — and have them checked?

A benchmark, at five sizes

This is the deep-taxonomy benchmark, a standard stress test for reasoners. The collection has it at five depths, and this is the largest:

Same shape each time; only the length of the chain changes.

What we tell eyecode

One fact, then three rules per level — 300,000 rules in all. Listed one by one they would make a 14 MB program, so a loop states them:

fact(type('ind', 'n0'))
for (let level = 1; level <= 100000; level++) {
  implied_by(type(X, `n${level}`), type(X, `n${level - 1}`))
  implied_by(type(X, `i${level}`), type(X, `n${level - 1}`))
  implied_by(type(X, `j${level}`), type(X, `n${level - 1}`))
}
query(type(X, 'n100000'))

The program is JavaScript, so it can compute its own rules: the loop states exactly the same clauses the long version would, in the same order. Read implied_by(type(X, 'n2'), type(X, 'n1')) as anything in n1 is also in n2. The i and j rules are the dead-end side branches.

What eyecode concludes

type('ind', 'n100000')

One answer: yes.

eyecode works backward from the question: to be in n100000, be in n99999; … all the way up to the fact we gave. The search is an explicit machine inside eyecode, so a hundred thousand levels deep is no problem.

Why: the proof in plain words

The proof is a chain of 100,001 steps:

1. 'ind' is in 'n0' — a fact we gave (fact 1).
2. So 'ind' is in 'n1' — rule 2.
3. So 'ind' is in 'n2' — rule 5.
4. … one step per level …
5. So 'ind' is in 'n100000' — rule 299999.

Each step names the exact rule it used, by number. Rules are numbered in the order the loop states them, so rule 299999 is the n rule of the last level. The 200,000 side-branch rules never appear: they do not help answer the question.

Checked, not just claimed

A separate checker read all 100,001 steps against the program and confirmed that each is an exact instance of the rule it cites, that the chain never loops back on itself, and that every step serves the answer.

Verdict: checked. All 100,001 steps verified, and nothing taken on trust.

The program is a few lines; its proof is about 14.5 MB, because a proof records every step it claims.

Try it

eyecode examples/deep-taxonomy-100000.js            # the answer
eyecode --stats examples/deep-taxonomy-100000.js    # and its cost

--stats reports "inferences":100001 — one step per level, plus the fact. Or open it in the playground.

Change the last line to query(type(X, 'j50000')) and run with --stats again: the answer is type('ind', 'j50000'), a side branch halfway down, reached in 50001 steps.

Takeaway

From ten levels to a hundred thousand, only the cost grows, in step with the depth, and the answer stays just as followable and just as checkable. And because the program is JavaScript, a rule set this large can be stated in a few lines.