A Category for Models

Let π’ž be the category of programs, where Ob(π’ž) and Hom(S, T)={fβ€…βˆ£β€…f(: : S): : T}. A model is a subcategory comprised of functions and types used in the code that implements that model. Then a model transformation is a function, t, on models M that induces a functor F : t(M)β†’M. We define the model transformation as function on models because you need to compute it going from the simple model to the more complex model, but the functor goes the other way, from the complex model to the simple model.

Properties of Transformations

Model transformations respect composition.

Proof: If t1(M)=Mβ€² there exists F : Mβ€²β†’M and t2(Mβ€²) = Mβ€³ there exists G : Mβ€³β†’Mβ€² then t2β€…βˆ˜β€…t1 induces a functor Gβ€…βˆ˜β€…F : Mβ€³β†’M by the definition of functor.

Examples

A simple model of gravity can be represented. Everyone knows the formula for the force of gravity, the sum of the masses divided by the double of the radius between them

$F = G \frac{m_1 + m_2}{2r}$

Oh wait, that isn’t right, it has that structure, but is it the sum or the product? And is twice the radius or the square of the radius?

A model transformation can recover the right model for us. The following figure show M on the left and Mβ€² on the right. The functor between them is shown using color.

gravity diagram

The functor from Mβ€² to M tells us how to transform Mβ€² back into M. We see that the only think that changed is Γ— becomes + and sqr becomes dbl. This is exactly the way a programmer would describe the difference between these two models.

We can see the notion of a fully faithful functor indicating that these models have the same structure. The functions in these two programs are in 1-1 correspondence. The notion of fully faithful functors says that for every pair of types S, T F maps HomMβ€²(S, T) to HomM(F(S),F(T)) with a 1-1 function. For this case F(S)=S for all types. So this reduces to HomMβ€²(S, T)β†’HomM(S, T) with a 1-1 function. Based on the sizes of the Hom sets, we see that there are only 4 possible fully faithful functors between these two models. The most obvious one is the one shown with color.

Isomorphism is too strict

You might think that since these diagrams look like graphs and the functors look like graph homomorphism, that graph isomorphism is a good definition of β€œmodels with the same structure”. But this is two strict.

In the following example the type graphs are not isomorphic, but there is a fully faithful functor between the model categories.

A category of models

Let ℳℴ𝒹 represent the category of models under transformation. Ob(ℳℴ𝒹) is the set of models and Homℳℴ𝒹(Mβ€²,M) is the set of functors from Mβ€² to M (ie. transformations from M to Mβ€²).

Perspective on Model Selection

Given an initial model M a set of morphisms in βˆͺxHomℳℴ𝒹(M, x) we want to pick the m that minisimizes some function β„“(m) which is the loss between the data and the model m. Suppose that T =β€„βŸ¨Ti⟩ is the set of transformations generated by {Tiβ€…βˆ£β€…iβ€„βˆˆβ€„β„}. We want to derive model selection algorithms that work for any M, ℓ, T.

These algorithms will exploit the algebra of the transformation set, for example if the set of transformations is just a compositional monoid then the only option is to enumerate the tree of possible transformations (List(T),β€…+β€…+, []) and pick the one that minimizes the loss. If the transformations have a stronger structure, such as forming a ring, and that structure is compatible with respect to the loss function, we should be able to find algorithms that exploit that structure.