home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #23 / NN_1992_23.iso / spool / sci / math / 12971 < prev    next >
Encoding:
Text File  |  1992-10-09  |  7.1 KB  |  158 lines
  1. Path: sparky!uunet!destroyer!gatech!usenet.ins.cwru.edu!po.CWRU.Edu!cfw2
  2. From: cfw2@po.CWRU.Edu (Charles F. Wells)
  3. Newsgroups: sci.math
  4. Subject: Graph based logic and sketches (abstract)
  5. Date: 9 Oct 1992 16:19:48 GMT
  6. Organization: Case Western Reserve University, Cleveland, Ohio (USA)
  7. Lines: 147
  8. Message-ID: <1b4bf5INNe2p@usenet.INS.CWRU.Edu>
  9. NNTP-Posting-Host: slc12.ins.cwru.edu
  10.  
  11.  
  12.              Graph-based Logic and Sketches
  13.              Atish Bagchi and Charles Wells
  14.  
  15.                       October 9, 1992
  16.  
  17. Extended Abstract
  18.  
  19. Traditional treatments of formal logic provide:
  20.  
  21. 1. A syntax for formulas. The formulas are typically defined recursively
  22.    by a production system (grammar).
  23.  
  24.  
  25. 2. An inference relation between sets of formulas. This may be given by
  26.    structural induction on the syntax for the formulas.
  27.  
  28.  
  29. 3. A rule for assigning meaning to formulas (semantics) that is sound
  30.    with respect to the inference relation. The semantics may also be
  31.    given by structural induction on the syntax of the formulas.
  32.  
  33.     First order logic, the logic and semantics of programming
  34. languages, and the languages that have been formulated for
  35. various kinds of categories are all commonly described in this
  36. way. The formulas in those logics are strings of symbols that
  37. are ultimately modeled on the sentences mathematicians speak and
  38. write when proving theorems.
  39.  
  40.     Mathematicians with a categorial orientation frequently
  41. state and prove theorems using graphs and diagrams (which may
  42. be described as graphs labeled coherently by data from some
  43. category). The graph, diagrams, cones and other data of a sketch
  44. are formal objects that correspond to the graphs and diagrams
  45. used by such mathematicians in much the same way as the formulas
  46. of traditional logic correspond to the sentences mathematicians
  47. use in proofs. The functorial semantics of sketches is sound in
  48. the informal sense that it preserves (usually by definition!)
  49. the structures given in the sketch. The analogy to traditional
  50. model theory is close enough that sketches and their models fit
  51. the definition of "institution" (Goguen and Burstall [2]), which
  52. is an abstraction of model theory.
  53.  
  54.     The content of this paper is to exhibit the structure in
  55. sketch theory that corresponds to items 1 and 2 in the
  56. description of logic (the deductive structure) and to provide a
  57. detailed translation of a particular logic between the
  58. string-based version and the sketch-based version.
  59.  
  60.     This work is parametrized by the type of categorial theory
  61. being considered. We assume given a finite-limit (projective)
  62. sketch E of a particular type of category as in [5] or [7]. E
  63. presents the type of category as essentially algebraic over the
  64. theory of categories. E -categories are then the models of E in
  65. Set. The kinds of categories that can be described in this way
  66. include categories with finite products, categories with limits
  67. or colimits over any particular set of diagrams, cartesian
  68. closed categories, regular categories, toposes, and many
  69. others.
  70.  
  71.     A formula in this setting is a potential factorization (PF)
  72. through a subobject of the codomain: formally, a pair consisting
  73. of an arrow of E and a subobject of the codomain of the arrow.
  74. We will refer to the codomain of the arrow as the codomain of
  75. the PF, and the subobject as the "claim" of the PF. Roughly, the
  76. PF is "true" if its arrow factors through its claim.  Sentences
  77. are PF's whose arrows have domain 1. We provide a general
  78. recursive construction of the objects and arrows of E (hence of
  79. the PF's in particular) which is derived from the similar
  80. recursive construction for initial algebras of FLS sketches
  81. given by Barr and the second author in [8].  Our thesis is that
  82. this recursive definition constitutes the rules of inference
  83. corresponding to item 2 above.
  84.  
  85.     An E-sketch is a sketch that allows the specification of any
  86. kind of construction that can be made in an E-category. This
  87. greatly enhances the expressive power of sketches when compared
  88. to Ehresmann's original definition. An E-sketch is a global
  89. element adjoined freely to E ([5] and [7]). The codomain of this
  90. adjoined arrow may be perceived as a description of the graph,
  91. diagrams and other constructions of the sketch.  Adjoining such
  92. an arrow constitutes the axioms of a theory, and the
  93. factorization of arrows through subobjects in the polynomial
  94. category E[s] obtained by adjoining such an arrow constitute the
  95. formulas and sentences that can be inferred from the sketch. The
  96. resulting system of inference is sound with respect to models.
  97. This type of logic fits some of the abstractions of logic that
  98. have been given, such as that of Meseguer in [4] and the
  99. formulation in terms of closures given by Tarski [6].
  100.  
  101.     As a kind of worked example, the paper will also contain a
  102. detailed description of the relationship between finite-product
  103. sketches and multisorted equational logic as given by Goguen and
  104. Meseguer [3]. It is intended that this translation be
  105. sufficiently algorithmic as to be implementable, for example in
  106. Mathematica. The equations of equational logic will be seen
  107. to correspond to a specific subset of the set of PF's; indeed,
  108. in the classifying topos of E, there is a specific object and
  109. subobject that is the common codomain and claim of the all the
  110. PF's. We will give explicit proofs of the correctness of the
  111. rules of inference given by Goguen and Meseguer in terms of the
  112. deductive system described above (the recursive construction of
  113. E).
  114.  
  115. References
  116. [1]M. Barr and C. Wells, Category theory for computing science.
  117.    Prentice-Hall International (1990).
  118. [2]J. A. Goguen and R. M. Burstall, A study in the foundations of
  119.    programming methodology: specifications, institutions, charters and
  120.    parchments. In D. Pitt et al., eds., Category Theory and
  121.    Computer Programming. Lecture Notes in Computer Science 240,
  122.    Springer-Verlag (1986), 313-333.
  123. [3]J. A. Goguen and J. Meseguer, Completeness of many-sorted
  124.    equational logic. Technical Report CSL-135, SRI International
  125.    Computer Science Laboratory, 333 Ravenswood Ave., Menlo Park,
  126.    CA 94025, USA (1982).
  127. [4]J. Meseguer, General Logics. Report SRI-CSL-89-5, SRI
  128.    International, Computer Science Laboratory, 333 Ravenswood Ave.,
  129.    Menlo Park, CA 94025, USA (1989).
  130. [5]A. J. Power and C. Wells, A formalism for the specification of
  131.    essentially-algebraic structures in 2-categories. Mathematical
  132.    Structures in Computer Science 2 (1992), 1-28.
  133. [6]A. Tarski, On some fundamental concepts of metamathematics. In
  134.    Logic, Semantics, Metamathematics, Oxford University Press,
  135.    1956.
  136. [7]C. Wells, A generalization of the concept of sketch. Theoretical
  137.    Computer Science 70 (1990), 159-178.
  138. [8]C. Wells and Michael Barr, The formal description of data types
  139.    using sketches. In M. Main, A. MElton, M. Mislove and D. Schmidt,
  140.    editors, Mathematical Foundations of Programming Language
  141.    Semantics, Springer Lecture Notes in Computer Science 298.
  142.    Springer-Verlag, 1988.
  143.  
  144. Atish Bagchi
  145. Department of Mathematics
  146. Case Western Reserve University
  147. University Circle
  148. Cleveland, OH 44106-7058, USA
  149. axb35@po.cwru.edu
  150.  
  151. Charles Wells
  152. Department of Mathematics
  153. Case Western Reserve University
  154. University Circle
  155. Cleveland, OH 44106-7058, USA
  156. cfw2@po.cwru.edu
  157. 
  158.