ora-0017
1.5.1 The LEGO theory
1.5.1 The LEGO theory
Suppose a child encounters pieces that can be placed side by side, joined, and taken apart. A minimal one-sorted signature counts connected components. It contains parallel juxtaposition \(\otimes \), an attachment generator
and a detachment generator
If brick shapes or interfaces must be typed separately, the corresponding structure is a colored PROP rather than a one-sorted PROP. Symmetry exchanges independent inputs. Interchange says that independent attachments can be performed in either order. Where joining preserves enough alignment and identity information to be exactly reversible, the child may discover the equations
Closing these generators under composition and tensor produces a presented PROP \(\mathbb P_{\mathrm{LEGO}}\). Its morphisms are formal construction and deconstruction programs; an algebra
interprets those programs as actual configurations and manipulations.
For any typed symmetric monoidal signature \(\Sigma \) of LEGO operations and set \(E\) of well-typed equations, there is a PROP \(\mathbb P_{\Sigma ,E}=\mathsf{FPROP}(\Sigma )/E\) such that symmetric monoidal functors from it to \(\mathcal V\) are precisely interpretations of the generators in \(\mathcal V\) satisfying \(E\).
Form the free strict symmetric monoidal category on the typed generators, then quotient each hom-set by the smallest symmetric-monoidal congruence containing \(E\). A symmetric monoidal interpretation of the generators extends uniquely through the free construction and factors through the quotient exactly when it satisfies the equations.
Physical detachment is not automatically a two-sided inverse. If attachment forgets orientation, damages a piece, permits several decompositions, or is defined only for compatible interfaces, then the appropriate structure may be a partial inverse, a groupoid of reversible moves, a localization, or a finite-limit theory of admissible attachment domains. The theory is learned from the observed laws; invertibility must not be built in merely because an action is colloquially called taking apart.
The LEGO example displays three distinct identification targets. The child may learn a category of configurations and transformations, a small sketch of generators and relations presenting that category, and a functorial model connecting the formal operations to perception and action. Two different sketches can present equivalent theories, so successful theory learning cannot mean recovering a privileged naming scheme or generating list. It must be stated up to a doctrine-relative equivalence of theories or their model semantics.