Description

G E N E R A L I Z E D G E N E R A L L O G I C S robert helgesson Doctor of Philosophy (PhD) Department of Computing Science Umeå University May 2013 Robert Helgesson: Generalized General Logics, May 2013

Information

Category:
## Music

Publish on:

Views: 84 | Pages: 37

Extension: PDF | Download: 0

Share

Transcript

G E N E R A L I Z E D G E N E R A L L O G I C S robert helgesson Doctor of Philosophy (PhD) Department of Computing Science Umeå University May 2013 Robert Helgesson: Generalized General Logics, May 2013 This work is protected by the Swedish Copyright Legislation (Act 1960:729) ISBN (digital): ISBN (printed): ISSN: UMINF: Electronic version available at Printed by: Print & Media, Umeå University Umeå, Sverige, 2013 A B S T R A C T Logic as a vehicle for sound reason has a long and lustrous history and while most developments follow the traditional notions of binary truth and crisp sentences, great efforts have been placed into the problem of reasoning with uncertainties. To this end the field of fuzzy logic is now of great importance both theoretically and practically. The present monograph seeks to extend and clarify the treatment of non-classical notions of logic and, more broadly, information representation in general. This is done using two theoretical developments presented with additional discussions concerning possible applications. The first theoretical development takes the form of a novel and strictly categorical term monad that readily allows for a multitude of non-classical situations and extensions of the classical term concept. For example, using monad composition we may represent and perform substitutions over many-valued sets of terms and thereby represent uncertainty of information. As a complementary example, we may extend this term monad to incorporate uncertainty on the level of variables and indeed the operators themselves. These two notions are embodied in the catchphrases computing with fuzzy and fuzzy computing. The second theoretical development is a direct generalization of the notion of general logics, a successful categorical framework to describe and interrelate the various concepts included under the umbrella term of logic. The initial leap towards general logics was the introduction of institutions by Goguen and Burstall. This construction cover the semantic aspects of logics and in particular, axiomatizes the crucial satisfaction relation. Adding structures for, e. g., syntactic entailment and proof calculi, Meseguer established general logics as a framework capable of describing a wide range of logics. We will in our generalization further extend general logics to more readily encompass non-classical notions of truth such as in fuzzy logics and logics operating over non-classical notions of sets of sentences. iii S A M M A N FAT T N I N G Logik är ett gammalt och kraftfullt verktyg för att föra korrekta resonemang och människor har under lång tid studerat och tillämpat olika logiska system. Dessa studier har till stor del fokuserat på logik som innefattar ett binärt sanningsbegrepp, det vill säga logik där en utsaga är antingen sann eller falsk. Givetvis är detta en väldigt begränsad vy då vi i vår vardag ofta måste värdera sanning på en betydligt mer flexibel skala. På samma sätt måste vi ofta resonera och fatta beslut utifrån information som på olika sätt kan vara osäker. En djupare förståelse för dessa otraditionella logiker är därför av stort intresse till exempel i expertsystem som mekaniskt föreslår beslut utifrån osäker information. I denna monografi beskriver vi två matematiska ramverk som tillåter oss att beskriva dessa typer av otraditionella logiker och otraditionell representation av information i allmänhet. Dessa teoretiska konstruktioner är kompletterade med diskussioner relaterade till praktiska och vidare teoretiska tillämpningar. Den första av de två teoretiska konstruktionerna är en strikt kategoriteoretiskt definierad termmonad som kan beskriva termer och variabelsubstitution för en mängd olika otraditionella termkonstruktioner. Till exempel, genom monadkomposition kan vi representera flervärda mängder av termer och detta ger oss möjlighet att representera osäker information. Alternativt kan vi konstruera en termmonad som uttrycker osäkerhet på ett mer fundamental sätt genom att termernas ingående variabler och operatörer i sig kan ha associerad osäkerhet. Den andra teoretiska konstruktionen är en direkt generalisering av det matematiska ramverket generell logik som axiomatiserar de olika komponenter som ofta faller under logikbegreppet. I generell logik beskrivs dock dessa utifrån en traditionell vy och för att beskriva otraditionella logiker krävs därför ofta obekväma representationer. Den nämnda generaliseringen syftar därför till att förenkla konstruktionen av mer exotiska logiker inom ett ramverk som till stor del liknar generell logik. iv P U B L I C AT I O N S Some passages and figures have appeared previously in the following publications: Patrik Eklund, Robert Helgesson, and Helena Lindgren. Towards refinement of clinical evidence using general logics. In L. Rutkowski, R. Tadeusiewicz, L. A. Zadeh, and J. M. Zurada, editors, ICAISC, volume 5097 of Lecture Notes in Computer Science, pages Springer, ISBN Patrik Eklund and Robert Helgesson. Composing partially ordered monads. In R. Berghammer, A. Jaoua, and B. Möller, editors, RelMiCS, volume 5827 of Lecture Notes in Computer Science, pages Springer, ISBN doi: / _7. Patrik Eklund and Robert Helgesson. Monadic extensions of institutions. Fuzzy Sets and Systems, 161(18): , ISSN doi: /j.fss Patrik Eklund, M.Ángeles Galán, Robert Helgesson, and Jari Kortelainen. Fuzzy terms. Fuzzy Sets and Systems, ISSN doi: /j.fss Patrik Eklund, M.Ángeles Galán, Robert Helgesson, and Jari Kortelainen. From Aristotle to Lotfi. In R. Seising, E. Trillas, C. Moraga, and S. Termini, editors, On Fuzziness, volume 298 of Studies in Fuzziness and Soft Computing, pages Springer Berlin Heidelberg, ISBN doi: / _23. Patrik Eklund, Mario Fedrizzi, and Robert Helgesson. Monadic social choice. In A. G. S. Ventre, A. Maturo, S. Hosková-Mayerová, and J. Kacprzyk, editors, Multicriteria and Multiagent Decision Making with Applications to Economics and Social Sciences, volume 305 of Studies in Fuzziness and Soft Computing. Springer Berlin Heidelberg, ISBN v A C K N O W L E D G M E N T S I first and foremost express my gratitude to my thesis supervisor Patrik Eklund whose support, endless enthusiasm, and deep knowledge has been invaluable to me throughout the process of understanding and appreciating the power and beauty that arise from adopting strict formalisms in the field of computer science. Further, I have through the years as a PhD student collaborated with a number of excellent scientists such as Mario Fedrizzi, M.Ángeles Galán, Jari Kortelainen, and Helena Lindgren. As collaborators on articles and conference presentations they have all had a direct and influential effect on me and this text. A special mention goes to Ulrich Höhle whose insights into monoidal categories and quantales, shared with me and Patrik during numerous online meetings, have greatly improved this thesis. More generally I would like to thank all colleagues I have met at conferences, workshops, and other functions for the many interesting and inspiring discussions we have had. I finally also would like to express my appreciation of the department of computing science at Umeå University whose support and expertise has been crucial in me being able to complete my studies. vii C O N T E N T S 1 introduction 1 2 category theory and algebra Algebra Preliminaries Category Theory Preliminaries Monads and Partially Ordered Monads Sorted Categories Monoidal Biclosed Categories Signatures Term Monads Composing Monads Kleene Monads Kleisli Over Kleisli 62 3 general logics Institutions Entailment Systems Logics Theories The Category of Entailment Systems The Category of Institutions The Category of Logics Proof Calculi and Logical Systems The Categories of Proof Calculi and Logic Systems Framework Logics Refinement of Clinical Evidence generalized general logics Institutions, Entailment Systems, and Logics Substitution Logic applications in computer science and engineering Terms in type theory 139 ix x contents 5.2 Description Logic Social Choice information and process in health care Ontology in Health and Social Care Melanoma BPMN BPMN Data Object Information Semantics BPMN Token Semantics conclusions 181 bibliography 185 L I S T O F F I G U R E S Figure 1 The relationship between Γ, Γ, and Sen(Σ). 77 Figure 2 Comparison of axiom-preserving and non axiom-preserving theory morphisms, denoted σ Th and σ Th, respectively 80 Figure 3 Comparison of axiom-preserving and non axiom-preserving theory morphisms, denoted σ Th and σ Th, respectively. Here the source square represents some theoremata Γ Sen(Σ) with Γ Γ Figure 4 Initial seeking of care by patient. 168 Figure 5 Referral after excision. 169 Figure 6 Pathologist histology examination. 169 Figure 7 Overall BPMN encoded NEOPLASMS Melanoma (C43-C44) process. 170 Figure 8 TNM staging and prediction as provided by AJCC. 171 Figure 9 Alternative, more attractive presentation of a clinical report term. 178 xi I N T R O D U C T I O N 1 The concept of mathematical logic certainly has a long and lustrous history. From its dawn primarily in ancient Greece to its development into a field of modern rigorous study in the 1800 s, it has formed a foundation on which many great works of mathematics and computer science have been constructed [37]. As a result of the attention paid to the topic, there exists today not a single all-encompassing notion of logic but a wide variety of logics for all imaginable purposes. For the field of computer science, the situation has been succinctly summarized by the well known quote: There is a population explosion among the logical systems being used in computer science. Examples include first order logic (with and without equality), equational logic, Horn clause logic, second order logic, higher order logic, infinitary logic, dynamic logic, process logic, temporal logic, and modal logic; moreover, there is a tendency for each theorem prover to have its own idiosyncratic logical system. Goguen and Burstall [70] With all these possible logics, it is clearly of interest to view the nature of these logics and their relationships as a mathematical field of study in and of itself. To accomplish this it is of essential importance to have good definitions that closely match our intuition of the nature of logic. The solution brought forth by Goguen and Burstall [70] was the notion of institutions, a notion that we essentially may view as an axiomatization of the = symbol from logic. A logic described within this axiomatic framework will have to provide a strict construction of the models used in the logic as well as the structure of the sentences used to write formulas in the logic. Finally, the institutional definition of the logic 1 2 introduction includes the aforementioned = symbol as a relation allowing us to determine when a given sentence holds in the logic. As described by Diaconescu [35] in his excellent historical review of institution theory, the concept of institutions first appeared in Burstall and Goguen [26] under the name of language but the modern name soon became popular and by the time of the first major treatment of institution theory in its own right [see 70] it was a well established name. Burstall and Goguen were deeply interested in the use of institutions as a foundation for specification theory and, e. g., the wide spread specifications languages CafeOBJ [34] and CACL [7] both have foundations that to a large degree have been influenced by institution theory [35]. Once the worth of a framework of this kind became recognized, further developments and applications were inevitable and fruitful work has, e. g., arisen in model theory. We will here, however, focus on a framework different from but very much inspired by institution theory. This framework, called general logics, arose from the desire of a formal foundation for logic programming. Noting that institutions were biased in favor of model theory, which is insufficient to fully understand logic programming, Meseguer [105] built general logics such that it encompasses both the model theoretic and proof theoretic aspects of logic. His construction is modularized and actually includes institutions as an essential component, namely the one providing a logic s semantic notion of entailment. Beyond this it also includes, e. g., a component that axiomatize syntactic entailment, provided by the relation, and a component that axiomatize the proof calculus. Consequently, general logics puts into concrete mathematical terms the elusive concepts that make up what we typically call logic. In Helgesson [77] we attempted a self-contained and accessible presentation of general logics as described by Meseguer [105] and Loeckx et al. [98]. When exploring the definitions of general logics is it possible to make two broad but important observations: On the one hand one may say that general logics is, in certain aspects, an opinionated framework. For example, it is possible within general logics to describe and work with a great many logics but increasing levels of cleverness are necessary the further you stray from the or- introduction 3 thodoxy of a world of trues and falses into the world of maybes and sortofs. On the other hand, general logics remains deeply neutral concerning other matters. In particular, general logics says little to nothing about the actual structure of sentences and models. While this, in many cases, is a quite desirable property for a logic framework, we nevertheless must recognize that great swathes of logics have in common a deep dependency on terms. In this thesis, we will address the first point by presenting a generalization of general logics up to proof calculi that gives us a framework suitable for descriptions of non-classical logic with great freedom as to the choice of, e. g., notions of truth and representations of sentence structures. Having such a generalized general logic we then address the second point by providing a specialization for logics over terms. This specialization we call substitution logic as the concepts of variables and variable substitution is shared by all such logics. It is worth noting that by terms we here will consider a notion defined in a considerably more rigorous manner than traditionally employed. In particular, it is for a sufficiently general construction of substitution logic not adequate to rely on the definition of terms commonly encountered in the literature as such terms do not readily generalize to non-classical constructions of term sets or terms over non-classical signatures. By traditional terms we will consider any construction that is in essence verbal, i. e., one that is equivalent to a text of the form: For a signature Ω and variable set X we have that all x in X are terms, all constants in Ω are terms, and for an n-ary operator ω in Ω we have ω(t 1,..., t n ) a term if t 1,..., t n are terms. There are, for our purposes, certain crucial weaknesses in such a definition. For example, it does not carry variable substitutions as an inherent functionality instead substitutions are added later, typically using a similarly verbal inductive definition. This makes it difficult to treat the term construction in a category theoretical framework, specifically, it is hard to show functoriality. As another example, imagine we want to represent uncertain infor- 4 introduction mation in the form of fuzzy sets of terms, in this case we again run into trouble with respect to substitutions, in particular, how should we interpret the definition above when wishing to substitute a variable by a fuzzy set of terms? As a final example we observe that the verbal definition provide us with little support if we wish to entertain the idea of generalizing signatures such that, e. g., an operator may have an associated uncertainty. Together these weaknesses cause the informal definition above to be rather uninformative with respect to possible generalizations that may be of interest in a general framework for substitution logics. For the underlying terms we will therefore present a strict category theoretical construction, building on previous work of Eklund et al. [48] but extended to many-sortedness, i. e., we will here focus on terms that are inherently discriminated into different sorts or types as they are typically known as in computer science. Such discrimination is of importance in many practical applications and allow us to, e. g., talk of Boolean or integer terms and operators such as that takes integer arguments but whose result is a Boolean. The step taken when generalizing from the unsorted term construction to the many-sorted construction is often thought of as a trivial one but as will be seen, this is not the case. The misconception as to the simplicity of this generalization may have its root in the verbal term construction above, where it is indeed the case that the generalization is simple. As already alluded to, we will in this text rely a great deal on category theory as a foundation on top of which we define the necessary constructions. This brings us several advantages for free, in particular we are given a wide existing vocabulary suitable for the task at hand. Briefly stated, category theory is a field of mathematics that allow rigorous study of mathematical structures and transformations between them in a consistent and convenient manner. We will also make extensive use of certain algebraic structures and notions from universal algebra. So as to make this text relatively self-contained, these underlying concepts will in Chapter 2 be briefly presented in a way that hopefully is clear and accessible to readers unfamiliar with category theory and the algebraic notions that will be employed. Clearly, though, it is a considerable advantage to have a prior solid un- introduction 5 derstanding of category theory and algebra. Prior knowledge of the basic notions of discrete mathematics and mathematical logic is, however, assumed. Though, for some easily forgotten details, brief descriptions have been included. The structure of this document is as follows note that we include brief explanations of the contributions given in the various sections. As already mentioned Chapter 2 provides a brief coverage of the necessary basic notions of category theory and algebra. In Chapter 2 we also introduce a novel notion of many-sorted signatures as well as their corresponding notion of terms. In this chapter we also introduce some results concerning monads: Firstly, we show that the notion of partially ordered monads may be extended in a natural way to Kleene monads that induce Kleene algebras in an interesting way. Secondly, we show a simple but rather interesting result identifying the Kleisli category of a composed monad with a Kleisli over Kleisli category. Next, Chapter 3 will provide a relatively thorough treatment of classical general logic. No new constructions or results are presented in this chapter. In Chapter 4, however, we introduce the generalized constructions over general logics so as to admit convenient treatment of non-classical logics. The notion of substitution logic is defined and discussed in that same chapter. A number of examples of possible applications within the field of computer science and engineering are introduced in Chapter 5. Similarly Chapter 6 introduces an application within the field of health care. Finally, Chapter 7 will conclude the monograph with a brief discussion and prospects of future work. C AT E G O RY T H E O RY A N D A L G E B R A 2 From its first embryonic developments by Eilenberg and Mac Lane in the first half of the 1940 s with their seminal article General theory of natural equivalences published in 1945 [41], being the major introduction category theory has developed into a field of mathematical study in its own right. Then, certain features of cat

Related Search

Computing Sciencespace weather / Computing sciencePhilosophy and Thought in Islamic SciencePhilosophy of Information and ComputingPhilosophy of Mind and Cognitive ScienceUniversity ScienceHistory of Computing (Computer Science)Scientific Computing (Computational Science)Guilan University of Medical ScienceUniversity of Applied Science and Managment

Similar documents

We Need Your Support

Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks