1989 Fiscal Year Final Research Report Summary
Design of Proving, Verifying, and Synthesizing System based on Constructive
| Project/Area Number |
62460220
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Informatics
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
SATO Masahiko Res. Inst. of Elec. Comm., Professor, 電気通信研究所, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KAMEYAMA Yukiyoshi Res. Inst. of Elec. Comm., Research Associate, 電気通信研究所, 助手 (10195000)
|
|---|
| Project Period (FY) |
1987 – 1989
|
| Keywords | Constructive Mathematics / Functional Programming Language / Intuitionistic Logic / Proof / Program Verification / Program Synthesis |
|---|
| Research Abstract |
This project has investigated the key-idea constructive programming very thoroughly. Constructive programming is a new paradigm in programming methodology, which takes constructive logical system as an underlying theory and provides a rigid and uniform basis for verifying programs, proving mathematical theorems, and synthesizing programs from its logical specifications.
Our main results are summarized as follows:
1. We designed a well-organized constructive logical system SST. SST is symbolic in the sense that all terms and formulas can be treated mechanically, and therefore, by computers.
SST is a suitable logic for writing specifications (datatypes as sets), and for reasoning about properties of programs, since SST is a first order predicate logic for partial terms.
2. We established the theoretical results. We first made a model of SST to show SST is consistent. This model reflects our intended domain of S-expressions. We proved the representation theorem for general recursive functions
… More
in SST. We then defined the formalized realizability interpretation of SST. This interpretation resembles so called q-realizabilty, but we refined it to allow arbitrary inductive definition. We proved the soundness of our realizability interpretation.
3. SST contains a pure functional programming language LAMBDA. LAMBDA is formed by taking closed terms in SST. It is purely functional, but for practical conveniences, we extended it to LAMBDA+. We implemented the interpreter of LAMBDA on a workstation.
4. We programmed several systems on top of LAMBDA. We made a metaeircular interpreter of LAMBDA itself, a proof-checking system of SST, and a program-extractor LAMBDA. We can reason about the properties of these programs by the proof-checking system itself. The program-extractor extracts a LAMBDA-program from a proof in SST.
5. Using the above systems, we examined by examples the idea of constructive programming. We made sample proofs, and checked its validity by the proof-checking system, and extracted computational parts by the program-extractor.
As a feed-back of this process, we refined SST and LAMBDA so that these systems become more simple and easy to treat. Less
|
