TRANSPARENCIES FOR PANEL DISCUSSION "LOGIC IN THE CS UNDERGRADUATE CURRICULUM" SIGCSE CONFERENCE, Atlanta, February 28, 1998 -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Personal position: more than " logic is useful in CS " more than " logic is important for CS education " COMPUTER SCIENCE *IS* APPLIED LOGIC Therefore A good computer scientist / applied logician MUST HAVE A LOGIC RELATED BASIC TRAINING -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Logic comes historically from * Philosophical logic ( 2 millenia ) * Mathematical logic ( 1 century ) A mixed blessing: POSITIVE provides impressive groundwork results NEGATIVE suggests that logic is imported to CS burdens CS-logic with off the mark traditions COMPUTER SCIENCE WOULD HAVE DISCOVERED AND DEVELOPED LOGIC IN ITS OWN IMAGE AS ITS CONCEPTUAL UNDERPINNING HAD LOGIC NOT BEEN THERE -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= LOGIC IS THE EXACT ANALYSIS OF GENERAL RULES relating MANIPULABLE FORM (syntax) with MEANING (semantics) CS IS THE FIRST SCIENCE WHERE THESE RELATIONS ARE CENTRAL, because *1* Exact rules of form are essential for interpretation by machines *2* Exact rules of meaning are essential because meaning is operational and of immediate importance [compare: natural / social / mathematical sciences] *3* Exact rules can be feasibly manipulated ( because there are machines to do it, e.g. compilation ) -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= THERE ARE 5 TYPES OF SYMBIOTIC RELATIONS BETWEEN LOGIC AND CS 1. FUNDAMENTAL CONCEPTS 2. FUNDAMENTAL CONSTRUCTS 3. ANALYSIS AND APPLICATIONS 4. ANALOGIES 5. SYNTHESIS LOWER DIVISION UG EDUCATION IS CONCERNED WITH 1 & 2 UPPER DIVISION INCLUDE SOME 3 -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= FUNDAMENTAL CONCEPTS: ELEMENTARY EXAMPLES * INDUCTIVE GENERATION OF DATA => inductive proofs definition by recurrence E.G. 0 x -> Sx yield all N F[0] F[x] -> F[Sx] yield F [ all N ] f(0) dfnd f(x) dfnd yield f [all N] -> f(Sx) dfnd dfnd * DISTINCTIONS BETWEEN SYNTAX & SEMANTICS E.G. numerals vs natural numbers program text vs operational semantics -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= FUNDAMENTAL CONCEPTS: "SOPHOMORE EXAMPLES" * PARSING and other syntactic issues (binding, scope, transformations) * THE REGRESSIVE (= AXIOMATIC) METHODS BASIC vs DERIVED NOTIONS built-in functions vs programmed/dfnd functions * ABSTRACTION & ENCAPSULATION functionality, types procedures, modules, fnct dfntn * LEVELS OF DISCOURSE E.G. PARAMETERS vs variables A x^2 + B x + C = 0 f(n) defnd by recursion vs f_n are defined by (discourse-level) recurrence -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= FUNDAMENTAL CONSTRUCT: EXAMPLES FROM PROGRAMMING LANG * FUNCTIONAL PROGRAMMING lambda calculus => LISP, SCHEME ... * DECLARATIVE PROGRAMMING prolog ... higher order * RECURSIVE PROCEDURES syntax as data self reference MORE PROGRAMMING EXAMPLES: KIM BRUCE DATABASE & AI EXAMPLES: PHOKION KOLAITIS -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= FUNDAMENTAL CONSTRUCTS: EXAMPLES FROM COMPUTATION THEORY * BOOLEAN LOGIC, CIRCUITS * GRAMMARS, FORMAL LANGUAGES * FINITE STATE MACHINES, AUTOMATA THEORY * UNIVERSAL DEVICES, INTERPRETERS -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= ANALYSIS AND APPLICATIONS * FORMAL METHODS SPECIFICATIONS LANGUAGE SEMANTICS, COMPILER SEMANTICS SOFTWARE SPECS HARDWARE SPECS CO-SPECIFICATION * VERIFICATION LOGICS OF PROGRAMS PROGRAM DERIVATION AND INFERENCE MODEL CHECKING * AUTOMATED MATHEMATICS AUTOMAT, NuPRL, Mathematical Vernacular -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= ANALOGIES PRINCIPLES & METHODS WHICH UNIFY MATHEMATICA LOGIC AND CS LOGIC E.G. the SCH homomorphism PROOFS PROGRAMS ---------------------- ---------------------- assumptions A ... variables x:A ... ... ... natural deduction P functional prgrm P ... ... Theorem T if type T ---------------------- ---------------------- HIGHER ORDER HIGHER ORDER LOGICS TYPES (polymorphism) -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= SYNTHESIS: NEW DIRECTIONS E.G. * INFORMATION THEORY * VISUAL REASONING / PROGRAMMING * NOTIONS OF CERTAINTY & APPROXIMATION interactive proofs cryptography * LOGICS UNDERLYING DYNAMIC SYSTEMS biological systems -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= FINAL MESSAGE DON'T TEACH MATHEMATICAL LOGIC COURSE TO COMP SCI STUDENTS BUT DO * TEACH CS LOGIC COURSE * INTEGRATE LOGIC TO EXISTING COURSES