lin-0262

22.2.1 Theory repair as sketch augmentation

Chapter 3 interpreted a learning sketch as a categorical theory and a realized system as one of its models. This reveals a second level of the LINCS workflow. Ordinary repair changes \(D\in \operatorname {Mod}(\mathbb S,\mathcal C)\). Theory repair proposes a sketch augmentation

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

and thereby changes the category in which admissible models live. The induced restriction functor

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

makes the relationship between the two theories inspectable rather than rhetorical.

The fiber of \(\iota ^{*}\) over an old model records its possible expansions. If the fiber is essentially a singleton, the added vocabulary may be only definitional. If it contains several inequivalent expansions, the old theory does not determine the new structure. If it is empty for a previously successful model, the augmentation has rejected that model and must explain why. These cases prevent every successful redescription from being counted as a discovery.