Dependency relationships:
A preorder can be considered as defining a system of relationships of dependencies between entities. These relationships are always transitive because if $A$ is dependent upon $B$ and $B$ is dependent upon $C$ then $A$ is dependent upon $C$. An example of a dependency ordering relationship like this, is the hierarchy of dependencies of files in a computer program.
Preorders are also used to model dependencies of events. In a familial preorder, a person is dependent upon his parents, who are dependent upon their parents and so on. In general, the events in spacetime are modeled by causal dependencies, so that each event is dependent upon its causes. Considering preorders as relationships of dependencies produces a slight change of perspective.
Functional dependencies:
If a preorder $P$ on a set $S$ models how the elements in the set are dependent upon one another, then a set-valued functor $F: P \to Sets$ can be considered to be a model of functional dependencies. The dependency on element upon another is associated with a function with realises the dependency. \[ F : P \to Sets \] There is another sense in functional dependencies appear: in the theory of relations. Functional dependencies are preorders on the sets of indices of relations. These functional dependencies in $\wp(I)^2$ have the following axioms:
- Reflexivity: if $A \subseteq B$ then $B \to A$
- Transitivity: if $A \to B$ and $B \to C$ then $A \to C$
- Composition: if $A \to C$ and $B \to D$ then $A \cup B \to C \cup D$
Definition. let $R$ be a relation consisting of functions $I \to X$ then $S$ functionally determines $T$ provided that $\forall a,b \in R: a|_S = b|_S \Rightarrow a|_T = b|_T$.
This naturally produces a functional dependency relationship from a relation $R$. As these functional dependencies are thin categories, we can produce set-valued functors over them that how one variable determines another.
Set-valued functors from functional dependencies:
A set valued functor has two parts: an object function and a morphism function. To begin with, we define the object part of the set-valued functor. Let $R$ be a relation defined by a family of functions of the form $I \to X$.
Definition. let $S \subseteq I$ then the underlying set of $S$ is the image of the restriction function $|_S : Hom(I,X) \to Hom(S,X)$.
Definition. let $S,T \subseteq I$ such that $S \to T$ then the underlying function $f_{(S,T)} : Hom(S,X) \to Hom(T,X)$ is the function which takes $l \in Hom(S,X)$ and then it finds an edge $E$ in $R$ that has $E_S = l$ and produces from it its restriction $E_T$.
By combining these two components: the underlying set of an object and the underlying function of an edge, we can get a set-valued functor from functional dependencies: \[ F : P \to Sets \] If we have $A \to B$ and $B \to C$ as functional dependencies, then $F_{(A,C)} = F_{(A,B)} \circ F_{(B,C)}$. In either case, the function determines the restriction to $C$ from the restriction to $A$, the later just does it through an intermediary. So $F$ is a functor determined by the relation $R$.
Restriction presheaf:
The condition of reflexivity means that $A \subseteq B$ means that $B \to A$. So a set of values in an association functionally determines its parts. This determines a contravariant functor from a partially ordered family of sets of indices. \[ F : C^{op} \to Sets \] Although we can often produce interesting set-valued functors from functional dependencies on relations, the restriction presheaf is something we can produce for any relation. This applies to any family of sets, partially ordered by inclusion. It is helpful to add other extra conditions, like that the family of sets is a topology in order to define the gluing axiom of sheaves.
Underlying relations of some set-valued functors
We saw previously that we can get set-valued functors to describe the functional dependencies of some relations. We can also apply this process in the reverse direction to get the underlying relations of some set-valued functor. Let $P$ be a finite preorder and $F : P \to Sets$ a set-valued functor.
Definition. let $A_1,...A_n$ be the objects of $P$ then define the relation $R$ of $F$ to be the relation in $F(A_1) ... F(A_n)$ that has $E \in R$ provided that $\forall m: A_i \to A_o \in Arrows(P)$ with $F(m) : F(A_i) \to F(A_o)$ we have that $E_o = F(m)(E_i)$.
The relation simply consists of tuples of elements of the underlying sets of the objects of the preorder, such that the relation satisfies all the functional dependencies of the set-valued functor.
Example. the underlying binary relation of a function $f$ consists of all ordered pairs $(a,b)$ with $b = f(a)$. It fully determines the function up to image.
The underlying binary relation can be empty. Consider a set-valued functor from the cospan category $F : [2,1] \to Sets$. Then the fiber product of the two functions determined by the cospan functor could be empty, in which case the underlying relation is empty. Thus, the underlying relation doesn't fully determine the set-valued functor. There is one special case though for which this is the case.
Topoi of equivalence relations:
An equivalence relation $E$ can be presented as a thin groupoid. Then by this presentation, $Sets^E$ is a topos. As the topos of a groupoid, this topos is boolean. So this is a special case of a topos of set-valued functors, for which the set-valued functors are determined by relations.
Proposition. let $E$ be an equivalence relation. Then $Sets^E$ is a boolean topos.
The topoi that emerge from equivalence relations are boolean, and so they can truly be presented as sets. In particular, they can be considered to be special cases of relations. Let $E$ be a complete equivalence relation of order $n$, then $Sets^E$ can be considered to be a topos of $F: E \to Sets$ functors. These functors are fully detremined by one-to-one-to-one-to... relations.
The topos $Sets^{K_2}$, the topos of bijections, is fully determined by one to one relations. The subobjects in the topos of bijections are equivalente to subsets of the one to one relation. Then $Sets^{K_3}$ consists of one-to-one-to-one relations and subobjects are subsets of these relations. $Sets^{K_4}$ consists of one-to-one-to-one-to-one relations and so on. The distinguishing property of these relations is their complete set of functional dependencies.
The topos of functions $Sets^{T_2}$ is the smallest non-boolean topoi of a preorder. The reason that it is not boolean and equivalently the reason it is not fully determined by its underlying relation is that functions have images. While it is true that set-valued functors on preorders can typically be considered to be functional dependencies on relations, this is not always strictly the case because of the images of functions.
For example, consider a functor in the topos $Sets^{T_3}$ which takes the form $F : T_3 \to Sets$ then this is a pair of functions $f : A \to B$ and $g : B \to C$. If the function $f$ is not surjective, then there are pairs in $g$ that can never be recovered by the relation $A \times B \times C$.
A set-valued functor on a finite total order is fully determined by its relation, only provided that each of its function is surjective. We can therefore say that set-valued functors on preorders are related to the functional dependencies on relations, but they are not always determined by them such as when their output functions are not all surjective.
Set-valued span functors:
A span functor has signature $F: [1,2] \to Sets$. The index preorder of this functor is a height two lower tree, so by generalization we can consider any functor $F: [1,n] \to Sets$ that has its origin a height two lower tree partial order.
Then $F$ is essentially a product of functions on its initial index set. In the case of $[1,2]$ we have two functions $f : A \to B$ and $A \to C$ that can be expressed as a product $A \to B \times C$. This determines a ternary relation $(a,b,c)$ with $f(a) = b$ and $g(a) = c$. So these kind of set-valued functors are very much related to their underlying relations.
In order to address the lack of surjectivity, these relations can be considered by embedded relations and the parent sets the relation is embedded in, including elements not in their image can be determined by the embedding. So these functors can determined by their relations up to an embedding.
Fundamental topoi:
The fundamental topoi: the topos of sets, the topos of functions, the topos of bijections, etc can be considered to be determined by systems of functional dependencies. The distinction between the topos of functions and the topos of bijections is that the later has more functional dependencies. These additional functional dependencies determine different categorical logics as well as subobject and quotient lattices.
Perspective on set-valued functors:
The set-valued functors on preorders can be considered to be systems of functional dependencies, but these don't always correspond to the functional dependencies on relations especially if the preorder is not an equivalence relation. The distinction between functional dependencies of relations and set-valued functors on preorders arises because of the images of functions.
Functional logic synthesis:
The role of topoi theory is that it unifies logic and functions. It does this by providing a common language for dealing with sets and functions, provided by their topoi: $Sets$ and $Sets^{\to}$. Topoi theory can therefore serve as the foundations of functional logic programming.
Traditionally, sets and functions are treated separately in logic programming and functional programming languages. The topos perspective suggests that there is no reason that we cannot logic programming and functional programming techniques: after all predicates and functions are merely different types of topos objects.
Implementation of relations in functional logic programming languages:
A relation in a functional logic programming language can be defined by the combination of a computable predicate function and a set-valued functor determining its functional dependencies. The set-valued functor can be used to help complete terms of the relation.
Alternatively, a function can be defined by a set-valued functor and a relation can be defined from it by its set of ordered pairs. As a result, the functional approach and the logical approach can ultimately arrive at the same result in a system based upon topos theory.
See also:
[1] Topoi from preorders
References:
[1] Armstrong's axioms:
No comments:
Post a Comment