Abstract
Meseguer's general
logics try to give an answer to the question of what is a logic? using
ideas from abstract model theory and category theory [3]. This is achieved by
extending further Dana Scott's definition of entailment system and combining it
with institutions of Goguen and
Burstall [1]. All the fundamental components of a logic like those of syntax,
entailment system, models, proof calculus and satisfaction are properly treated
in general logics. Our approach analyses general logic’s proof calculi using trees and is based on the result that
any graph is the homeomorphic image of a tree. The only well known proof of
this result makes use of topology and universal covering spaces [4]. This leads
to the main result of the paper in which we prove the existence of universal
coverings in the category of Meseguer general logic.
1.
Introduction
1.1
Categorical logic
We follow J. Lambek and P. Scott [2] in their
treatment of logical deduction. According to this, sentences are objects and
deductions are arrows in a category. This approach is rather syntactical than
semantical, is independent from logical valuations and is compatible with
Meseguer's general logics.
Deduction can be treated in terms of graphs and
categories according to Lambek and Scott. The objects of any graph can be
considered as formulas while the
arrows can be considered as deductions
or proofs. The associative law in
categories can be considered as a rule of
inference.
A deductive
system is a graph in which to each object A is associated an arrow 1a :
A ® A, the identity arrow, and to each pair of arrows f:
A ® B and g: B ® C is
associated an arrow gf: A ® C, the composition
of f with g. A category then , is a deductive system in which the following equations hold, for all f: A ® B, g: B ® C and h: C ® D:
f 1A = f = 1B f , (hg) f = h(gf)
1.2.
General Logics
General
logics try to provide a very general framework for defining already developed
logics including many sorted equational, first and second order logic, modal
logics etc.
This paper deals with systems of propositions in the context of general logics.
Meseguer's general
logics try to give an answer to the question of «what is a logic?» ,using
ideas from abstract model theory and category theory [3]. This is achieved by
extending further Dana Scott's definition of entailment system and combining it
with institutions of Goguen and Burstall [1]. All the fundamental components of
a logic like those of syntax, entailment system, models, proof calculus and
satisfaction are included in the definition of a (general) logic. General
logics try to provide a very general framework for defining already developed
logics including many sorted equational, first and second order logic, modal
logics etc.
1.2.1 Entailment systems
Entailment systems
is a categorical formalization of the
broad concept of (syntactical)
Logical context for theories . It relevance with the Information science is
that it can be used to formulate various requirement and specification systems
for the development of software of many different information systems . The
entailment system approach is invariant
of the choice of initial concepts (called signatures ) and of the way the propositions are composed ( category
of sentences ) .
Definition An entailment
system is a triple E = (Sign, sen, ÃÄ
) such that
Sign is a category whose objects are called signatures
sen:
Sign ®Set
is a functor associating
to each signature S
a corresponding set of S
- sentences, and
ÃÄ
is a function associating to each S Î |Sign| a binary relation ÃÄ
S Í P (sen(S))
´sen(S) called S - entailment such that the following properties are satisfied:
1. reflexivity: for any f
Îsen(S), {f} ÃÄ
S f
,
2. monotonicity:
if G ÃÄ S f
and G '
Ê G then G'ÃÄ
S f,
3. transitivity:
if G
ÃÄ S fi for all i Î I, and G È { fi | i ÎI} ÃÄ
S y, then
G
ÃÄ S y,
4. ÃÄ
- translation: if G
ÃÄ S f,
then for any H: S ® S' in Sign,
sen(H)(G)
ÃÄ S' sen(H)(f).
***
.The
category deductive system of an entailment system and an entailment system of a Deductive system
denoted by D(E)
: an arrow a:x->y belongs to
D(E) iff {x}ÃÄ
y
(and by RÃÄ(D(E)) the
entailement relation defined by a deduction system: We put
AÃÄ
a iff there is an arrow for some xÎA
.The A is a set of sentences of the
deductive system D(E) .
1.2.2 Institutions
Institutions is somehow a complementary approach relative to the entailement systems in
the sense that it formulates categorically the concept of semantical (model
theoretic ) Logical context for theories .
Definition An institution
is a 4-tuple I = (Sign, sen, Mod, ÆÍ)
such that
Sign is a category whose objects are
called signatures,
sen:
Sign ®
Set is a functor
associating to each signature S
a set of S-sentences,
Mod: Sign ®Catop is
a functor that gives for each signature S
a category whose objects
are called S-models, and
ÆÍ
is a function associating to each S
Î|Sign| a binary relation ÆÍS Í |Mod(S)| ´ sen(S)
called S-satisfaction satisfying the following satisfaction condition for each S
® S' in Sign: for
all M' Î|Mod(S)| and all f
Îsen(S),
M' ÆÍS' sen(H)(f) ÛMod(H)(M') ÆÍS' f.
1.2.3 Logics
Putting together both the categorical formulation of
syntactical and semantical (model theoretic ) Logical context ,namely entailement
systems and institutions we get the categorical formulation of Logical
context or general Logic :
Definition
A logic is a 5-tuple L = (Sign, sen,
Mod, ÃÄ
,ÆÍ
) such that:
(Sign, sen, ÃÄ)
is an entailment system,
(Sign, sen, Mod, ÆÍ)
is an institution,
and the following soundness
condition is satisfied: for any S Î|Sign|, G Í sen(S),
and f Îsen(S),
G
ÃÄS fÞ G ÆÍS f
where, by definition, the relation G ÆÍS f holds
if and only if M ÆÍS fholds
for any model M that satisfies all the sentences in G.
1.2.4
Map of entailment systems
Definition
Given two entailment
systems E = (Sign, sen, ÃÄ
) and E' = (Sign', sen', ÃÄ'
), a map of entailment systems (F,
a)
: E ® E' consists of a natural tranformation a: sen Þ sen' o F and
an a - sensible functor F:
Th0 ® Th0'satifying
the following property:
G ÃÄ S f Þ aS(G)
ÃÄ' F(S,Æ) aS(f).
1.3
Graphs and Free Categories
Every category C determines a graph UC that has the
same objects and arrows as the category. Every functor F: C ® C' is also a
morphism UF: UC ® UC' between the corresponding graphs. Using the above
we can define the forgetful functor U:
Cat ® Grph, from small categories to small graphs.
Let O be a
fixed set. An O - graph G is a graph
with O as its set of objects. Any O-graph G may be
used to generate a category C on O. The arrows of this category will be the
strings of composable arrows of G, so that an arrow of C from b to a may be
pictured as a path from b to a consisting of succesive edges of G. This
category C will be written C = C(G) and is called the free category generated by the graph G.
In the previous definition the concept of graph is actually
that of the oriented graph.If we want the concepts of non-oriented praph then
we defined it as following :
Definition
A non-oriented
graph H consists of a set X=vertH ,a set Y=egdeH and two maps Y®XxX
y®(o(y),t(y))
(o(y) for origin of y and t(y) for terminal of y) and Y®Y y® which satisfy the following condition: for each yÎY
we have , y¹and o(y)=t().
We remark that although we define the set of edges as
oriented edges (arrows) as we give always each
edge with both directions the result is the non-oriented graph the
definition .
Given an (oriented graph) it is always possible to add
with every oriented edge (arrow) the one with oposite direction and to get the
definition of non-oriented graph as before .This non-oriented graph we call non-oriented version (or corresponding
non-oriented ) of the given graph .
2.
Topological prerequisites
For the definitions of the previous terms see [9
Munkres] pp 155 ,pp 161,pp 393.
Except of the basic concept of the topological space
we require also the concepts of covering
map ,covering space ,homotopy and fundamental
group .
Given a topological space X , a path
in X from x to y is a continuous map
f:[a,b] ®X of some closed
real interval into X ,such that f(a)=x and f(b)=y .A space X is said to
be path connected if every pair of
points of X can be joined by a path in X .
If f is a path in X from x to y ,and g is a path in X
from y to z we define the composition
f*g of f and g to be the path h given by the equations
h(s)={f(2s)
for sÎ[0,1/2] and g(2s-1) for sÎ[1/2, 1]
Definition
Let X be a space ; let xo
be a point of X .A path in X that
begins and ends at xo is called loop
based at xo . The set of
path homotopy classes of loops based at xo
,with the operation * (of composition of representatives of homotopic classes paths ,[f]*[g]=[f*g] ) ,
is called the fundamental group ( or first homotopy group ) of X relative to
the base point xo It is denoted by p1(X,
xo) .
Example
For a detailed
definition of the fundamental
group see again the same book [Munkress] pp 326.
We shall not enlarge on the definition of a path
homotopy class but we shall mention that an honotopy transformation of a path
is a continuous transformation of it that fixes the end points and is
realizable in a continuous way inside the topological space.
Definition
A space X is said to be simply connected if it is
path-connected space (that is any two
points can be connected with a continuous path ) and if p1(X,
xo) is the trivial (one-element) group for some xoÎX ,and hence for every xoÎX .
A topological space B is said to be semilocally path connected if every
point b of B has a neighborhood V such that the homomorphism of p1(V,b)
into p1(B,b)
induced by inclusion is trivial.
A topological space B is said to be locally path connected at x if for
every neighborhood U of x ,there is a path-connected neighborhood V of x
contained in U .If B is locally path
connected at each of its points ,then it is said to be locally path connected .
For a detailed
definition of covering map and universal covering space see [Munkress] pp 331 and 341.
Definition
.Let p: E®B be a continuous surjective map. The open set U of B
is said to be evenly covered by p if
the inverse image p-1 (U) can be written as the union of disjoint
open sets Va in E such that for each a
, the restricion of p to Va onto U is an homeomorphism .The collection { Va } will be called a
partition of p-1 (U) into slices
.If any point b of B has a neighborhood U that is evenly covered by p ,then
p is called a covering map , and E is said
to be a covering space of B .If E is
a simply connected space and p is a covering map ,then we say that E is a universal covering space of B .
If B has a universal covering space E ,then E is
uniquely determined up to homeomorphism (provided B is locally path connected )
.The reason we call E universal covering
space is because it covers every other path-connected covering space of B.
(see[Munkress] pp 342 excersise 12*
,theorems (b),(c) ).
A sufficient condition
for the existence of universal covering space is given by the next theorem (see [Munkress]
pp 303 ,theorem 14.4.
Theorem
Let B be path connected
,locally path connected ,and semilocally simply connected .Let b0 ÎB .Given a subgroup H of p1(B,b0)
,there exists a path connected covering space p:E®B and a point e0 Î p-1 (b0) such that the induced
homomorphism p* of the fundamental groups by the covering map ,gives
p* ( p1(B,b0))=H
.In particular B has a universal covering space(H={1}).
( The proof of this lemma is based also on Corollary
14.5 in [9] pp. 397).
We sate also a basic result of «lifting» continuous
function from a space to a covering space of it .
Definition Let p:E®B be a map .If f is a cintinuous mapping of some space X into
B ,a lifting of f is a map :X®E such that p°=f .
Theorem
Let p:E®B be a covering map ; let
p(e0) =b0 . Let f and g be two paths in B from b0
to ; b1 let and be their liftings to
paths in E begining at e0 .
If f and g are homotopic ,then and end at the same point
of E and are homotopic .
3.
Trees as universal covering topological spaces of graphs.
In this paragraph we try to make formal an intuitive
fact of which are aware many workers in the software engineering that «Any flow-graph
or chart or petri-net of a program can
be untied to a tree». It
seems that there is more than one approach to this. One is purely algebraic
associates flow-charts to groups
and makes use of the fact that
any group is the quotient of a free group
The other is purely topological . We prefer the topological one ([4] pp.
14, 28).
First let us remember what is a tree:
Definition
An non-oriented tree
is a non-oriented graph without circles (or loops ) .A disjointunion of
non-oriented trees is called non-oriented forest
.
Definition
3.1
Let
a non - oriented graph G with vertices X=vertG and edges
Y=edgeG. That is we form the topological space T which is the disjoint union of
X and Yx[0,1], where X and Y are provided with the discrete topology and the
[0,1] has the topology of the real interval .Let R be the equivalence relation
on T for which (y,t)= (, 1-t) ,(y,1)=t(y) for
y in Y and t in [0,1] .By is denoted the edge y
with the inverse direction .The quotient space real(G)=T/R is called the (topological)
realization
of the graph G.
Remark
3.2 Realization is a
functor that commutes with direct limits .
Let a connected graph G . It is not difficult to prove
that real(G)
is path connected, locally path
connected and semilocally simply connected topological space.
Lemma
Let a connected graph G
.This in particular means that any two vertices can be joint with a path
(sequence of consecutive arrows ) It holds that
real(G) is path connected, locally path connected and
semilocally simply connected topological space.
Corollary
3.4.The realization real(G) of any connected non-oriented
graph G has a universal covering space which is the
realization real(T) of a non-oriented tree T. The realization real(G) of any
non-oriented graph G has a
universal covering space which is the realization real(T) of a non-oriented
forest T.
Proof:
The universal
covering of real(G), let us denote it by , is simply connected ,path connected .It holds that
there is a graph T such that real(T)= .By the lifting theorem all branches of real(G) (that are
compacts arcs actulally ) are lifted as arcs in . By the covering mapping property each branche is lifted in
to a disjoint set of arcs in . Any loop or cycle of the graph G is lifted to an infinite
set of arcs that make a path infinite
in both directions like consequtive
intervals in a infinite line (the universal covring space of a circle is the
infinite line ).Any point and any neighbourhood of belongs to these arcs .The set of these arcs makes
a (possibly infinite ) graph T ,that is homomorphically mapped on G and real(T)= (this is also assured by noting that real (T) is a simply
connected covering space of real (G) and using the uniquness of the universal
covering space ).As is simply connected
and path connected so is real(T) and the graph T .Thus T is a non-oriented tree
.
If the graph is non-connected we apply the previous
procedure to each connected component of it and we get the correspoonding
assertion for the universal covering forests QED.
Example
and Figure .
Definition
3.5 : A morphism of non-oriented graphs from T ,to H such
that the induced continuous map on the realization of the graphs is also a
topological covering map is called covering
map of the graphs. The graph T is said to cover
the graph H or that the T is a covering
graph of H.
Definition
3.6 The non-oriented tree T of a connected non-oriented graph G defined by the universal covering space of real(G)
we call
universal covering tree of
the graph.
If
the graph is not connected then we apply the above procedure to each one of its
connected components and the graph T is the disjoint union of non-oriened trees
in other words the universal covering
forest of the graph G .
Example
and figure
Theorem
3.7. A universal covering tree of a graph G, covers any
other covering graph of G.
Remark
The flow-charts or flow petri-nets of programs are finite connected graphs with two pointed
vertices called beginning and end and with all braches oriented .If any loop
of the graph is transversed say only once then any maximal path (of
monotone orientation ) has first vertice
the beginning and the last the end.In particular any arrow (oriented branche
)is contained in such a path. We shall call such graphs programs flow-chart graphs. If to any arrow is drawn say a square
in the middle of it while every vertice a circle then it may very well be called
program flow , petri-net .
Finally we remark that any morphism of graphs f:G®H defines a
continuous function
in the obvious way
(the correspondence of two branches defines an
homeomorphism of two real open
intervals ) .We call the mapping the topological morphism extracted by the graph
morphism .
The concept of oriented tree is defined as following
Definition
An (oriented ) tree T is a graph such that its
corresponding non-oriented graph is a is a non-oriented tree .An (oriented) forest is the disjoint union of a set
of (oriented) trees .
Remark
.The algebraic technique
to lift or «untie» program flow-chart graphs to trees corresponds to any
program flow-chart graph a ring- polynomial (called path generated function ) and vice
versa. The ring polynomial to which is
lifted in the free ring the polynomial of program flow-chart graph corresponds
to a tree that we call the computation
tree of the program flow-chart graph. The two techniques (the topological
and the algebraic ) are not equivalent .
We shall not formulate explicitly the algebraic technique in this
paper.
5.
Universal coverings of entailment systems.
In this paragraph we introduce the concept of universal covering of an entailment system.The idea is to “unfold” the category of deductions of the
entailment to one that is actually the
universal covering tree of them . The other
aspects of the entailment system like
the sorts and signatutes may not
change. An additional technicality is that
as the graph of the category of deductions of the entailment system may
be non-connected the “lift” is for every connected component to its the universal covering tree and the
“universal covering deduction category” is actually the free cartegory
generated by the disjoint union of the (simply) connected universal covering
trees thus a “forest” of trees .
The derived
system of a system
E is the system obtained from E
such that
a) The
signatures are the same , the sets of sentences for each signature are all the
subsets of all sentences of E (objects of the image of the functor sen ) of
this signature .
b) The deduction category of is defined as following:Let all the subsets of the sentences of E,they are defined as
the sentences of E’ . The entailment relation on all subsets of the sentences of is defined as the smallest extension to an
entailment relation than includes the new deductions on the sentences of ,from the
deduction of E. The extension of the
entailment relation is defined explicitly as following: For any subset A of sentences of and any sentence a
of it , we put AÃÄ a iff
for every dÎa there is bÎA such that it holds
b ÃÄ
d in the entailment system of E .We notice that the sentences of are actually sets
of sentences of the sentences of E .Thus it appears as a second Logical level or degree
system .
Definition
4.2 : The entailment system E’ defined as before is called
the derived entailment system of E .
Example
Definition
: A tree (forest )entailment
system, is a Mesenquer entailment system E such that the category of deductions
D(E’) is a the free category, that is
generated by an oriented tree (forest) .
The entailment system T is called connected
iff the category D(E’) is a connected graph .
Remark:
Let two entailment systems
Ea and Eb and
their derived Ea’ and Eb’. Any morphism of the graphs of the deduction categories of
the sentences of the derived systems
,D(P(senEa))=D(Ea’) , D(P(senEb))=D(Eb’)
,( where by P(x) we denote the power set of x) defines
an entailment morphism of the derived entailment systems .The minimality
of the extension of the entailment system
in the derived ,gives that the graph D(E’) (actually a category )
defines completly the entailment system E, while the signatures are fixed . And
any morphism between the derived entailment systems is projected directly to a
morphism of the source entailment systems.And in addition any morphism of the two entailment systems Ea
and Eb defines a morphism of
the derived systems .Actually the
technique of the derived entailment system was introduced in order to have that
(fixing the signature ) the entailment
system E is completly determined by the deduction category D(E’)
(also a graph ) of its derived entailement sets of sentences .
Definition
4.3 : A covering
map f : Ea --> Eb between two entailment systems is a map
of entailment systems such that the
signatures are fixed ( the F is the identity functor ) and the continuous morphism which is extracted from the graph of
the deduction category of the
entailment systems real( D(P(senEa)))=real(D(Ea’) to real(D(P(senEb)))=real(D(Eb’) is a covering mapping of graphs .We say
that the system Ea
derives covering of the system
Eb .We
also say that the derived system E’a covers
the E’b,or
that the E’a is
a covering system of Eb
.
Remark: Given a map of entailment systems f Ta --> Tb we extract a morphism of graphs from the
graph D(P(senTa))=D(Ta’ ) of the first system Ta to the D(P(senTb))=D(T’b) ,or of
the graphs of the deductions systems of the derived systems .The fiber (inverse
image ) of any vertice of D(P(senTb))=D(Tb’ ) defines a
partition on the set of vertices of D(Ta’ ) (the vertices of D(Ta’
) are subsets of sentences ,of Ta )
,thus an equivalence relation .As the equivalence relation is one obtained by a
system morphism it is a congruence R .If in addition the signatures of the
system do not change (are the identity functor ) by the morphism f ,we can say
that the system Tb is the quotient of the system Ta at
the sentences under the congruence R and we write “Ta /R = Tb ” .
The Universal
covering entailement system denoted by of the entailment
system T is the system obtained from T such that the signatures are
the same ,and the sets of sentences are the vertices of the universal
covering of the graph D(P(senT
))= D(T’) that is of the deduction category of the derived system . The
category of deductions on all subsets of the sentences of is defined as the
smallest extension of the entailment relation of T’ to an entailment relation
(on ) than
includes the new deductions on the new sentences introduced by the the .The extension of the
entailment relation in is defined explicitly as following: For any subset A’ of sentences of C() =D() (where by C(G) we denote as we mentioned the free
category of the graph G ) and any
sentence a of we put A ÃÄ
a if p(A) ÃÄ
p(a) in the derived entailment system T’of T ,where p is the covering map p: ->D(T’) .We notice
that the sentences of T’ and are actually sets of sentences of the sentences of T .
Thus it seems as a second logical level or degree ,system.
We remark also that if the deduction category D(T’) is
not a connected graph then we apply this process to each one of its connected
components .
Definition
4.4 The entailment system defined as above is called universal covering system of T .
Example
and figure
Theorem
4.5 (main result): Every entailment system has a universal covering entailment system .
Proof:
We apply the theorem of
the previous paragrapg that gives a universal covering forest to each graph .As
the graph here we take the deduction
graph of the derived system .The covering maps of the deduction graphs define
covering maps of the entailment systems .QED
Example
and figure .
Theorem
4.6 Every entailment system
E is isomorphic to a quotient system of a forest entailment
system.
Proof:
Direct from the previous
theorem and the definition of quotient entailment system .
QED
Theorem
4.7 There is forgetfull functor from the category of
entailment systems E with arrows the
covering maps, to the category of topological spaces (actually realisations of
graphs) .
Proof:We correspond to each entailment system T the
topological space real(D(T’)) .As we restrict from all entailement maps to
covering entailment maps the corespondence preserves arrows and thus is functor
.QED
Theorem
4.8 The universal covering entailment system of an
entailment system T covers all other
covering systems of the system T.
Proof:It holds as this holds for the universal covering
topological spaces and due to the definition of the covering entailment maps
.QED.
Corollary
4.9 The set of systems that cover a system admits the structure of a category with
objects the systems and arrows the covering entailment maps such that the
universal covering system is an initial object and arrows are the covering maps
of entailment systems.
Proof:
It holds as the universal
covering space has the property to cover any other covering space , due to the
definition of the covering entailment map and the choice opf the category with
arrows only the covering entailment maps .An initial object in a category has
arrows to all other objects in the category .QED.
[1] J. Goguen and R. Burstall. Institutions: Abstract
model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1):
95-146,1992.
[2] J. Lambek and
P.J. Scott, Introduction to higher order categorical logic, Cambridge
University Press 1986.
[3] J. Meseguer. General logics. In H.-D. Ebbinghaus
et. al, editors, Logic Colloquim'87,
pages 275-329. North-Holland,1989.
[4] J. P. Serre. Trees. Springer - Verlag.
[5] M. Barr and C. Wells. Toposes, Triples and
Theories, Springer 1985.
[6] J.A.Goguen. On Homomorphisms, Correctness,
Termination, Unfoldments, and Equivalence of Flow Diagram Programs, Journal of
Computer and System Sciences, pp. 333 - 365, Vol.8, No3, 1974.
[7] S. Mac Lane. Categories for the Working
Mathematician, Graduate Texts in Mathematics 5, Springer-Verlag.
[8] G. Graetzer. Universal Algebra, Second Edition,
Springer 1979.
[9] J. Munkeres. Topology a first course,
Prentice-Hall 1975.
[10] J. Meseguer. Conditional rewriting logic as a
unified model of concurrency. Theoretical Computer Science, 96:73-155, 1992.
[11] R. Diaconescu. Category-Based Semantics For
Equational and Constraint Logic Programming, D. Phil. Oxford University Computing
Laboratory, Programming Research Group, 1994. Also, Technical Monograph
PRG-116.