Logic and Computation - McGill School Of Computer Science

the structure of programs and we prove that every program normalizes using logical relations ...... We therefore introduce an explicit context for bookkeeping,.
Logic and Computation

Brigitte Pientka

School of Computer Science McGill University Montreal, Canada

These course notes have been developed by Prof. B. Pientka for COMP527:Logic and Computation. Part of the material is based on course notes by Prof. F. Pfenning (Carnegie Mellon University). DO NOT DISTRIBUTE OUTSIDE THIS CLASS WITHOUT EXPLICIT PERMISSION. Instructor generated course materials (e.g., handouts, notes, summaries, homeworks, exam questions, etc.) are protected by law and may not be copied or distributed in any form or in any medium without explicit permission of the instructor. Note that infringements of copyright can be subject to follow up by the University under the Code of Student Conduct and Disciplinary Procedures. Copyright 2014 Brigitte Pientka

Contents 1 Introduction

5

2 Natural Deduction 2.1 Propositions . . . . . . . . . . . . . . . . . . . . 2.2 Judgements and Meaning . . . . . . . . . . . . 2.3 Hypothetical judgements and derivations . . . . 2.4 Local soundness and completeness . . . . . . . 2.4.1 Conjunction . . . . . . . . . . . . . . . . 2.4.2 Implications . . . . . . . . . . . . . . . . 2.4.3 Disjunction . . . . . . . . . . . . . . . . 2.4.4 Negation . . . . . . . . . . . . . . . . . 2.5 First-order Logic . . . . . . . . . . . . . . . . . 2.5.1 Universal and Existential Quantification 2.6 Localizing Hypothesis . . . . . . . . . . . . . . 2.7 Proofs by structural induction . . . . . . . . . . 2.8 Exercises . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

7 8 8 10 15 15 16 17 18 19 20 25 27 28

3 Proof terms 3.1 Propositions as Types . . . . . . 3.2 Proving = Programming . . . . 3.3 Proof terms for first-order logic 3.4 Meta-theoretic properties . . . 3.4.1 Subject reduction . . . . 3.4.2 Type Uniqueness . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

31 31 38 38 39 41 41

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

4 Induction 43 4.1 Domain: natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . 43 4.1.1 Defining for natural numbers . . . . . . . . . . . . . . . . . . . 44 4.1.2 Reasoning about natural numbers . . . . . . . . . . . . . . . . . 44 3

4.1.3 Proof terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2 Domain: Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3 Extending the induction principle to reasoning about indexed lists and other predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.4 First-order Logic with Domain-specific Induction . . . . . . . . . . . . 5 Sequent Calculus 5.1 Normal Natural Deductions . . . . . . . . . . . . 5.1.1 Sequent calculus . . . . . . . . . . . . . . 5.1.2 Theoretical properties of sequent calculus 5.1.3 Cut-elimination . . . . . . . . . . . . . . . 5.2 Consequences of Cut Elimination . . . . . . . . . 5.3 Towards a focused sequent calculus . . . . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

6 Normalization 6.1 Genera