lin-0053

3.2 Sketches as categorical theories

The sketch is more than a dataflow schema. It is a presentation of a categorical theory: generators provide the sorts and primitive operations, while path equations and designated universal constructions provide its axioms. This viewpoint continues the separation between syntax and semantics made explicit by Lawvere’s functorial semantics of algebraic theories [ Lawvere , 1963 ] .

A single-sorted finitary Lawvere theory is a small category whose objects are finite powers of one distinguished object. Its arrows represent operations, composition represents substitution, and equality of arrows records equational axioms. A model in \(\mathbf{Set}\) is a product-preserving functor. For example, a theory of monoids contains a multiplication \(m:X^2\to X\) and a unit \(e:1\to X\); associativity and the unit laws are equalities between the corresponding composite arrows. A product-preserving functor interprets these generators as an actual monoid.

Sketches enlarge this language. They can use many sorts, select particular cones and cocones, and present structures whose axioms involve specified limits or colimits. A learning sketch uses the same division of labor: \(\mathbb S\) is the theory, while a functor \(D\) is one attempted interpretation of it. Learning inside a fixed sketch changes the interpretation without silently changing the theory that the interpretation is supposed to satisfy.

¹1. Under standard size and arity hypotheses, categories of models of suitable limit theories and sketches are accessible or locally presentable. This makes a theory-generated model space amenable to construction from small presentable pieces [ Makkai and Paré , 1989 , Adámek and Rosický , 1994 ] . ↩

Definition 3.2 Sketch augmentation

A sketch augmentation is a morphism

\[ \iota :\mathbb S\longrightarrow \mathbb S^{+} \]

that transports the existing generators and declarations while possibly adding new objects, arrows, path equations, designated cones, or designated cocones. It induces a restriction functor

\[ \iota ^{*}: \operatorname {Mod}(\mathbb S^{+},\mathcal C) \longrightarrow \operatorname {Mod}(\mathbb S,\mathcal C) \]

that forgets the added structure.

For an old model \(D\), the fiber of \(\iota ^{*}\) over \(D\) is the space of its expansions to the augmented theory. An empty fiber says that the proposed theory is incompatible with \(D\). An essentially unique expansion is characteristic of a definitional extension. Multiple inequivalent expansions expose genuine underdetermination: the new generators or axioms require evidence not contained in the old model.

Boundary

Repairing a model of \(\mathbb S\) and augmenting \(\mathbb S\) are different learning problems. The first searches for a better interpretation of a fixed theory. The second changes the space of admissible interpretations and therefore requires stronger admission tests.