 Author
 Year
 2010
 Title
 Shortcircuit logic
 Number of pages
 25
 Publisher
 Ithaca, NY: arXiv.org
 Document type
 Report
 Faculty
 Faculty of Science (FNWI)
 Institute
 Informatics Institute (IVI)
 Abstract

Shortcircuit evaluation denotes the semantics of propositional connectives in which the second argument is only evaluated if the first argument does not suffice to determine the value of the expression. In programming, shortcircuit evaluation is widely used.
A shortcircuit logic is a variant of propositional logic (PL) that can be defined by shortcircuit evaluation and implies the set of consequences defined by a module SCL. The module SCL is defined using Hoare's conditional, a ternary connective comparable to ifthenelse, and implies all identities that follow from four basic axioms for the conditional and can be expressed in PL (e.g., axioms for associativity of conjunction and double negation shift.) In the absence of sideeffects, shortcircuit evaluation characterizes PL. However, shortcircuit logic admits the possibility to model sideeffects. We use sequential conjunction as a primitive connective because it immediately relates to shortcircuit evaluation. Sequential conjunction gives rise to many different shortcircuit logics. The first extreme case is FSCL (free shortcircuit logic), which characterizes the setting in which evaluation of each atom (propositional variable) can yield a sideeffect. The other extreme case is MSCL (memorizing shortcircuit logic), the strongest (most identifying) variant we distinguish below PL. In MSCL, only static sideeffects can be modelled, while sequential conjunction is noncommutative. We provide sets of equations for FSCL and MSCL, and for MSCL we have a completeness result.
Extending MSCL with one simple axiom yields SSCL (static shortcircuit logic, or sequential PL), for which we also provide a completeness result. We briefly discuss two variants in between FSCL and MSCL, among which a logic that admits the contraction of atoms and of their negations (i.e., x^x contracts to x and ¬x ^ ¬x contracts to ¬x if x is a propositional variable).  Link
 Link
 Language
 English
 Permalink
 http://hdl.handle.net/11245/1.328225
 Downloads
Disclaimer/Complaints regulations
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.