HTML/alglogc2.htm

   1 <html>\r
   2 \r
   3 <head>\r
   4 <title> Algorithmic Logic: its home page</title>\r
   5 </head>\r
   6 \r
   7 <body>\r
   8 <H1> Algorithmic Logic </H1>\r
   9 <h6> its home page </h6>\r
  10 \r
  11 <h4>Table of contents</h4>\r
  12 <ol>\r
  13 <li><a href="#def">Definition <em> per genus proximus et differentia specifica</em></a>\r
  14 <li><a href="#goal">Goals of AL</a>\r
  15 <li><a href="#struc">Structure of AL</a>\r
  16 <li><a href="#appli">Applications</a>\r
  17   <dir>\r
  18   <li>specifications of algorithms, data structures and programming languages\r
  19 \r
  20 \r
  21  \r
  22   <li>analysis of properties of programs (<em>verification</em>)\r
  23 \r
  24   <li>axiomatic definition of programming languages\r
  25 \r
  26   </dir>\r
  27 <li><a href="copyrigh.htm">Copyrights </a>\r
  28 <li><a href="biblio.htm">Readings</A>\r
  29 \r
  30 <li><a href="#new">What's new in AL?</a>\r
  31 <li><a href="projects.htm">Invitation to projects </A>\r
  32    <dir>\r
  33      <li>the assistant in proving, more precisely ...\r
  34      <li>an axiomatic specification of the Loglan'95 programming language...\r
  35    </dir>\r
  36 \r
  37 </ol>\r
  38 <hr><br><br><br>\r
  39 <ol>\r
  40 <p><li><h6><a name="def">Definitions</h6></a> \r
  41 <DL>\r
  42     <DT><em>algorithmic logics</em></dt>\r
  43     <DD> are a kind of logics of programs, their components are:\r
  44          a formalized algorithmic language and \r
  45          a consequence operation defined by means of logical axioms and inference rules. \r
  46     </DD>\r
  47 <p>\r
  48     <dt><em>logics of programs</em> </dt>\r
  49     <dd>is a family of logics, the language of a logic of programs admits \r
  50         programs as modalities. <br>\r
  51         Examples: <ul>\r
  52          <li>calculus of Floyd (descriptions of flowdiagrams)[1967], <li>calculus (Hoare) of partial correctness formulas [1969],\r
  53          <li>algorithmic logic [1969-1994], <li>calculus of weakest preconditions (Dijkstra)[1974], <li>dynamic logic [1976], etc. \r
  54          </ul>\r
  55     </dd>\r
  56 <p>\r
  57     <dt><em>an algorithmic language</em> </dt>\r
  58     <dd>\r
  59         is the smallest language which contains both the set of programs and the set of first order formulas and which is closed under the formation rule:<br>\r
  60 if P is a program and f is a formula then the expression Pf is an algorithmic formula. The set of algorithmic formulas admits the usual formation rules: disjunction, conjunction, negation, implication, quantification.  \r
  61     </dd>\r
  62 \r
  63 </dl>\r
  64 \r
  65 <li><p>\r
  66 <h6><a name="goal">Goals of AL</A></h6>\r
  67 - the study of semantic properties of computer programs. The role of AL \r
  68 in computer science is similar to that of mathematical logic in mathematics.\r
  69 AL studies those properties of programs whih are valid by virtue of their\r
  70 syntactical structure, independently of any interpretation of functional and\r
  71 relational symbols in programs. This leads to the discovery of algorithmic \r
  72 tautologies and inference rules, thus enabling algorithmic reasoning.\r
  73 Various programming constructs, one may say, various programming languages\r
  74 lead to various logics. In one logic you can discuss the properties of \r
  75 deterministic iterative programs, in another one may analyse the properties \r
  76 of concurrent(hence non-deterministic) programs, in yet another ...\r
  77 The theories based on AL are of interest for the study of abstract data types.\r
  78 For example, an algorithmic theory of stacks is the theory determined by its \r
  79 algorithmic language and the set specific axioms, <br>\r
  80 \r
  81 <p>\r
  82 <li><h6><a name="struc">Structure of AL</A></h6>\r
  83 <em> A recipe</EM>:\r
  84 Take one programming language Lp and its semantics. Consider the \r
  85 semantical phenomena of the executions of programs (like termination, \r
  86 correctness, partial correctness, equivalence etc.). Add a first-order \r
  87 language L1. Mix well, you will obtain an algorithmic language La. \r
  88 Remark its capability to express the semantical properties of programs \r
  89 (mentioned earlier).\r
  90 What you need now is a handful of axioms and inference rules. Be careful. \r
  91 Avoid inconsistency. Search for the completeness of your logic.\r
  92 Now, you are ready to serve  formal proofs\r
  93 of semantical properties of programs and other theorems. \r
  94 \r
  95 <li>\r
  96 <h6><a name="appli">Applications</A></h6>\r
  97 <ul>\r
  98 <li>specification of algorithms, data structures and programming languages\r
  99 A program K is specified by a pair of formulae alpha and beta. The formula\r
 100  of the form <br>\r
 101 alpha => K beta<br>\r
 102 is satisfied by a state of memory s iff either s does not satifies the \r
 103 precondition alpha, or if program K transforms the initial state s into a\r
 104 resulting state s' (i.e. no infinite loops, no fails either) and the state \r
 105 s' satisfies the post-condition beta.\r
 106 A set Z of formulae specifies a (family of) data structure(s) iff all formulas\r
 107 are valid in the data structure belonging to the family and no data structure\r
 108 outide the family satisfies all the formulae of the given set Z\r
 109 \r
 110  \r
 111 <li>verification and more precisely analysis of properties of programs\r
 112 One does it by proving the formulas that express the properties f programs\r
 113 \r
 114 <li>axiomatic definition of programming languages\r
 115 In a paper we we proved that the meanings of programming operators such as\r
 116 assignment operator, composition of programs operator begin... end,\r
 117 condititional instruction operator if ... then ... else ... fi operator,\r
 118 iteration instruction operator while... do ... od are uniquely determined\r
 119 by he fact that they satisfy the tautologies of algorithmic logic and that\r
 120 they are conformant to the inference rules of AL.\r
 121 In other papers we show that the primitive data types of programming languages\r
 122 are axiomatizable and we study their algorihmic theories.\r
 123 </ul>\r
 124 <br>\r
 125 \r
 126 <li><h6><a href="copyrigh.htm">Copyrights </a></h6>\r
 127 \r
 128 <li>\r
 129 <h6>What to <a href="biblio.htm">read</a>?</h6>\r
 130 <br>\r
 131 \r
 132 <li><h6><a name="new"> What's new in AL?</A></h6>\r
 133 We would like to announce two results of 1994.<br>\r
 134 In spite of the <a href="#Tennenbaum">Tennenbaum's theorem</A>\r
 135  <a name="powrot1"></a>it is possible to \r
 136 to construct a programmable and non-standard model for\r
 137  the elementary theory of stacks.\r
 138 The same remark applies as well to other specifications.<br>\r
 139 \r
 140 <strong>Theorem 1</strong><br>\r
 141 Let <a href="#stacks">S</a> be<a name="powrot2"></a> the algebraic specification of stacks. There exists a programmed\r
 142 module Stacks which correctly implements all the axioms mentioned in the specification S,\r
 143 the module Stacks admits infinite popping of certain stacks.\r
 144 <br>WARNING. Be careful, it may be the case that a software module satisfies\r
 145 all axioms of a given first-order specification, yet it may be pathological\r
 146 one. The facts: a module fulfills the axioms and the module is programmable \r
 147 do not necessarily means that the module has any value.<br>\r
 148 \r
 149 <br><strong>Theorem 2</strong><br>\r
 150 Algorithmic theory of stacks of bounded capacity is the \r
 151 complement of a recursively enumerable set.\r
 152 <br> Intuitively speaking this result gives an assuring answer to the question\r
 153 <em> 'Can one do the research of properties of programs\r
 154 using the calculus of AL? The nature of AL seem so complicated. Perhaps it would be better \r
 155 to use another logic of programs.'</em><br>\r
 156 Quite unexpectedly the oponents of AL are confronted with \r
 157 two facts:<br>\r
 158 - the dynamic logic has finitistic inference rules and \r
 159   the highly undecidable set of axioms,<br>\r
 160 - the algorithmic logic has a number of omega-rules,\r
 161   but the set of theorems of algorithmic theories of\r
 162   practical interest is relatively low in the hierarchy of Kleene-Mostowski.\r
 163 \r
 164 \r
 165 \r
 166 \r
 167 \r
 168 \r
 169 \r
 170 \r
 171 \r
 172 \r
 173 \r
 174 <li>\r
 175 <H6><a name="project">Two projects</A> </H6>\r
 176 <ul>\r
 177 <li>the assistant in proving, more precisely ...\r
 178 <li>an axiomatic specification of the Loglan'95 programming language...\r
 179 </ul>\r
 180 \r
 181 </ol>\r
 182 <hr>\r
 183 <h4>Explanations of notions used </h4><hr>\r
 184 <br>\r
 185 <a name="stacks">\r
 186 Algebraic specification of stacks:<Br>\r
 187 The universe is a union of two sets S- for stacks and E- for elements.<br>\r
 188 Operations and predicates:<br>\r
 189 push: E x S -> S<br>\r
 190 pop:  S -> S <br>\r
 191 top:  S -> E <br>\r
 192 empty: S -> {true, false} <br>\r
 193 Axioms:<br>\r
 194 <em>not</em> empty(push(e,s))<br>\r
 195 s = pop(push(e, s)) <br>\r
 196 e = top(push(e, s)) <br>\r
 197 <em>not</em> empty(s) => s = push(top(s), pop(s)) \r
 198 <a href="#powrot2">Back</a><br><br><hr>\r
 199 </a>\r
 200 <br>\r
 201 <a name="Tennenbaum">Tennenbaum's theorem<br>\r
 202 If M is a recursive(<em>i.e. programmable</em>) model of Peano's\r
 203 axioms of arithmetic of natural numbers then it is isomorphic to the\r
 204 standard model of natural numbers.<a href="#powrot1">Back</a>\r
 205 \r
 206 <hr>\r
 207 <address> <a href="../GMyAS.html">GM y AS</a> 10:07  01/01/1995 </address>\r
 208 </body>\r
 209 </html>\r