Executable Frontier

Abstract

The executable frontier consists of pending nodes whose direct prerequisites are complete.

Theorem 1.1 (The complement frontier is exactly the ready pending set).

$$\begin{gathered} \forall edge:V\to V\to Prop,pending:\mathrm{Set}\left(V\right),node:V, \\ node\in \mathrm{executableFrontier}\left(edge,\mathrm{complement}\left(pending\right),pending\right)⟺ \\ (node\in pending\wedge \forall prerequisite:V,\mathrm{edge}\left(prerequisite,node\right)\Rightarrow \neg (prerequisite\in pending)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DagSemantics/ExecutableFrontier.mem_frontier_complement_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

A node belongs to the frontier computed over the complement of pending exactly when it is pending and none of its direct prerequisites remain pending.

The equivalence unfolds the definitions of executableFrontier and ReadyOver. It concerns direct prerequisites and does not replace them with arbitrary reachable ancestors.

References

• Truth anchor: D5/S3/ConceptDynamics/DagSemantics/ExecutableFrontier.mem_frontier_complement_iff
• Dependency: D5/S3/ConceptDynamics/DagSemantics/PrerequisiteClosure