A tree recognizer in the Bellantoni-Cook class

Three expressions of B deciding whether a bitstring is the preorder spelling of a binary tree, and their correctness against the Valid predicate of the encoding. Composed with RankedAlphabet.valid_iff_exists_spell, isTreeSem_eq_singleton_iff_exists_spell states that an expression of B accepts exactly the spellings of binRanked's terms. BellantoniCook.BC reformulates [BellantoniCook1992]'s class; by [HeraudNowak2011] Theorems 1 and 2, which relate B to Cobham's class in both directions, composed with Cobham's theorem identifying Cobham's class with the polynomial-time functions, B coincides with the polynomial-time functions. That composition is used and not proved here, so the membership test lies in that class without a separate complexity argument.

The recognizer is a single right-to-left scan rather than a recursive descent. A descent would parse the second subtree from a remainder the first call computes, which sits in safe position, and recursion on a safe argument is what the class forbids.

Main definitions

BellantoniCook.zeroAtRaw, BellantoniCook.oneAtRaw — the empty bitstring and the one-bit string [true] at an arbitrary arity.

BellantoniCook.falseAtRaw — the one-bit string [false] at an arbitrary arity.

BellantoniCook.comb — the stack depth and the underflow verdict in a single value, of arity (1, 0).

BellantoniCook.eqOne — whether a bitstring has length one, of arity (0, 1).

BellantoniCook.isTree — the recognizer, of arity (1, 0).

BellantoniCook.combSem, BellantoniCook.eqOneSem and BellantoniCook.isTreeSem — the meaning of each of the three at its arity, over which every statement of the module is stated.

Main statements

BellantoniCook.combSem_eq — the scan computes RankedAlphabet.Binary.depth in unary, offset by one, while RankedAlphabet.Binary.ok holds, and [false] once it has failed.

BellantoniCook.eqOneSem_eq — eqOne accepts exactly the bitstrings of length one.

BellantoniCook.isTreeSem_eq_singleton_iff_valid — isTree accepts exactly the words binRanked's scan accepts.

BellantoniCook.isTreeSem_eq_singleton_iff_exists_spell — equivalently, exactly the spellings of binRanked's terms.

BellantoniCook.isTreeSem_eq_ite — the recognizer as the indicator of binRanked's scan.

Implementation notes

The scan carries the stack depth and the underflow verdict in one recursive value, told apart by its head. While no node bit has been read below depth two the value is the depth in unary offset by one, so its head is true; once one has been, the value is [false], which the node step reproduces, that value's two predecessors being empty. Each bit is read once.

Each unfolding lemma is stated per constructor with the recursive value exposed on the right. Sem is a function type, so evalRec recurses at a function motive and every eliminator in the chain sits there; eliminators at function motives reduce only when their scrutinee is a constructor, so a symbolic-bit or fold-shaped statement is not definitional.

Every unfolding lemma closes by rfl across the module boundary, and so depends on the @[expose] attributes Basic.lean carries on Direction, rc, q, sig, compChildren, BC, evalRec, evalValue, evalStep and BC.eval. Removing any of them leaves those lemmas stuck; the failure is silent at the language server and appears at lake build.

combSem, eqOneSem and isTreeSem name each meaning at its arity, so that the arity pair is reduced and rewriting under it type-checks. A meaning taken through the Sigma projection instead has a type headed by that projection rather than by an arrow, and rw under it fails as not type-correct at implicit transparency.

References

[BellantoniCook1992]

[HeraudNowak2011]

Tags

Bellantoni-Cook, polytime, implicit computational complexity, safe recursion, binary tree, preorder, recognizer

The empty bitstring at an arbitrary arity.

The one-bit string [true] at an arbitrary arity.

The one-bit string [false] at an arbitrary arity.

Prepend true to the recursive value.

Drop the low bit of the recursive value.

The guard of the node step: the recursive value with two bits dropped. It is empty exactly when the value is the failure flag, whose two predecessors truncate to the empty bitstring, or a depth below two.

The leaf step: push a level onto a live value, whose head is true, and return the failure flag on a value that is empty or has head false.

The node step: pop a level when at least two remain, and return the failure flag otherwise. An existing failure propagates, its guard being empty.

The raw tree of the scan. The base is [true], the empty bitstring having depth zero and satisfying RankedAlphabet.Binary.ok.

The stack depth and the underflow verdict of a bitstring in one value: the depth in unary, offset by one so that a live value is non-empty with head true, and [false] once a node bit has been read below depth two.

The inner conditional of eqOne: whether the predecessor of the argument is empty. The even branch is unreachable only under this module's own use, where the argument is always a unary numeral; the expression and its characterization are stated for an arbitrary bitstring, over which the branch is reached.

The raw tree of the one-test: empty is not one, and otherwise the argument is one exactly when its predecessor is empty.

Whether a bitstring has length one, returning [true] or [].

The raw tree of the recognizer: the scan's predecessor has length one.

The recognizer: whether a bitstring is the preorder spelling of a binary tree. The output is [true] or [], so correctness is an equation rather than a disequation.

comb at its declared arity. Elaborating this is the assertion that BC.arity comb is (1, 0).

eqOne at its declared arity.

isTree at its declared arity.

The scan's meaning at its arity, ascribed so that the arity pair is reduced and rewriting under it type-checks.

The one-test's meaning at its arity, ascribed likewise.

The recognizer's meaning at its arity, ascribed likewise.

The scan's value on the empty bitstring: depth zero, offset by one.

A leaf bit pushes a level onto a live value, and is absorbed by a failure.

A node bit pops a level when at least two remain, and fails otherwise. The guard is the value with two bits dropped, so a failure, whose two predecessors are empty, propagates.

The scan computes the stack depth in unary, offset by one, while RankedAlphabet.Binary.ok holds, and the absorbing value [false] once it has failed.