<p>The support for building towers of category constructors is one of the main design features of CAP. Many categories that appear in the various applications can be modeled by towers of multiple category constructors. The category constructor <code class="func">ReinterpretationOfCategory</code> (<a href="chap12.html#X81D06FCA7ECE38C4"><span class="RefLink">12.6-1</span></a>) allows adding one last layer on top which allows expressing the desired (re)interpretation of such a modeling tower. In particular, this category constructor allows specifying the name of the category together with customized methods for the operations</p>
<ul>
<li><p>ObjectConstructor</p>
</li>
<li><p>MorphismConstructor</p>
</li>
<li><p>ObjectDatum</p>
</li>
<li><p>MorphismDatum</p>
</li>
</ul>
<p>in order to reflect the desired (re)interpretation with a user-interface that is independent of the modeling tower (see below for details). Note that the same tower might have multiple interpretations.</p>
<p>The reinterpretation <code class="code">R</code> is isomorphic to the top category <code class="code">cat_n</code> in the tower. In practice, the word <q>tower</q> stands more generally for a finite poset with a greatest element.</p>
<p>We will show how one can reinterpret a category with the following guiding example: We reinterpret <code class="code">Opposite( CategoryOfRows( R ) )</code> as <code class="code">CategoryOfColumns( R )</code> using <code class="func">ReinterpretationOfCategory</code> (<a href="chap12.html#X81D06FCA7ECE38C4"><span class="RefLink">12.6-1</span></a>) with the options described in the following (see <code class="code">CategoryOfColumns_as_Opposite_CategoryOfRows.gi</code> in <code class="code">AdditiveClosuresForCAP</code> for a full implementation).</p>
<ol>
<li><p>Set the options <code class="code">category_filter</code>, <code class="code">category_object_filter</code>, and <code class="code">category_morphism_filter</code> to the filters corresponding to the data structure of the desired reinterpretation, e.g. <code class="code">IsCategoryOfColumns</code>, <code class="code">IsCategoryOfColumsObject</code>, and <code class="code">IsCategoryOfColumsMorphism</code>.</p>
</li>
<li><p>Set <code class="code">object_constructor</code>, <code class="code">object_datum</code>, <code class="code">morphism_constructor</code>, and <code class="code">morphism_datum</code> to the functions one would write for <code class="code">ObjectConstructor</code> and so on for a primitive implementation of the desired reinterpretation. In our example, <code class="code">object_constructor</code> takes the reinterpretation <code class="code">R</code> (which lies in <code class="code">IsCategoryOfColumns</code> due to the filter set in the first step) and an integer, and returns a CAP object in the category with attribute <code class="code">RankOfObject</code> set to the integer, just like a primitive implementation of <code class="code">CategoryOfColumns</code> would do.</p>
</li>
<li><p>Set <code class="code">modeling_tower_object_constructor</code>, <code class="code">modeling_tower_object_datum</code>, <code class="code">modeling_tower_morphism_constructor</code>, and <code class="code">modeling_tower_morphism_datum</code>: <code class="code">modeling_tower_object_constructor</code> gets the same input as <code class="code">object_constructor</code> but must return the corresponding object in the tower <code class="code">cat_n</code>. <code class="code">modeling_tower_object_datum</code> has the same output as <code class="code">object_datum</code> but gets the reinterpretation <code class="code">R</code> and an object in the tower <code class="code">cat_n</code> as an input. In our example, <code class="code">modeling_tower_object_constructor</code> gets the reinterpretation <code class="code">R</code> and an integer as in step 2 and wraps the integer as a <code class="code">CategoryOfRowsObject</code> and the result as an object in the opposite category. <code class="code">modeling_tower_object_datum</code> gets the reinterpretation <code class="code">R</code> and an object in <code class="code">Opposite( CategoryOfRows( R ) )</code> (that is, an integer boxed as a category of rows object boxed as an object in the opposite category) and returns the underlying integer. <code class="code">modeling_tower_morphism_constructor</code> and <code class="code">modeling_tower_morphism_datum</code> are given analogously.</p>
</li>
</ol>
<p>By composing <code class="code">modeling_tower_object_datum</code> with <code class="code">object_constructor</code> and <code class="code">modeling_tower_morphism_datum</code> with <code class="code">morphism_constructor</code> (with suitable source and range), <code class="code">ReinterpretationOfCategory</code> defines a functor "Reinterpretation" from <code class="code">cat_n</code> to <code class="code">R</code>. Similarly, it defines a functor "Model" from <code class="code">R</code> to <code class="code">cat_n</code> by composing <code class="code">object_datum</code> with <code class="code">modeling_tower_object_constructor</code> and <code class="code">morphism_datum</code> with <code class="code">modeling_tower_morphism_constructor</code> (with suitable source and range). "Reinterpretation" should be an isomorphism of categories with inverse "Model". More precisely, one has to take care of the following things:</p>
<ul>
<li><p>Since <code class="code">R</code> should just be a reinterpretation of <code class="code">cat_n</code> with a nicer data structure, we certainly want "Reinterpretation" to be an equivalence of categories with pseudo-inverse "Model".</p>
</li>
<li><p><code class="code">ReinterpretationOfCategory</code> copies all properties from <code class="code">cat_n</code> to <code class="code">R</code>, including properties like <code class="code">IsSkeletalCategory</code> which are not necessarily preserved by mere equivalences.</p>
</li>
<li><p>To fulfill the specification of WithGiven operations, reinterpreting a WithGiven object <code class="code">A</code> in <code class="code">cat_n</code> as an object in <code class="code">R</code> and taking its model again must give an object equal to <code class="code">A</code>. So we require applying "Reinterpretation" and then "Model" to give the identity. Conversely, let <code class="code">B_1</code> be an object in <code class="code">R</code>. We take its model and reinterpret this again to form an object <code class="code">B_2</code>. By construction of <code class="code">R</code>, <code class="code">B_1</code> and <code class="code">B_2</code> are equal if and only if their models are equal. But since applying "Reinterpretation" and then "Model" gives the identity, taking the model of <code class="code">B_2</code> simply gives an object equal to the model of <code class="code">B_1</code>. Thus, also <code class="code">B_1</code> and <code class="code">B_2</code> are equal. Hence, "Reinterpretation" has to be an equivalence which is a bijection on objects, and hence an isomorphism (although "Model" is not necessarily its inverse). Note: Alternatively, one can make sure that WithGiven operations in <code class="code">cat_n</code> are only called via the corresponding non-WithGiven operation in <code class="code">cat_n</code>. This can be achieved by reinterpreting all operations of <code class="code">cat_n</code> (i.e. creating <code class="code">R</code> with <code class="code">only_primitive_operations := false</code>), disabling redirect functions (i.e. creating <code class="code">R</code> with the option <code class="code">overhead := false</code>) and not calling WithGiven operations of <code class="code">R</code> manually.</p>
<p>Operations in <code class="code">ReinterpretationOfCategory</code> are implemented as follows:</p>
<ol>
<li><p>Apply <code class="code">object_datum</code> and <code class="code">morphism_datum</code> to the input to get the underlying data.</p>
</li>
<li><p>Apply <code class="code">modeling_tower_object_constructor</code> and <code class="code">modeling_tower_morphism_constructor</code> to the underlying data to get objects and morphisms in the tower <code class="code">cat_n</code>.</p>
</li>
<li><p>Apply the operation of the tower <code class="code">cat_n</code>.</p>
</li>
<li><p>Apply <code class="code">modeling_tower_object_datum</code> or <code class="code">modeling_tower_morphism_datum</code> to the result to get the underlying data.</p>
</li>
<li><p>Apply <code class="code">object_constructor</code> or <code class="code">morphism_constructor</code> to the underlying data to get an object or a morphism in the reinterpretation <code class="code">R</code>.</p>
</li>
</ol>
<p>The first two steps define the functor "Model" and the last two steps define the functor "Reinterpretation". "Reinterpretation" on objects and morphisms is called <code class="code">ReinterpretationOfObject</code> and <code class="code">ReinterpretationOfMorphism</code> in the code. "Model" on objects and morphisms is called <code class="code">ModelingObject</code> and <codeclass="code">ModelingMorphism</code> in the code.</p>
<h4>12.4 <span class="Heading">Relation to <code class="code">CompilerForCAP</code></span></h4>
<p>The operation of the tower <code class="code">cat_n</code> (step 3 above) usually unboxes objects and morphisms, operates on the underlying data, and boxes the result. The unboxing usually cancels with step 2 above, and boxing the result usually cancels with step 4 above. If one now compiles the operations of the reinterpretation <code class="code">R</code>, only the following steps remain:</p>
<ol>
<li><p>Apply <code class="code">object_datum</code> and <code class="code">morphism_datum</code> to the input to get the underlying data.</p>
</li>
<li><p>Operate on the underlying data. (previously part of step 3)</p>
</li>
<li><p>Apply <code class="code">object_constructor</code> or <code class="code">morphism_constructor</code> to the underlying data to get an object or a morphism in the reinterpretation <code class="code">R</code>. (previously step 5)</p>
</li>
</ol>
<p>This is exactly what a primitive implementation would look like. Thus, in many cases compiling a reinterpretation immediately gives a primitive implementation with no remaining references to the tower <code class="code">cat_n</code>.</p>
<p>Reinterprets a category <var class="Arg">category</var> (the "modeling category") to form a new category <code class="code">R</code> (the "reinterpretation") subject to the options given via <var class="Arg">options</var>, which is a record with the following keys:</p>
<ul>
<li><p><code class="code">name</code>: the name of the reinterpretation <code class="code">R</code>,</p>
</li>
<li><p><code class="code">category_filter</code>, <code class="code">category_object_filter</code>, <code class="code">category_morphism_filter</code>, <code class="code">object_datum_type</code>, <code class="code">morphism_datum_type</code>, <code class="code">object_constructor</code>, <code class="code">object_datum</code>, <code class="code">morphism_constructor</code>, <code class="code">morphism_datum</code>: same meaning as for <code class="func">CategoryConstructor</code> (<a href="chap11.html#X8070F8B48111E8A7"><span class="RefLink">11.2-1</span></a>), which is used to create the reinterpretation <code class="code">R</code>,</p>
</li>
<li><p><code class="code">modeling_tower_object_constructor</code>: a function which gets the reinterpretation <code class="code">R</code> and an object datum (in the sense of <code class="code">object_datum</code>) and returns the corresponding modeling object in the modeling category,</p>
</li>
<li><p><code class="code">modeling_tower_object_datum</code>: a function which gets the reinterpretation <code class="code">R</code> and an object in the modeling category and returns the corresponding object datum (in the sense of <code class="code">object_datum</code>),</p>
</li>
<li><p><code class="code">modeling_tower_morphism_constructor</code>: a function which gets the reinterpretation <code class="code">R</code>, a source in the modeling category, a morphism datum (in the sense of <code class="code">morphism_datum</code>), and a range in the modeling category and returns the corresponding modeling morphism in the modeling category,</p>
</li>
<li><p><code class="code">modeling_tower_morphism_datum</code>: a function which gets the reinterpretation <code class="code">R</code> and a morphism in the modeling category and returns the corresponding morphism datum (in the sense of <code class="code">morphism_datum</code>),</p>
</li>
<li><p><code class="code">only_primitive_operations</code> (optional, default <code class="code">false</code>): whether to only reinterpret primitive operations or all operations.</p>
<p>Returns the functor from the modeling category <code class="code">ModelingCategory</code>(<var class="Arg">R</var>) to the reinterpretation <var class="Arg">R</var> which maps each object/morphism to its reinterpretation.</p>
<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ModelingObject</code>( <var class="Arg">R</var>, <var class="Arg">obj</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a CAP category object</p>
<p>Returns the object in <code class="code">ModelingCategory</code>(<var class="Arg">R</var>) modeling the object <var class="Arg">obj</var> in the reinterpretation <var class="Arg">R</var>.</p>
<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ReinterpretationOfObject</code>( <var class="Arg">R</var>, <var class="Arg">obj</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a CAP category object</p>
<p>Returns the reinterpretation in <code class="code">R</code> of an object <var class="Arg">obj</var> in <code class="code">ModelingCategory</code>(<var class="Arg">R</var>).</p>
<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ModelingMorphism</code>( <var class="Arg">R</var>, <var class="Arg">mor</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a CAP category morphism</p>
<p>Returns the morphism in <code class="code">ModelingCategory</code>(<var class="Arg">R</var>) modeling the morphism <var class="Arg">mor</var> in the reinterpretation <var class="Arg">R</var>.</p>
<p>Returns the reinterpretation in <code class="code">R</code> with given source and range in <codeclass="code">R</code> of a morphism <var class="Arg">mor</var> in <code class="code">ModelingCategory</code>(<var class="Arg">R</var>).</p>
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
