TPG: Computation and Logic

Jim Laird

October 1999

1 Module Description

The aim of this course is to cover basic theory in the areas of recursion theory, lambda-calculus and logic, with particular reference to problems and applications in computer science.

Syllabus

Recursion Theory (See [7]) Recursive functions, the equivalence of models of computation, decision problems, coding and Kleene normal form.

λ-calculus (See [15], [13]) Conversion, reduction, confluence theorem, typed and untyped versions of λ-calculus, λ-definable functions are the partial recursive functions;

Logic (See [4], [12], etc.) Language and semantics. Proof systems. Soundness and completeness of predicate calculus. Complete and incomplete, decidable and undecidable theories.

Structure

The course is based on student presentations, supported by group discussion. Each presentation should cover the material laid down in the syllabus for that session. Feel free to incorporate additional related material, or to use a different presentation from that in the reading suggested (but be prepared to say how your presentation relates to that in the reading list).

The sessions are intended to be more like seminars than lectures — everyone present can contribute, questions are encouraged, and the presenter should encourage interaction, for example by including questions on the material presented. Although the syllabus is divided under three headings, there are many interesting connections between them, both historical and mathematical . Try to make explicit the relevance of what is being presented to what has been covered in previous sessions, for instance using previous discussion points as motivation for your talk.

Some general questions are included in the description of the sessions as possible discussion points.

Ask one of the secretaries for overhead slides and pens. Alternatively, you could use latex with the csslides option (see the local documentation) — not necessary by any means but familiarity with this package could be useful. In general, write less rather than more on each slide (you can always expand the material during presentation). Aim to give a 30–40 minute presentation, thereby leaving plenty of time for questions and discussion.

Please feel free to contact me, jdl, room 2605, if you wish to discuss the contents or details of a presentation.

Assessment

Assessment will be on the basis of your presentations, and your contribution to the discussion of the material.

2 Breakdown of course

2.1 Recursion Theory

For recursion theory, we will follow [7]; another account can be found in [4]. For some readings on characterisations of computability, see also [14]. More advanced material is covered in [9, 17].

2.1.1 Generating Computable Functions

Establish the definition of “computable by an unlimited register machine”, giving an example of a simple computation on a URM. Establish that functions computable this way are closed under various operations (composition, recursion, etc).

References: [7, chapters 1 and 2]

Questions: Why choose this characterisation of computability rather than another? Is this a “realistic” model of computation?

2.1.2 Church’s thesis

Establish the Gödel-Kleene characterisation of the partial recursive functions, and the definition of primitive recursive. Make plausible the equivalence of “partial recursive” with “computable by a URM”. Introduce some further characterisation of computability over the natural numbers.

References: [7, chapter 3].

[19] contains a (cod) philosophical discussion of what computability means.

Questions: How might we conceivably come to doubt Church’s thesis? What does computability over the natural numbers have to say about other data types?

2.1.3 Encoding programs

Traditional recursion theory lets programs become available as data by some encoding process. Describe the assignment of indices to programs. Show that we can effectively enumerate the set of all programs, and deduce the existence of uncomputable functions (both by a cardinality argument, and by direct diagonalisation). Also cover the s-m-n theorem.

References: [7, chapter 4]

Questions: Can these results be established without such an encoding process?

2.1.4 Universal programs

Define the notion of universal program. Give the Kleene normal form for recursive functions, and sketch the proof that every computable function can be put in this form. Show there is a total recursive function that is not primitive recursive (compare Ackermann’s function).

References: [7, chapter 5] Questions: Why can we not diagonalise out of the partial recursive functions as we can out of the primitive recursive functions?

2.1.5 Decidable problems, recursive sets

Show examples of undecidable problems (halting problem etc). Give some ‘reallife’ examples from mathematics (e.g. diophantine equations [16]), or computer science [5]. Explain recursive and r.e. sets, and show a set which is not r.e.

References: [7, chapters 6,7].

2.2 λ-Calculus

The λ-calculus originated as another attempt to characterize computability, but it is also the basis of functional programming. We will follow [15] and [13] (the latter is newer, and has a clearer presentation of some results but there is only one copy in the library); [3] is an encyclopaedic account of the theory (and worth consulting just for the photographs).

2.2.1 λ-calculus

Give syntax of λ-calculus and a careful specification of substitution. Explain α-convertibility and β-reduction. Give the Church-Rosser theorem (without full proof).

References: [15, chapter 1] [13, ch. 1–3]

Questions: What is the significance of the λ-calculus?

2.2.2 Combinatory Logic

Explain what a combinator is, with examples. Give the syntax of combinatory logic. Describe reduction with the K and S combinators, normal form, and Church-Rosser. Show that abstraction can be simulated with combinators.

References: [15, chapter 2], [13, chapter 4]; also [21] is an amusing tour round the use of combinators.

Questions: What do we gain and/or lose in moving from λ-calculus to combinatory logic?

2.2.3 Fixed points

Show fixed-points always exist in the untyped λ-calculus. Explain the η-rule, βη-normal form, and Böhm’s theorem. Discuss the history of the λ-calculus and the various notions of function involved.

References: [15, chapter 3] [13, 3.1]

Questions: Can we have nontrivial sets on which all endofunctions have fixedpoints? What implications does this have for the semantics of the λ-calculus,

2.2.4 Representing the recursive functions

Explain the Church numerals. Explain representability of functions in the λcalculus, and show that the representable functions are exactly the partial recursive ones. State undecidability of β-equality.

References: [15, chapters 4,5] [13, chapter 3]

2.2.5 Typed λ-calculus

Explain the notion of type, and the typed version of the λ-calculus. Explain its relation to the untyped version. Strong normalisation (without proof). A brief account of assigning types to untyped terms.

References: [15, chapters 6,8 pp 205–210]

2.3 Logic

Logic is generally divided into proof theory and model theory, both subjects with historical and contemporary relevance for computer science — this is where the mathematical study of syntactic objects (proofs and programs) and denotational models began. There are many opportunities for making links to material covered previously in the course. There is no single text covering all the material in this part of the course. A text that covers some of the early sessions adequately is [8]. However, the proof-theoretical side is given more thorough treatments in [10, 11].

For the sessions on incompleteness [4] is an excellent book. [12] is an idiosyncratic but entertaining description of an attempt to reconcile proof and model theory from a computer science perspective.

2.3.1 Predicate Calculus

Carefully define the propositional and predicate calculi, and their semantic interpretations, including the notions of validity and satisfiability. State and explain the compactness theorem for predicate logic, and the Löwenheim-Skolem theorems.

Questions: What does the Tarskian notion of truth tell us that is not obvious?

References: [8, Chapters 1 and 2] or [10, Chapter 5 Sections 1–6].

2.3.2 Proof systems

Discuss proof systems in Hilbert style, natural deduction and sequent calculus for predicate calculus, connections between them and with the typed λ-calculus and combinators.

[2, Chapter 1] and [12][Chapters 2—5], [10].

Questions: Why is there still no single standard notion of proof?

2.3.3 Predicate calculus: completeness

Give a careful proof of completeness for the predicate calculus without equality. Indicate how it extends to the equality case. Deduce the compactness theorem.

References: [8, Chapter 3], [10, chapter 5 sec 5–6]; see also [6].

Questions: When is it easier to reason abut a logic using a semantic characterisation, and when is it easier to use proof theory?

2.3.4 Cut elimination

State the cut elimination theorem for the sequent calculus, and prove it for the propositional fragment without the contraction rule. Use cut elimination to show that every proof of Σ_{1} − IND is witnessed by a primitive recursive function.

References: [2, Chapter 1] 2.3.5 Gödel’s incompleteness theorems

The definition of Gödel’s provability predicate. Incompleteness and the unprovability of consistency. References: [20] is fully comprehensive, also [4, chapter 16],

References

[1] S. Abramsky: Handbook of Logic in Computer Science, Vol 1 , Clarendon Press, 1992.

[2] P. Aczel et al (eds): Proof Theory, Cambridge University Press, 1988.

[3] H. Barendregt: The Lambda Calculus: Its Syntax and Semantics, North-Holland, 1984.

[4] Boolos and Jeffrey: Computability and Logic Third Edition. Cambridge University Press, 1990.

[5] G. Rozenberg and A. Salomaa: Cornerstones of Undecidability. Prentice Hall, 1994.

[6] J.N.Crossley et. al.: What is mathematical logic?, Oxford University Press, 1978.

[7] N. Cutland: Computability, Cambridge University Press, 1980.

[8] D. van Dalen: Logic and Structure, Second Edition, Springer-Verlag, 1983.

[9] M. Davis: Computability and Unsolvability, McGraw-Hill, NY, 1958. Reprinted 1982.

[10] J.H. Gallier: Logic for Computer Science, Wiley, 1987.

[11] J.-Y. Girard: Proof Theory and Logical Complexity, Bibliopolis, Naples, 1987.

[12] J.-Y. Girard (tr. and appendices by P. Taylor and Y. Lafont: Proofs and Types, Cambridge University Press, 1990.

[13] C. Hankin: Lambda-calculi: a guide for computer scientists, Oxford University Press, 1994.

[14] R. Herken: The Universal Turing machine: a half-century survey, Oxford UP, 1988.

[15] J.R. Hindley and J.P. Seldin: Introduction to Combinators and the λcalculus, London Mathematical Society, 1986.

[16] Y.V. Matiyasevich: Hilbert’s tenth problem, MIT Press, 1993.

[17] P.G. Hinman: Recursion-theoretic hierarchies, Springer-Verlag, 1978.

[18] J. M. E. Hyland and C.-H. L. Ong: On Full abstraction for PCF To appear in Theoretical Computer Science. Available from

    hypatia.dcs.qmw/author/OngCHL

[19] R. Penrose: The Emperor’s new mind: concerning computers, minds and the laws of physics, OUP, 1989.

[20] R. M. Smullyan: Gödel’s incompleteness theorems,Oxford 1992

[21] R.M. Smullyan: To mock a mockingbird and other logic puzzles including an amazing adventure in combinatory logic, Knopf, 1985.