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.
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.
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.
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.
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.
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β²).
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.