Title: Reflection Mechanism in Constructive Programming
(Ph D. Thesis for Doctor of Engineering at Graduate School
of Kyoto University)
Author: Yukiyoshi Kameyama
Supervisor: Professor Masahiko Sato
Abstract:
This thesis studies the role of the reflection mechanism in
Constructive Programming.
Constructive Programming is a method of program development based on
constructive logic in which correct programs are automatically
extracted from proofs of given specifications. Recently it has been
widely accepted that the reflection mechanism is quite useful in
Constructive Programming.
RPT, Reflective Proof Theory, is a constructive logic proposed by
Sato. Since the reflection mechanism is built-in in RPT, it can be a
suitable basis for our study. In Chapter 2, we first propose a formal
system of RPT. We then give several theorems in the formal system,
which show the expressive power of the reflection mechanism of
RPT. Finally, we study metamathematical properties of the formal
system. In particular, the strong normalization theorem and the
consistency are proved for our formal system without inductive
definitions.
In Chapter 3, we describe our Constructive Programming System based on
the formal system given in Chapter 2. The system is implemented by the
programming language Lambda, which is at the same time the object
language of RPT. We give an overview of our Constructive Programming
System. As a substantial example of proof development using our
system, we demonstrate a mechanized proof of the Church-Rosser
property of the programming language Lambda. We also present a concrete
example of Constructive Programming based on our system, and present a
method to eliminate redundant parts from a program.
In Chapter 4, we will study yet stronger reflection
mechanism. Although the reflection mechanism in RPT is quite useful,
we cannot re-define a modified provability relation internally. The
re-definition of the provability relation is the key to eliminate
redundant parts in extracted programs. To solve this problem, we
propose the mechanism of half-monotone inductive definitions. A
half-monotone inductive definition is an extension of the conventional
monotone inductive definition so that we can define the provability
relation naturally. We give a theory and a realizability
interpretation of the half-monotone inductive definitions. We also
interpret several theories such as Martin-Lof's type theory and the
Logical Theory of Constructions using this mechanism. We also apply
the mechanism to the provability relations and show a method of
program refinement.
In Chapter 5, we turn our attention to programming languages. The
programming language Lambda given in Chapter 2 is a purely functional
one in the sense that there are no side-effects. It is an interesting
research problem to introduce imperative features into our
language. The programming language Lambda! (pronounced ``lambda
bang'') was proposed by Sato as an extension of Lambda in which the
assignment and the while statements are introduced. We give some
conservativeness results on Lambda! in Chapter 5.
In Chapter 6, we give concluding remarks of the thesis.