Workspaces

A workspace is a forest, a finite multiset, of syntactic objects. The forest product is disjoint union with unit the empty forest, so a workspace is exactly what of' lifts into the Hopf algebra ConnesKreimer ℤ (UnorderedTree Vertex). A moved element occupies repeated isomorphic components, and the number of copies is the chain's multiplicity (Workspace.chainMultiplicity): chain identity lives at the workspace level, with no index on the trace leaf. Merge on workspaces and its identity with the algebraic Merge operator are in Merge/SyntacticObject.lean.

Main definitions

• Minimalist.Workspace: forests of syntactic objects.
• Minimalist.Workspace.chainMultiplicity: the multiplicity of a syntactic object in a workspace.

References

• [MCB25], §1.2 (Definition 1.2.1)

@[reducible, inline]

abbrev Minimalist.Workspace : Type

A workspace is a forest of syntactic objects.

Equations

• Minimalist.Workspace = UnorderedTree.Forest Minimalist.SyntacticObject

def Minimalist.Workspace.chainMultiplicity (S : SyntacticObject) (W : Workspace) : ℕ

chainMultiplicity S W = W.count S, the number of isomorphic copies of S in W.

Equations

• Minimalist.Workspace.chainMultiplicity S W = Multiset.count S W