Project/Area Number  05680276 
Research Category 
GrantinAid for Scientific Research (C).

Research Field 
計算機科学

Research Institution  KYUSHU UNIVERSITY 
Principal Investigator 
広川 佐千男 九州大学, 教養部, 助教授
HIROKAWA Sachio KYUSHU UNIVERSITY,DEPARTMENT OF PHYSICS,ASSOCIATE PROFESSOR, 理学部, 助教授 (40126785)

CoInvestigator(Kenkyūbuntansha) 
KOMORI Yuichi SHIZUOKA UNIVERSITY,DEPARTMENT OF MATHEMATICS,ASSOCIATE PROFESSOR, 理学部, 助教授 (10022302)

Project Fiscal Year 
1993 – 1994

Project Status 
Completed(Fiscal Year 1994)

Budget Amount *help 
¥1,700,000 (Direct Cost : ¥1,700,000)
Fiscal Year 1994 : ¥900,000 (Direct Cost : ¥900,000)
Fiscal Year 1993 : ¥800,000 (Direct Cost : ¥800,000)

Keywords  Constructive logic / Lambda calculus / Type theory / Intuitionistic logic / Relevant logic / CurryHoward / Formulasastypes / Classical logic / 構成的論理 / ラムダ計算 / 型理論 / 直観主義論理 / 適切さの論理 / curryHaward / 型としての論理式 / 古典論理 / 線形論理 
Research Abstract 
A formal system was obtained for the correspondence between formulas and computation rules. This correspondence extends the Formulasastype notion which is a basis of functional programming languages and program extraction from the constructive proofs. An essential discovery above the intuitionistic logic was the reduction rule for Peirce formula. This formula characterises the classical logic. The reduction rule we obtained has natural meaning not only from logical view point but also from program extraction using classical proofs. Several properties of the reduction were obtained. The similarity to the continuation computation was found as well. Further analysis is necessary. The following are the selection of the result for substructural logics below intuitionistic logic. Komori gave a clear syntactic proof for the PW problem in relevant logic by applying Gentzen system. Hirokawa characterised the lambdaterms that correspond to the proofs in PW and clarified the structure of the proofs in PW.In the joint work with M.Takahashi and Y.Akama, Hirokawa obtained a description of the set of proofs for a formula in intuitionistic logic as a contextfreelike grammar.
