Structure

Kinds are described structurally using our logic in a number of ways using several core operators. Classification is covered with the inheritance operators < and <p; structural relationships are formalized using the inclusion operators _p and _, equivalence has several forms, P and l; realization, the relationship

between instances and kind, is formalized with the operators <r and:; composition is captured in several forms,, _, and _; and interpretation, the translation of kind to kind or instances to instances, is realized with the operators,!and.

 

Rules

Relevant Rules.

(Parent Interp*) (Fully Equiv*) (Partial Equiv*)

􀀀,L K,K,! L ` _ 􀀀 ` K <p L

􀀀 ` L K·K,! L = idL,_

􀀀 ` U P V

􀀀 ` [U] = [V ]

􀀀 ` U l V

􀀀 ` [V ] _ [U]

The most important rules of kind theory in the context of this paper are ummarized in Table 1. The gamma in these rules is an explicit context of sequents (kind theory sentences). _ is a list of arbitrary sentences, idL is the identity function on kind L, and the asterisk denotes that all of these rules are reversible

(that is, they are bijections).

The rule (Parent Interp*) states that, if an inheritance relationship exists between kinds, then two interpretations must also exist: one that takes the parent to the child, preserving all structure, and a right adjoint of that map that takes the child to the parent. This rule essentially subsumes the related notions of type

coercion, structural type checking, and classification.

The relationship between equivalence and canonicality is elucidated in the other two rules. First, two assets, that is, kinds or instances, are fully equivalent if and only if their canonical forms are identical.

Second, two assets are partially equivalent if their canonical forms are structurally contained—that is, one of them is part of the other.