Time-bounded description composition -- definitions

A chain-rule upper bound is not valid for arbitrary unrelated machines. This module therefore isolates the operational premise that a joint machine can compose a bounded program for firstOutput with a bounded conditional program for secondOutput given firstOutput. The program compiler, both source clocks, the target clock, and both description budgets remain explicit.

The joint output uses the library's canonical pair codec. The compiled program syntax is a parameter: later evaluator constructions may use pair, its reverse orientation, or a more efficient self-delimiting code.

def Complexity.TimeBoundedProgramCompositionAt {jointTapes firstTapes secondTapes : ℕ} (jointMachine : TM jointTapes) (firstMachine : TM firstTapes) (secondMachine : OracleTM secondTapes) (compile : List Bool → List Bool → List Bool) (firstOutput secondOutput : List Bool) (firstTime secondTime jointTime firstBound secondBound : ℕ) : Prop

Under fixed description budgets and clocks, compile composes an ordinary program for firstOutput and a random-access conditional program for secondOutput into a program for their canonical pair.

This is deliberately an operational contract, not an assumption that arbitrary machines satisfy a chain rule.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TimeBoundedConditionalPairCompositionAt {jointTapes conditionTapes resultTapes : ℕ} (jointMachine : TM jointTapes) (conditionMachine : TM conditionTapes) (resultMachine : OracleTM resultTapes) (compile : List Bool → List Bool → List Bool) (result condition : List Bool) (conditionTime resultTime jointTime conditionBound resultBound : ℕ) : Prop

Condition-first composition for the chain-rule orientation used by SoI. The ordinary program produces condition; the oracle program then produces result given random access to that condition; the joint output is nevertheless ordered as pair result condition.

Keeping this contract distinct from TimeBoundedProgramCompositionAt prevents an unnoticed swap between C(y) + C(x | y) and the encoded output pair x y.

Equations

• One or more equations did not get rendered due to their size.