The clocked evaluation's spine #
The space-bounded spine (DescriptiveComplexity.Draw.Data.evalRule) ends its
last checkpoint in one of two outer phases – the sweep's advance, or the
post-sweep reset – because it runs inside an iteration. A clocked program has
neither: its evaluation runs once, and its last checkpoint leaves into
whatever phase the caller names. So the spine's rules
are not the space-bounded ones at another embedding; they are two rules per
checkpoint instead of three, at the clocked program's own phases
(DescriptiveComplexity.Draw.NexPh).
Everything else is shared: the sites are DescriptiveComplexity.Draw.EvalSite,
the machineries' rules are the parameter, and the ownership and separation
proofs are the same case analysis with the dead third rule gone.
The run is nexEval_reachesIn, and it is the space-bounded spine's count with
the same shape: one machinery's width plus its dispatch and its walk back, once
per variable.
The file also assembles the program: the spine's rules at the shared
machineries – a clocked program's tower above the atom is the space-bounded one,
PMF, SMF, SEF and varRuleF and all – with
nexEvalHosrcF/nexEvalSepF, and nexProg – the outer layer's rules at the
two sweep specifications with the evaluation's as their parameter. That last is
built directly rather than through
DescriptiveComplexity.Draw.Assembly, because a clocked program is not
deterministic: its guess site fires three rules on the same data, which is the
one piece of nondeterminism it has, and what does hold there is
DescriptiveComplexity.Draw.Data.nexSep_postGuess.
The rules of a clocked checkpoint: the walk back to the marker, and the one dispatch – into the variable's machinery below the last checkpoint, out of the evaluation at it.
- stay : NexEvalChkRule
Walk left back to the marker.
- dsp : NexEvalChkRule
Dispatch: into the machinery, or out of the evaluation.
Instances For
Dependency graph
Dependency graph
Dependency graph
The rule shape of each clocked evaluation site.
Equations
Instances For
Dependency graph
The rules of a clocked evaluation's spine: per checkpoint the walk back and the dispatch; the sub-machineries' rules are the parameter, and the exit at the last checkpoint is the caller's phase.
Equations
- One or more equations did not get rendered due to their size.
- dt.nexEvalRule one ruleM subEntry exitPh (DescriptiveComplexity.Draw.EvalSite.sub s) ρ = ruleM s ρ
Instances For
Dependency graph
The spine at the clocked machineries #
The types of the spine, and its rules at the clocked variable machineries: what
DescriptiveComplexity.Draw.Data.nexRule takes as its evaluation parameter.
The phases are EvalPh over the machineries', as in the space-bounded program;
only the machineries are the clocked ones and the exit is the accepting phase.
The rule shape of the clocked evaluation's sites: the spine's own, two rules per checkpoint, over the machinery sites of the shared tower.
Instances For
Dependency graph
The rules of the clocked evaluation's machineries: one copy of the clocked variable machinery per spine position – its exit the next checkpoint – and the output's, whose exit is the accepting phase.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The rules of the clocked evaluation: the spine over the machineries,
leaving at the last checkpoint into the output's machinery, whose own exit
is the accepting phase. The accepting predicate reads that machinery's verdict
bit, so the evaluation has to run it: a last checkpoint that went straight to
acceptP would leave the bit unwritten.
Equations
- dt.nexEvalRuleF zero one args = dt.nexEvalRule one (dt.nexSmRule zero one args) dt.smEntry (DescriptiveComplexity.Draw.NexPh.evalP (DescriptiveComplexity.Draw.EvalPh.sub dt.smEntryOut))
Instances For
Dependency graph
The clocked program #
The rule set assembled: the outer layer's rules at the two sweep
specifications, with the evaluation's as their parameter. Unlike the
space-bounded program this is not an
DescriptiveComplexity.Draw.Assembly – the guess site fires three rules on the
same data, which is the program's one piece of nondeterminism – so the record
is built directly and the separation that does hold is
DescriptiveComplexity.Draw.Data.nexSep_postGuess.
The rule names of the clocked program: a site of its outer layer, or of its evaluation, and one of that site's rules.
Equations
- dt.NexRIx = ((i : DescriptiveComplexity.Draw.NexSite dt.SEF) × DescriptiveComplexity.Draw.NexSh dt.SEF (Option dt.KIx) G dt.NexSESh i)
Instances For
Dependency graph
The clocked program: the outer layer's rules – the opening step, the build sweep, the walk home, the guess sweep, the walk home – with the clocked evaluation's as their parameter, and the reduction's constants. The accepting phase is the outer layer's, and its verdict is read from the control exactly as the space-bounded program's is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The spine's run, on a clock: from the checkpoint before the first variable at the marker to the checkpoint after the last, one machinery run per position, each with its dispatch and its walk back.