Canonicality
Associated with every kind K is a full interpretation function [], read as “canonical”. Given a kind (instance) it returns the canonical form of that kind (instance). The canonical form of a canonical form is itself. If we have a term of the form [k] = l we call the asset l the canonical kind of k. Likewise, for instances, we use the term canonical instance. When we do not distinguish kind or instance, we say canonical realization or canonical asset. Canonicality preserves all structure of its domain and, since the codomain is generative (it is constructed entirely by the canonicality operation), then it can have no new structure. This means that it is possible to define a full interpretation between any two canonically equivalent assets, but not necessary that such interpretations exist. Thus, canonicality induces an equivalence relation; interpretations do not. Rewriting logic embedded in a type system are used in [18] to define and compute canonical forms of kinds and instances. All operations within kind theory but for resolution are deterministic due to the fact that that their operational semantics are Church-Rosser. Resolution is defined in general rewriting logic and is both undecidable and NP-hard, but in all the common cases that we have explored in the actual use of resolution in practice are tractable and decidable1
|
