The Information Flow Framework (iff)

Download 475 b.
Hajmi475 b.

The Information Flow Framework (IFF)

  • Robert E. Kent

Peirce Quotation

Table of Contents

  • Part 0. Introduction to the IFF

    • What is an Ontology?
      • (definition)
      • (dictionaries)
      • (distinctions)
    • The SUO-IFF Project
    • Origins and Influences
    • The Categorical Manifesto
    • IFF Design Guidelines
    • IFF Development Phases
      • Principle of Conceptual Warrant
      • Principle of Categorical Design
  • Part I. The IFF Metatheory

    • The IFF Architecture
      • (old version)
      • (new version)
      • The IFF Metastack
      • Four Fundamental Relations
    • The IFF Code
      • The IFF (meta) Ontologies
      • Some Example IFF Terms
      • The Basic IFF Terms
    • The IFF Metalanguages
      • (old version)
      • (new version)

Part 0. Introduction to the IFF

  • What is an Ontology?

    • (definition)
    • (dictionaries)
    • (distinctions)
  • The SUO-IFF Project

  • Origins and Influences

  • The Categorical Manifesto

  • IFF Design Guidelines

  • IFF Development Phases

    • Principle of Conceptual Warrant
    • Principle of Categorical Design

What is an Ontology? (definition)

  • Example. Consider the e-commerce example (Figure 1) of a schema (ontology).

    • concepts are represented as nodes,
    • relationships are represented as edges,
    • constraints are represented as parallel pairs of edge paths, limits and coproducts.

What is an Ontology? (dictionaries)

  • Dictionaries and Ontologies.

  • An ontology is similar to a dictionary, but has greater detail and structure. In the IFF there is a strong analogy between dictionaries and meta-ontologies.

    • Builders. There is a correspondence between the builders of dictionaries and those of meta-ontologies. Corresponding to the lexicographers, who create dictionaries, are the ontologicians (mathematicians, particularly category-theorists) who create meta-ontologies.
    • Source material. There is a correspondence between the source material used by dictionaries and that used by meta-ontologies. The entries placed and described in dictionaries have three sources:
      • terms borrowed from other dictionaries,
      • new terms used to express concepts in works of literature, and
      • new terms used to express concepts in everyday speech.
    • By analogy, the concepts axiomatized in meta-ontologies originate from three sources:
      • terms borrowed from other meta-ontologies,
      • new metalevel terms used to express concepts in object-level ontologies, and
      • new metalevel terms used to express the conceptual structure of a community.
    • For both dictionaries and ontologies, the second source is most important.
    • Source creators. There is a correspondence between the source creators used by dictionaries and those used by meta-ontologies. Corresponding to the literary figures who originate new terms in works of literature are the knowledge engineers who originate and use new metalevel terms in object-level ontologies.

What is an Ontology? (distinctions)

  • The object/meta distinction.

    • An object-level ontology represents some aspect of the “real world”. We distinguish between populated and unpopulated ontologies.
      • Unpopulated ontologies have only type information [aka schemas or theories].
      • Populated ontologies have both type and instance information, plus the classification relationship between these two kinds of things [aka databases or logics].
    • A meta-level ontology is an ontology about ontologies. It represents some aspect of the organization of object-level ontologies.
  • The prescriptive/descriptive distinction.

    • Both dictionaries and ontologies come in two basic philosophies: prescriptive or descriptive. A descriptive dictionary or ontology describes actual usage. Most modern dictionaries are descriptive. The IFF is a descriptive metatheory, since it uses the constraint called “conceptual warrant”.
  • The monolithic/modular distinction.

    • The monolithic-modular distinction is important for the maintenance of object-level ontologies. A monolithic ontology is one-size-fits-all. The monolithic approach is not compatible with the need for continual revision and consistency checking. The modular approach, which advocates the lattice and category of theories constructions, is very compatible with these needs.

The SUO-IFF Project

Origins and Influences

The Categorical Manifesto

  • Mathematical Context (~ Category)

    • “To each species of mathematical structure, there corresponds a category whose objects have that structure, and whose morphisms preserve it.”
  • Passage (Construction) between Contexts (~ Functor)

    • “To any natural construction on structures of one species, yielding structures of another species, there corresponds a functor from the category of the first species to the category of the second.”
  • Generalized Inverse (~ Adjunction)

    • “To any canonical construction from one species of structure to another corresponds an adjunction between the corresponding categories.”
    • Two special cases:
      • Reflection: GF = IdB “G is rali to F” “B reflective subcategory A”
      • Coreflection: IdA = FGG is rari to F” “A coreflective subcategory B”
  • Sums, Quotients and Fusions (~ Colimit)

    • “Given a species of structure, say widgets, then the result of interconnecting a system of widgets to form a super-widget corresponds to taking the colimit of the diagram of widgets in which the morphisms show how they are interconnected.”

IFF Design Guidelines

  • In the development of the IFF, certain guidelines have proven to be very important.

  • Goal. The IFF metatheory was designed to represent first order logic, its languages, theories, model-theoretic structures and (local) logics, including satisfaction. This metatheory incorporates the theory of institutions of Goguen and Burstall.

  • Meta-guideline. Follow the intuitions of the working category-theorist. Such intuitions represent naive category theory. The meaning of naive here is not pejorative. It means primitive, natural, intuitive, first-formed, primary, not evolved or elemental.

  • Practice. Initially formulate any IFF module as a set-theoretic axiomatization using a first order expression. Eventually, by eliminating quantifiers and logical connectives, move, morph or transform this set-theoretic axiomatization toward a category-theoretic axiomatization.

  • Rule-of-thumb. Keep it simple! From the foundational standpoint, this means that we start with no assumptions at all. However, in view of the Cantor diagonal argument, as a first step we assume a slender hierarchy called the IFF metastack.

IFF Development Phases

  • Phase 1: (2000-2001)

    • First ontology axiomatized: The IFF Category Theory (meta) Ontology (IFF-CAT).
    • A non-starter: a topos axiomatization. Objections due to its lack of warrant.
      • Warrant means evidence for or token of authorization.
      • Conceptual warrant is an adaptation of the librarianship notion of literary warrant.
  • Phase 2: (2001-2003)

    • Designed bottom-up; Require conceptual warrant; Follow categorical design principle.
    • Important metalogic concept incorporated: finite limits; for example, composition of class functions requires the pullback concept.
  • Phase 3: (2004-2006)

    • Central task: reorganization of the IFF metastack using "adjunctive axiomatization".
      • This will provide the metastack with better structure.
      • This will simplify the IFF-KIF meta-language core by not requiring the definite descriptive operator.
    • Important metalogic concept incorporated: exponents.
    • Fibrations and indexed categories will also be central.
    • Institutions will be fully axiomatized.
  • Principles. During the IFF development, four concepts have eventually emerged as important. One of these concepts, the IFF metastack, is discussed elsewhere. The other three concepts are principles for IFF development. In chronological order these are

    • the principle of conceptual warrant,
    • the principle of categorical design and
    • the principle of institutional logic.
  • Conceptual warrant restricts the introduction of upper metalevel terminology, whereas categorical design forces the introduction of this terminology, principally in the core.

The Principle of Conceptual Warrant

  • Principle: All IFF terminology should require conceptual warrant for their existence: any term that appears in (and is axiomatized by) a metalanguage should reference a concept needed in a lower metalevel or object level axiomatization.

  • Note: The terminology appearing in any standardization meta-ontology will exert authority. Because of this, in selecting which terminology to specify in the IFF, we utilize the notion of “conceptual warrant”. Warrant means evidence for, or token of, authorization.

  • Analogue: Conceptual warrant is an adaptation of the librarianship notion of literary warrant. According to the Library of Congress, its collections serve as the literary warrant (i.e., the literature on which the controlled vocabulary is based) for the Library of Congress subject headings system. In the same fashion, the object-level (n = 0) and lower metalevel (n = 1) terminology of the IFF serves as the conceptual warrant for the IFF upper metalevel (n = 2) axiomatization.

The Principle of Categorical Design

  • Principle: The design of a module at any particular metalevel should adhere to the property that its axiomatic representation is strictly category-theoretic:

    • All axioms use terms from the metalanguage at that metalevel.
    • All axioms are atomic: no axioms use explicit logical notation; no variables, quantification (‘forall’, ‘exists’) or logical connectives (‘and’, ‘or’, ‘not’, ‘implies’,‘iff’) are used.
  • Note: The peripheral (non-core) modules in the lower IFF metalevel (n = 1) have the tripartite form: outer category namespace, inner object and morphism namespaces.

    • Currently, the outer namespace follows the categorical design principle exactly.
    • And the inner namespaces follow it to a great extent (80–90%).

Part I. The IFF Metatheory

  • The IFF Architecture

    • (old version)
    • (new version)
    • The IFF Metastack
    • Four Fundamental Relations
  • The IFF Code

    • IFF (meta) Ontologies
    • Some Example IFF Terms
    • The Basic IFF Terms
  • The IFF Metalanguages

    • (old version)
    • (new version)

The IFF Architecture (old version)

The IFF Architecture (new version)

The IFF Metastack

  • There are axiomatizations for categories, finite (and general) limits/colimits, exponents and subobject classifiers.

  • The IFF metastack represents the chain of categories (toposes)

  • Set1  Set2  Set3  ...  Setn  ...  Set

Four Fundamental Relations

  • The chain of categories (toposes)

    • Set1  Set2  …  Setn  …  Set
  • are axiomatized in the IFF Core (meta) Ontology (IFF-CORE).

  • These inclusions represent the fact that axiomatization at level n includes specialization of the axiomatization at level n+1.

  • Specialization (technical term) means the exact adaptation of the core terminology and axiomatization at level n+1 to level n by use of four fundamental relations: subset, (function) (optimal-)restriction and (relation) abridgment (plus intersection).

IFF (meta) Ontologies

Some Example IFF Terms

The Basic IFF Terms

The IFF Metalanguages (old version)

  • Each metalevel has an associated metalanguage

    • It contains the metalanguage directly above it.
    • Its terminology is defined by the meta-ontologies at that level.
    • It is used to axiomatize the (meta-)ontologies at all lower levels.
  • Introductions

    • IFF-Ur – axiomatization for categories
    • IFF-Top – axiomatization for finite limits
    • IFF-Upper – axiomatization for exponents and finite colimits
    • IFF-Lower – axiomatization for subobjects and general limits/colimits
  • IFF-KIF enables lisp-like first-order expression: functions, binary relations, connectives and quantifiers. Uses restricted quantification.

The IFF Metalanguages (new version)

  • Each metalevel has an associated metalanguage

    • It contains the metalanguage directly above it.
    • Its terminology is defined by the meta-ontologies at that level.
    • It is used to axiomatize the (meta-)ontologies at all lower levels.
  • IFF metashell

    • Logical part: enables lisp-like first-order expression: sets, unary functions, binary relations, connectives and quantifiers. Uses restricted quantification with guards and definite description.
    • Mathematical part: (IFF-META namespace) meta-terminology allowing IFF-CORE to conform to the principle of categorical design.
  • IFF meta-ur & IFF meta-n: (IFF-CORE ontology) introduces axiomatization for toposes; that is, for categories, finite limits/colimits, exponents, subobjects and general limits/colimits

Part II. The IFF Institutional Application

  • Two IFF Efforts to Represent FOL

    • The IFF-ONT
      • (old version)
      • (new version)
    • The IFF-FOL
  • Logical Environments

    • Languages
      • Language Expressions
      • Language Colimits
    • Models
    • Theories
      • The Category of Theories
      • Theory Colimits (fusion)
    • Truth Classification & Truth Concept Lattice
    • Truth Concept Lattice Functionality
  • Institutions

    • The Grothendieck Construction
    • The Truthful Connection

Two IFF Efforts to Represent FOL

  • Non-Traditional FOL

    • The IFF Ontology (meta) Ontology (IFF-ONT)
      • old version
      • new version
  • Traditional FOL

    • The IFF First Order Logic (meta) Ontology (IFF-FOL)

The IFF Ontology (meta) Ontology (IFF-ONT) (old version)

  • Nontraditional.

  • Home page:

  • Based on view that n-ary relations incorporate a notion of hypergraphs.

  • Also, novel definition of models via classifications: t | r instead of r(t).

  • Completely axiomatized: Language, Theory, Model and Logic.

  • Language and Theory are cocomplete.

  • Free models and logics exist.

  • Models are nonstandard: they have a subset of abstract tuples.

  • Problem:

    • Model fiber functions must be restricted to bijective variable functions.
    • Must limit Language and Theory to corresponding subcategories Language≐ and Theory≐
    • Language≐ (hence, Theory≐) is not cocomplete; in fact, does not have coproducts.
    • Analysis: reference (sort) function is too inflexible (Note: such a sort function is recommended in Enderton's text!).

The IFF Ontology (meta) Ontology (IFF-ONT) (new version)

  • Traditional.

  • Discussion and links at

  • Still based on view that n-ary relations incorporate a notion of hypergraphs.

  • In fact, identifies languages with hypergraphs (of a certain kind).

  • This kind of hypergraph does not use a reference (sort) function.

  • Languages (hence, theories) are cocomplete.

  • Model fiber function exists.

  • Special advantage: hypergraphs are equivalent to spangraphs.

    • Spangraphs are a more flexible definition of logical language (in terms of relational arity).
    • Spangraphs nicely model the SCL "role-set syntax", where arguments form a set of role-value pairs.
    • Example: ‘(Married (role-set: (wife Jill) (husband Jack)))’
    • This notion has been advocated in SCL development by Pat Hayes. Position and argument order are not needed. According to Hayes, this provides some insurance against communication errors.

The IFF First Order Logic (meta) Ontology (IFF-FOL)

Logical Environments

  • Distinctions

    • Potential versus actual
    • Formal versus interpretive
  • Four Fundamental Notions

    • Language
      • basic formalism
    • Theory
    • Model
      • actual or interpretive semantics
    • Logic
      • combined semantics


  • We assume that each language has an adequate, possibly denumerable, set of variables X. This generalizes the usual case where sequences are used – the advantage for this generality is elimination of the dependency on sequences and natural numbers. Cardinal numbers represent a skeletal quotient.

  • A language L = rel(L), ent(L), arity(L), sign(L):

    • a relation type set rel(L),
    • an entity type set ent(L),
    • a reference set pair L = refer(L) = Xent(L),
    • an arity function L = arity(L) = sign(L) · tuple-arity(L) : rel(L)  X, and
    • a signature function L = sign(L) : rel(L)  tuple(refer(L)).
    • For any relation type ρ  rel(L)
    • arity(L)(ρ) = {x, x, … xn  X is its arity with external form ρ, x, x, … xn,
    • L(ρ) : arity(L)(ρ)  ent(L) is its signature with external form ρ, x : ε, x : ε, … xn : εn,
    • where L(ρ)(xk) = εk for  < k < n.

Language Expressions

  • Associated with any language L = ent(L), rel(L), L, L, L is an expression language expr(L) = ent(L), rel(expr(L)), L, expr(L), expr(L) that extends L.

    • The set of entity types and the reference set pair of expr(L) are the same as L.
    • The relation types of expr(L) are L-expressions. The set rel(expr(L)) of L-expressions is inductively defined on relation types rel(L) using the logical quantifiers and connectives.
    • The arity and signature functions
      • expr(L) = arity(expr(L)) : rel(expr(L))  X
      • expr(L) = sign(expr(L)) : rel(expr(L))  tuple(refer(L))
    • are recursively-defined extensions from the relation types of L to the expressions of L. Sentences are expressions with empty arity .
  • Associated with any language morphism f = rel(f), ent(f) : L  L is an expression language morphism expr(f) = rel(expr(f)), ent(f) : expr(L)  expr(L) that extends f.

    • The entity type function is identity.
    • The relation function rel(f) : rel(L)  rel(L) is recursively extended to an expression function rel(expr(f)) : rel(expr(L))  rel(expr(L)).
  • There is a language morphism L = embed(L) L  expr(L) that embeds any language into its associated expression language.

    • The entity function is the identity.
    • The relation function rel(L) rel(L)  rel(expr(L)) embeds relation types as expressions.
  • There is a language morphism L = collapse(L) expr(expr(L))  expr(L) that collapses the expression of expression language of any language into its expression language.

    • The entity function is identity.
    • The relation function rel(L) rel(expr(expr(L)))  rel(expr(L)) collapses expressions.

Language Colimits

  • Language colimits are important:

    • they are the basis for theory colimits.
  • They involve two opposed processes:

    •  “summing” “keeping things apart” “preserving distinctness”
    •  “quotienting” “putting things together” “identification” “synonymy”
  • The “things” involved here are symbols:

    • relation type symbols
    • entity type symbols
    • and the concepts they denote.


  • A model M is a product of a language (= hypergraph) and a classification.

    • rel(M) is a relation classification; instances are abstract “tuples”.
    • ent(M) is an entity classification; types are “sorts”. Entity types are unary relation types.
    • The type aspect typ(M) = typ(rel(M)), typ(ent(M)), arity(M), sign(M) is a language.
    • The instance aspect inst(M) is a hypergraph.
  • This approach is comparable to the structure of Aristotle's ontological framework.

    • The two distinctions in Aristotle's ontological framework of “universal versus particular” and of “quality versus substance” are analogous to the two distinctions in the semantic architecture of the IFF between “type versus instance” and “relation versus entity”.
  • There is a type functor from models to languages typ : Model  Language.

  • There is a model functor from languages to classes mod = typ : Language  SET.

    • For fixed language L we denote by mod(L) the class of models of that type.
    • For any language morphism f : LL, we can define a model fiber function
    • mod(f) : mod(L)  mod(L).
    • There is a satisfaction relation
      • M |L
    • between models Mmod(L) and expressions   expr(L) (hence, sentences).


  • A theory T = base(T) axm(T) consists of an underlying language L = base(T) and a set of sentences axm(T)  sen(L) called the axioms of T. Theories represents formal or axiomatic semantics. We assume a fixed common variable set X for all languages.

    • An L-model M is a model of the theory T, denoted M |LT, when M satisfies each axiom   axm(T); that is, when M |L  for all axioms   axm(T).
    • A theory T entails a sentence   sen(L) when M |LT implies M |L for any model M. Such a sentence is called a theorem of T. Any axiom is a theorem. The set of theorems of T is denoted by thm(T). The theory clo(T) = T = L, thm(T) is called the closure of T. A theory is closed when it equals its closure.
    • Two theories T and T are compatible when they share the same type language: base(T) = base(T). A theory T is a specialization of a compatible theory T when T entails every theorem of T; that is, when thm(T)  thm(T). Then we also say that T is a generalization of T, and denote this by T  T. This is a preorder on theories over L – any theory T is equivalent to its closure Tclo(T).

The Category of Theories

  • Contexts:

    • Theory
    • Closed Theory
    • Language

Theory Colimits (Fusion)

  • Informally, identify the theories to be used in the construction.

  • Alignment: Formally, create a diagram of theories T of shape (indexing) graph G that indicates this selection. This diagram of theories is transient, since it will be used only for this computation. Other diagrams could be used for other fusion constructions.

Truth Classification & Truth Concept Lattice

  • Truth classification of 1st-order language L

    • Instances are L-models.
    • Types are L-sentences.
    • Incidence is satisfaction: M |=  when  is true in M.
  • Truth concept lattice of L

    • In the IFF approach, this is the appropriate
    • “lattice of ontological theories.”
    • Formal concept is a pair c = ext(c), int(c) where:
      • The int(c) is a closed theory (set of sentences).
      • The ext(c) is the collection of all models for that theory.
    • Lattice order is the opposite of theory inclusion.
    • The join or supremum of two theories is the intersection of the theories.
    • The meet or infimum of two theories is the theory of the common models.
    • Both L-models and L-sentences generate formal truth concepts (theories).
      • An object concept is the theory of a model.
      • An attribute concept is the models of a sentence.

Truth Concept Lattice Functionality


  • I = Sign, Mod, Sen, ⊨

  • Sign: an abstract category of signatures .

  • Sen : Sign  Set: a sentence functor indexing abstract sentences Sen() by signatures .

  • Mod : Sign  SETop: a model functor indexing abstract models Mod() by signatures .

  • |  Mod()Sen(): a signature parameterized satisfaction relation.

  • Satisfaction Condition (expresses the invariance of truth under change of notation): For any signature morphism f :  ', any '-model M' and any -sentence e,

  • M' |' Sen(f)(e) iff Mod(f)(M') | e.

  • Spec : Sign  Set: a specification functor indexing abstract theories (specifications) Spec() by signatures . A -specification is a set of -sentences.

  • I : Sign  CLSN: a classification functor is a concise definition of an institution. But CLSNCLG.

  • Î : Sign  CLG: a concept lattice functor is an alternate definition of an institution.

  • Example institutions

    • first order logic (with first order structures as models)
    • many sorted equational logic (with abstract algebras as models)
    • Horn clause logic
    • variants of higher order and of modal logic

The Grothendieck Construction

The Truthful Connection


  • The IFF is a descriptive category metatheory whose architecture contains nested metalanguages.

  • The main institutional application of the IFF is axiomatized in the Ontology (meta) Ontology (IFF-ONT) and the First Order Logic (meta) Ontology (IFF-FOL). These form flexible and general institutions for first order logic.

  • Institutions formally express semantic integration as an ontological fusion process. Each community represents their conceptual space in their own terms, and connects with others via morphisms that enable ontological alignment specification.

  • Institutions represent logical environments and institution morphisms connect logical environments. Amongst other things, the IFF is in the process of axiomatizing the theory of institutions.


  • What is an Ontology?

    • (other views)
    • (other views)
  • Language Morphisms

  • Language Sums

  • Language Endorelations

  • Language Quotients

  • Theory Morphisms

  • Theory Sums

  • Theory Endorelations and Quotients

What is an Ontology? (other views)

  • B. Chandrasekaran, Jorn R. Josephson, V. and Richard Benjamins.

    • "Ontological analysis clarifies the structure of knowledge. Given a domain, its ontology forms the heart of any system of knowledge representation for that domain. Without ontologies, or the conceptualizations that underlie knowledge, there cannot be a vocabulary for representing knowledge …. Second, ontologies enable knowledge sharing."
  • Tom Gruber.

    • "An ontology is an explicit specification of a conceptualization. The term is borrowed from philosophy, where an ontology is a systematic account of existence. For AI systems, what 'exists' is that which can be represented."
  • Jeff Heflin.

    • "An ontology defines the terms used to describe and represent an area of knowledge. Ontologies are used by people, databases, and applications that need to share domain information (a domain is just a specific subject area or area of knowledge, like medicine, tool manufacturing, real estate, automobile repair, financial management, etc.). Ontologies include computer-usable definitions of basic concepts in the domain and the relationships among them (note that here and throughout this document, definition is not used in the technical sense understood by logicians). They encode knowledge in a domain and also knowledge that spans domains. In this way, they make that knowledge reusable.... Ontologies are usually expressed in a logic-based language, so that detailed, accurate, consistent, sound, and meaningful distinctions can be made among the classes, properties, and relations."

What is an Ontology? (other views)

  • Christopher Welty.

    • "Ontology is a discipline of philosophy whose name dates back to 1613 and whose practice dates back to Aristotle. It is the science of what is, the kinds and structures of objects, properties, events, processes, and relations in every area of reality. … [W]hat the field of ontology research attempts to capture is a notion that is common to a number of disciplines: software engineering, databases, and AI to name but a few. In each of these areas, developers are faced with the problem of building an artifact that represents some portion of the world in a fashion that can be processed by a machine."
  • John F. Sowa.

    • "The subject of ontology is the study of the categories of things that exist or may exist in some domain. The product of such a study, called an ontology, is a catalog of the types of things that are assumed to exist in a domain of interest D from the perspective of a person who uses a language L for the purpose of talking about D."
  • Tim Berners-Less, James Hendler, and Ora Lassila.

    • "In philosophy, an ontology is a theory about the nature of existence, of what types of things exist; ontology as a discipline studies such theories. Artificial-intelligence and Web researchers have co-opted the term for their own jargon, and for them an ontology is a document or file that formally defines the relations among terms. The most typical kind of ontology for the Web has a taxonomy and a set of inference rules."
  • SUO WG.

    • "An ontology is similar to a dictionary or glossary, but with greater detail and structure that enables computers to process its content. An ontology consists of a set of concepts, axioms, and relationships that describe a domain of interest. … An upper ontology is limited to concepts that are meta, generic, abstract and philosophical, and therefore are general enough to address (at a high level) a broad range of domain areas."

Language Morphisms

  • A language morphism f = rel(f), ent(f) : L  L:

    • a relation type function rel(f) : rel(L)  rel(L), and
    • an entity type function ent(f) : ent(L)  ent(L).
    • These must preserve arity and signature:
    • preservation of arity:
    • rel(f) · arity(L) = arity(L)
    • L(rel(f)(ρ)) = var(f)(L(ρ)) for any relation type ρ  rel(L)
    • if ρ, x, x, … xn then rel(f)(ρ), x, x, … xn
    • preservation of signature:
    • rel(f) · sign(L) = sign(L) · tuple(refer(f))
    • L(rel(f)(ρ)) = tuple(refer(f))(L(ρ)) for any relation ρ  rel(L)
    • if ρ, x : ε, x : ε, … xn : εn then rel(f)(ρ), x : ent(f)(ε), … xn : ent(f)(εn)

Language Sums – “keeping things apart” 

  • Let L1 and L be two languages with common variable set X.

  • The sum language L1+L:

    • The relation type and entity type sets are the disjoint unions of their components
    • rel(L1+L) = rel(L1)+rel(L) and ent(L1+L) = ent(L1)+ent(L).
    • The variable set is the fixed set X, var(L1+L) = var(L1) = var(L) = X.
    • The arity function is the pairing
    • arityL1L = L1L = L1, L : rel(L1)rel(L) X
    • with L1L(1) = L1(1) for 1  rel(L1) and L1L() = L() for   rel(L).
    • The signature function is the pairing
    • signL1L = L1L = L1, L : rel(L1)rel(L)  tuple(refer(L1L))
    • with L1L(1) = L1(1) for 1  rel(L1) and L1L() = L() for   rel(L).
  • The sum injection language morphism in(L1) = inrel(L1)inent(L1) : L1  L1L:

    • The relation function is the disjoint union injection
    • inrel(L1rel(L1)  rel(L1L) = rel(L1)rel(L);
    • the entity function is the sum injection
    • inent(L1ent(L1)  ent(L1L) = ent(L1)ent(L).
  •  The sum L1+L is a coproduct in the category Language(X).

Language Endorelations

  • Let X be any set representing a fixed set of variables. Let endo(X) denote the class of all language endorelations at X.

  • A language endorelation is a triple J = lang(J), rel(J), ent(J) consisting of

    • a language lang(J) = L with variable set X,
    • a binary endorelation rel(J) = Rrel(L)rel(L) on relation types of L, and
    • a binary endorelation ent(J) = Eent(L)ent(L) on entity types of L.
  • These must satisfy the following constraints on arity and signature functions of L. Here R is the equivalence relation generated by rel(J) = R and E is the equivalence relation generated by ent(J) = E. For any pair of relation types ρ1, ρ2  rel(L), if (ρ, ρ)  rel(J) = R, then

    • arity(L)(ρ) = arity(L)(ρ) and sign(L)(ρ)  sign(L)(ρ),
  • where   sign(refer(L))sign(refer(L)) is the equivalence relation on tuples defined as follows: τ  τ when arity(refer(L))(τ) = arity(refer(L))(τ) and τ(x) E τ(x) for all x  arity(refer(L))(τ) = arity(refer(L))(τ).

  • Often, the endorelations rel(J) = R and ent(J) = E are equivalence relations on relation types and entity types. However, it is not only convenient but also very important not to require this. In particular, the endorelations defined by parallel pairs of language morphisms (coequalizer diagrams) do not have component equivalence relations. A simple inductive proof shows that the triple Ĵ = L, R, E is also a language endorelation.

Language Quotients – “putting things together” 

  • The quotient L/J of an endorelation J = LRE = lang(J), rel(J), ent(J) on a variable set X is the language defined as follows:

    • The set of relation types are the equivalence classes rel(L/J) = rel(L)/R.
    • The set of entity types are the equivalence classes ent(L/J) = ent(L)/E.
    • The set of variables is var(L/J) = var(L) = X.
    • The arity function L/J = arity(L/J) : rel(L)/R  X is defined pointwise: L/J(ρR) = L(ρ) for all relation types ρ  rel(L).
    • The signature function L/J = sign(L/J) : rel(L)/R  tuple(refer(L/J)) is defined pointwise: L/J(ρR)(x) = L(ρ)(x)E for all relation types ρ  rel(L) and variables x  L(ρ).
  • There is a canonical quotient language morphism

    • J = rel(J), ent(J) : L  L/J
  • whose relation type function is the canonical surjection

    • rel(J) = canon(rel(J)) =  R : rel(L)  rel(L)/R, and
  • whose entity type function is the canonical surjection

    • ent(J) = canon(ent(J)) =  E : ent(L)  ent(L)/E.
  • The fundamental property for this language morphism is trivial, given the definition of the quotient language above.

Theory Morphisms

  • Theories are related through theory morphisms.

  • A morphism of theories f : T  T is a language morphism f : L  L that maps source axioms to target theorems: sen(f)(axm(T))  thm(T). Then, a morphism of theories maps source theorems to target theorems: sen(f)(thm(T))  thm(T).

  • When the source and target share the same base language (they are compatible) and the base language morphism is the identity, a morphism of theories f : T  T is equivalent to a theory ordering T  T, which states that theory T generalizes theory T or theory T specializes theory T.

  • The composition and identities for theory morphisms are defined in terms of their base type language morphisms. Theories and theory morphisms form the category Theory.

Theory Sums

Theory Endorelations and Quotients

  • Given a theory T = base(T), axm(T), a theory endorelation J is a language endorelation J = ent(J), rel(J) over L = base(T) . Recall that J has an associated type language endorelation expr(J) = ent(J), expr(J) over expr(L).

  • The entity, relation and expression endorelations generate equivalence relations

    • E  ent(L)ent(L),
    • R  rel(L)rel(L), and
    • R*  expr(L)expr(L).
  • The set of expressions on the quotient base language is expr(T/J) = expr(L)/R*.

  • The quotient T/J = base(T/J), axm(T/J) of an endorelation J on a theory T has

    • base(T/J) = base(T)/base(J) , the quotient of the base language of the base endorelation,
    • axm(T/J) = φR*  φ  axm(T), the collection of equivalence classes of axioms of T.
  • There is a canonical quotient theory morphism J : T  T/J whose base is the canonical quotient type language morphism

    • base(J) = base(base(J)) : base(T)  base(T/J) = base(T)/base(J) .
  • This morphism clearly maps axioms of T to axioms of T/J.

Do'stlaringiz bilan baham:

Ma'lumotlar bazasi mualliflik huquqi bilan himoyalangan © 2017
ma'muriyatiga murojaat qiling