Complete query blocks in finite decision trees -- definitions

queryAll queries continuation builds the complete decision tree that queries every coordinate in queries, in order, and then invokes continuation with the resulting finite restriction. This is the block operation used by the canonical switching tree.

def Complexity.DecisionTree.On.assignmentFor {N : ℕ} (queries : List (Fin N)) (input : BitString N) : Restriction.On N

The restriction induced by reading queries from a total input. Earlier list entries take precedence, although duplicate queries receive the same value and therefore do not change the result.

Equations

• Complexity.DecisionTree.On.assignmentFor [] input = Complexity.Restriction.On.empty
• Complexity.DecisionTree.On.assignmentFor (index :: rest) input = (Complexity.Restriction.On.single index (input index)).comp (Complexity.DecisionTree.On.assignmentFor rest input)

def Complexity.DecisionTree.On.assignmentOfPath {N : ℕ} : List (Fin N × Bool) → Restriction.On N

The finite restriction recorded by a query/value path. Earlier path entries take precedence if a malformed path repeats a query.

Equations

• Complexity.DecisionTree.On.assignmentOfPath [] = Complexity.Restriction.On.empty
• Complexity.DecisionTree.On.assignmentOfPath (query :: rest) = (Complexity.Restriction.On.single query.1 query.2).comp (Complexity.DecisionTree.On.assignmentOfPath rest)

def Complexity.DecisionTree.On.queryAll {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) : On N

Query every coordinate in a list before entering a continuation.

The continuation receives exactly the partial assignment collected along the query block.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DecisionTree.On.queryAll [] continuation = continuation Complexity.Restriction.On.empty

def Complexity.DecisionTree.On.deepBranch {N : ℕ} (queries : List (Fin N)) : (Restriction.On N → On N) → Restriction.On N

The partial assignment selected by the canonical deepest path through a complete query block.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DecisionTree.On.deepBranch [] x✝ = Complexity.Restriction.On.empty

def Complexity.DecisionTree.On.deepBlockPath {N : ℕ} (queries : List (Fin N)) : (Restriction.On N → On N) → List (Fin N × Bool)

The query/value prefix selected by the canonical deepest path through a complete query block.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DecisionTree.On.deepBlockPath [] x✝ = []