Course on Normalization
Abstract
The aim of this course is to present a basic technique from proof theory, Gentzen's normalization for natural deduction systems, and to discuss some of its applications. By normalization we mean a collection of algorithms transforming a given derivation into a certain normal form. A derivation is called normal if it does not contain any detour or - in Gentzen's terminology - cut, i.e. an application of an introduction rule immediately followed by an application of an elimination rule. Such normalization algorithms are useful because they allow to straighten out complex derivations and in this way extract hidden information. We will treat many applications which demonstrate this, e.g. the subformula principle, Herbrand's theorem, the interpolation theorem, and an exact characterization of the initial cases of transfinite induction provable in arithmetic. From the computer science point of view, an even more interesting field of application for normalization algorithms is the possibility to extract the constructive content of a maybe complex mathematical argument. Such algorithms can yield verified programs from derivations proving that certain specifications can be fulfilled. Of course, the feasibility of programs obtained in this way will depend to a large extent on a good choice of the derivation, which should be done on the basis of a good idea for an algorithm. However, in this approach it is possible to use ordinary mathematical machinery for the development of programs.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 17, 1989
- Accession Number
- ADA213961
Entities
People
- Helmut Schwichtenberg
Organizations
- Ludwig-Maximilians-Universität München