Book contents
- Frontmatter
- Contents
- Preface
- Programme of lectures
- Basic proof theory
- A short course in ordinal analysis
- Proofs as Programs
- A simplified version of local predicativity
- A note on bootstrapping intuitionistic bounded arithmetic
- Termination orderings and complexity characterisations
- Logics for termination and correctness of functional programs, II. Logics of strength PRA
- Reflecting the semantics of reflected proof
- Fragments of Kripke-Platek set theory with infinity
- Provable computable selection functions on abstract structures
Proofs as Programs
Published online by Cambridge University Press: 05 November 2011
- Frontmatter
- Contents
- Preface
- Programme of lectures
- Basic proof theory
- A short course in ordinal analysis
- Proofs as Programs
- A simplified version of local predicativity
- A note on bootstrapping intuitionistic bounded arithmetic
- Termination orderings and complexity characterisations
- Logics for termination and correctness of functional programs, II. Logics of strength PRA
- Reflecting the semantics of reflected proof
- Fragments of Kripke-Platek set theory with infinity
- Provable computable selection functions on abstract structures
Summary
Suppose a formal proof of ∀x∃y Spec(x, y) is given, where Spec(x, y) is an atomic formula expressing some specification for natural numbers x, y. For any particular number n we then obtain a formal proof of ∃ySpec(n, y). Now the proof–theoretic normalization procedure yields another proof of ∃ySpec(n, y) which is in normal form. In particular, it does not use induction axioms any more, and it also does not contain non–evaluated terms. Hence we can read off, linearly in the size of the normal proof, an instance m for y such that Spec(n, m) holds. In this way a formal proof can be seen as a program, and the central part in implementing this programming language consists in an implementation of the proof–theoretic normalization procedure.
There are many ways to implement normalization. As usual, a crucial point is a good choice of the data structures. One possibility is to represent a term as a function (i.e. a SCHEME–procedure) of its free variables, and similarly to represent a derivation (in a Gentzen–style system of natural deduction) as a function of its free assumption and object variables. Then substitution is realized as application, and normalization is realized as the built–in evaluation process of SCHEME (or any other language of the LISP–family). We presently experiment with an implementation along these lines, and the results up to now are rather promising. Some details are given in an appendix.
- Type
- Chapter
- Information
- Proof TheoryA selection of papers from the Leeds Proof Theory Programme 1990, pp. 79 - 114Publisher: Cambridge University PressPrint publication year: 1993
- 5
- Cited by