Logic, (Functional) Programming, Model Checking
van Jan Eijck · 2014
This lecture will combine the topics of the title in various ways. First I will show that logic is part of every programming language, in the form of boolean expressions. Next, we will analyze the language of boolean expressions a bit, looking both at syntax and semantics. If the language of boolean expressions is enriched with quantifiers, we move from propositional logic to predicate logic. I will discuss how the expressions of that language can describe the ways things are. Next, I will say something about model checking, and about the reverse side of the expressive power of predicate logic. I will end with a brief sketch of epistemic model checking. In the course of the lecture I will connect everything with (functional) programming, and you will be able to pick up some Haskell as we go along. Every Programming Language Uses Logic From a Java Exercise: suppose the value of b is false and the value of x is 0. Determine the value of each of the following expressions: b && x == 0 b || x == 0 !b && x == 0 !b || x == 0 b && x != 0 b || x != 0 !b && x != 0 !b || x != 0 Question 1 What are the answers to the Java exercise? The Four Main Ingredients of Imperative Programming Assignment Put number 123 in location x Concatenation First do this, next do that Choice If this condition is true then do this, else do that. Loop As long as this condition is true, do this. The conditions link to a language of logical expressions that has negation, conjunction and disjunction. Let’s Talk About Logic Talking about logic means: talking about a logical language. The language of expressions in programming is called Boolean logic or propositional logic. Context free grammar for propositional logic: φ ::= p | ¬φ | φ ∧ φ | φ ∨ φ | φ→ φ | φ↔ φ.