1990 Fiscal Year Annual Research Report

プログラム基礎理論の総合的研究

Research Project

Project/Area Number	02302009
Research Institution	Tohoku University
Principal Investigator	佐藤雅彦東北大学, 電気通信研究所, 教授 (20027387)
Co-Investigator(Kenkyū-buntansha)	亀山幸義東北大学, 電気通信研究所, 助手 (10195000) 龍田真東北大学, 電気通信研究所, 助手 (80216994)
Keywords	プログラム理論 / 直観主義論理 / 型理論 / グラフ理論
Research Abstract	計算機は現在、社会のいたるところで使われるようになっているが、その需要の爆発的増加にプログラム作成者の育成が追いつかず、いわゆるプログラムの危機とよばれる状態が予見されている。また、人間が作成したプログラムは必然的に誤りをともなうものであり、そのプログラムが要求仕様を満たすかどうかの保証がない。これらの状況に対処するためには、要求仕様、作成、保守の各段階において、プログラムの基礎的諸理論を統合し、数学的理論に基づいた厳密な方法が必要とされる。また、これらを自動化するめ、数理的に系統化された理論の研究とそれに基づく処理系の開発が不可欠である。こうした見地に立ち、本研究では、各研究分担者は、(1)基礎数理、(2)応用数理、(3)プログラミングの3つの主題について、プログラミングの基礎となる理論の構築、理論に基づくプログラム開発方式の研究、実際の応用プログラムの開発を行った。主要な研究実績として、直観主義論理、証明論、カテゴリ-論、型理論、λ計算、項書き替え系、再帰的関数論、様相論理、スコット理論、組み合わせ論、グラフ理論、代数学などの基礎的諸理論について考察し、相互の関連を検討した。特に、直観主義論理に基づく形式的体系を構築し、プログラムの検証、プログラムの合成等を試みた。また、論理型プログラム、関数型プログラム、対象指向プログラムなどの処理系について研究を行った。これらの研究活動の成果を発表する機会として、研究集会を開催し、相互の研究の理解を深めた。

Research Products

(34 results)

All Other

All Publications (34 results)

[Publications] Masahiko Sato and Yukiyoshi Kameyama: "Constructive Programming in SST" Proceedings of the JapaneseーCzechoslovak Seminar on Theoretical Foundations of Knowledge Infromation Processing,INORGA,1990. 23-30 (1990)
[Publications] 龍田真: "型理論I" コンピュタソフトウェア. 8ー1. 25-33 (1991)
[Publications] 亀山幸義: "構成的数学体系RPTに基づく超数学定理の形式化" 情報処理学会第42回全国大会. 1. 47-48 (1991)
[Publications] H.Enomoto,H.Mizutani and N.Tokushige: "A word problem in Coxeter semigroups" Discrete Mathematics(to appear).
[Publications] H.Ono: "Structural rules and a logical hierarchy" Proceedings of the Summer School and Conference on Mathematical Logic,Valna,1988,Plenum Press. 95-104 (1990)
[Publications] H.Ono: "Reasoning about knowledge and knowledge acquisitionーa case study" Proceddings of the JapaneseーCzechoslovak Seminar on Theoretical Foundations of Knowledge Information Processing,Prague,1989,Inorga. 61-69 (1990)
[Publications] P.Minari,M.Takano and H.Ono: "Intermediate predicate logics determined by ordinals" J.Symbolic Logic. 55. 1099-1124 (1990)
[Publications] H.Ono: "Phase structures and quantales" Technical Reports,Division of Mathematical and Information Sciences,Faculty of Integrated Arts and Sciences,Hiroshima University. 1-25 (1990)
[Publications] R.Nakajima,Y.Nishikawa,J.Nomura and K.Sawada: "Modeling of hierarchical multiobjective largeーscale problem inventory/production management and its practical application,Large Scale Systems:Theory and Applications 1986" 4th IFAC/IFORS symposium,Pergamon. 2. (1987)
[Publications] R.Nakajima,Y.Nishikawa,J.Nomura and K.Sawada: "Design of a decisionーsupport workstation system for hierarchical multiobjective largeーscale problem in inventory control,Operational Research'87" Proceedings of the Eleventh International Conference,NorthーHolland. (1988)
[Publications] R.Nakajima,K.Sawada and J.Nomura: "Decisionーsupport workーstation system for hierarchical multiobjective largeーscale inventory control" Matsushita Electr.Works Tech.Rep.37. 1-57 (1988)
[Publications] R.Nakajima,M.Hagiya,T.Hattori,A.Morishima,N.Nilde,R.Okazaki,T.Sakuragawa,T.Suzuki,H.Tsuiki and T.Yuasa: "Overview of GMW+Wnn system" Proceedings of the 2nd IEEE Conference on Computer Workstation,IEEE Comput.Soc.Press. (1988)
[Publications] S.Arikawa,A.Yamamoto and T.Shinohara: "Inductive Inference of Formal Languages by Elementary Formal Systems" Information Modelling and Knowledge Bases,IOS. 148-160 (1990)
[Publications] C.Zeng and S.Arikawa: "逆導出における2つの操作の完全性について" Proc.4th Annual Conference of JSAI. 139-142 (1990)
[Publications] H.Yuasa and S.Arikawa: "Pseudo Extension in Default Reasoning and Belief Revision by Model Inference" Lecture Notes in Artificial Intelligence,SpringerーVerlag. 383. 27-37 (1989)
[Publications] S.Arikawa et al.: "The text batabase management system SIGMA:An improvement of the main engine" Proc.Berliner InformatikーTage. 72-81 (1989)
[Publications] S.Arikawa et al.: "Elementary Formal System as a Unifying Framework for Language Learning" Proc.Computational Learning Theory,1989. 312-327 (1989)
[Publications] N.Zhou,T.Takagi,K.Ushijima: "A Matching Tree Oriented Abstract Machine for Prolog" Proc.of the 7th International Conference on Logic Programming,1990. 159-173 (1990)
[Publications] N.Zhou,T.Takagi,K.Ushijima: "Reducing the Cost of Backtracking for Prolog" Proc.of the International Conference on Information Thechnology,1990. 33-40 (1990)
[Publications] M.Hagiya: "Synthesis of rewrite programs by higherーorder and semantic unification" Proceedings of the First International Workshop on Algorithmic Learning Theory. 396-410 (1990)
[Publications] M.Hagiya: "Programming by example and proving by example using higherーorder unification" 10th Conference on Automated Deduction,Lecture Notes in Artificial Intelligence. 448. 588-602 (1990)
[Publications] M.Hagiya and 劉樹令: "Model inference of constrained recursive figures" Proceedings of the First International Workshop on Algorithmic Learning Theory. 335-367 (1990)
[Publications] M.Hagiya: "Higherーorder unification as a theorem proving procedure" Eighth International Conterence on Logic Programming.
[Publications] M.Hagiya: "高階単一化と証明の一般化" 人工知能学会誌.
[Publications] 大芝猛: "エルブランの定理の構成的証明" 名古屋工業大学学報. 41. 99-108 (1989)
[Publications] K.Hirose: "Formation and Developement of the concept of the algorithm" Advances in Software Science and Technology. 2. (1990)
[Publications] Y.Ichisugi and A.Yonezawa: "Distributed Garbage Collection Using Group Reference Counting" Tech.Rep.,Dept.of Inf.Sci.,University of Tokyo. 90ー014. (1990)
[Publications] S.Matsuoka,K.wakita and A.Yonezawa: "Synchronization constraints with inheritance:What is not possibleーSo what is?" Tech.Rep.,Dept.of Inf.Sci.,University of Tokyo. 90ー010. (1990)
[Publications] S.Matsuoka and A.Yonezawa: "Metaleval solution to inheritance anomaly in concurrent objectーoriented languages" Proceeidng of the ECOOP/OOPSLA'90 Workshop on Reflection and Metalevel Architectures in ObjectーOriented Programming. (1990)
[Publications] T.Watanabe and A.Yonezawa: "An actorーbased metalevel architecture for groupーwide reflection" Proceedings of the REX School/Workshop on Foundations of ObjectーOriented Languages,Noordwijkerhout,the Netherlands,Lecture Notes in Computer Science,SpringerーVerlag(to appear). (1990)
[Publications] T.Watanabe and A.Yonezawa: "An actorーbased metalevel architecture for groupーwide reflection" Proceeidng of the ECOOP/OOPSLA'90 Workshop on Reflection and Metalevel Architectures in ObjectーOriented Programming. (1990)
[Publications] 榎本彦衛,加納幹雄: "グラフの構造" 朝倉書店,
[Publications] 林晋、小林聡: "構成的プログラミングの基礎" 遊星社,
[Publications] A.Yonezawa: "ABCL:An ObjectーOriented Concurrent System" The MIT Press, 329 (1990)

1990 Fiscal Year Annual Research Report

プログラム基礎理論の総合的研究

Principal Investigator

佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)

Research Products

[Publications] Masahiko Sato and Yukiyoshi Kameyama: "Constructive Programming in SST" Proceedings of the JapaneseーCzechoslovak Seminar on Theoretical Foundations of Knowledge Infromation Processing,INORGA,1990. 23-30 (1990)

[Publications] 龍田 真: "型理論I" コンピュタソフトウェア. 8ー1. 25-33 (1991)

[Publications] 亀山 幸義: "構成的数学体系RPTに基づく超数学定理の形式化" 情報処理学会第42回全国大会. 1. 47-48 (1991)

[Publications] H.Enomoto,H.Mizutani and N.Tokushige: "A word problem in Coxeter semigroups" Discrete Mathematics(to appear).

[Publications] H.Ono: "Structural rules and a logical hierarchy" Proceedings of the Summer School and Conference on Mathematical Logic,Valna,1988,Plenum Press. 95-104 (1990)

[Publications] H.Ono: "Reasoning about knowledge and knowledge acquisitionーa case study" Proceddings of the JapaneseーCzechoslovak Seminar on Theoretical Foundations of Knowledge Information Processing,Prague,1989,Inorga. 61-69 (1990)

[Publications] P.Minari,M.Takano and H.Ono: "Intermediate predicate logics determined by ordinals" J.Symbolic Logic. 55. 1099-1124 (1990)

[Publications] H.Ono: "Phase structures and quantales" Technical Reports,Division of Mathematical and Information Sciences,Faculty of Integrated Arts and Sciences,Hiroshima University. 1-25 (1990)

[Publications] R.Nakajima,Y.Nishikawa,J.Nomura and K.Sawada: "Modeling of hierarchical multiobjective largeーscale problem inventory/production management and its practical application,Large Scale Systems:Theory and Applications 1986" 4th IFAC/IFORS symposium,Pergamon. 2. (1987)

[Publications] R.Nakajima,Y.Nishikawa,J.Nomura and K.Sawada: "Design of a decisionーsupport workstation system for hierarchical multiobjective largeーscale problem in inventory control,Operational Research'87" Proceedings of the Eleventh International Conference,NorthーHolland. (1988)

[Publications] R.Nakajima,K.Sawada and J.Nomura: "Decisionーsupport workーstation system for hierarchical multiobjective largeーscale inventory control" Matsushita Electr.Works Tech.Rep.37. 1-57 (1988)

[Publications] R.Nakajima,M.Hagiya,T.Hattori,A.Morishima,N.Nilde,R.Okazaki,T.Sakuragawa,T.Suzuki,H.Tsuiki and T.Yuasa: "Overview of GMW+Wnn system" Proceedings of the 2nd IEEE Conference on Computer Workstation,IEEE Comput.Soc.Press. (1988)

[Publications] S.Arikawa,A.Yamamoto and T.Shinohara: "Inductive Inference of Formal Languages by Elementary Formal Systems" Information Modelling and Knowledge Bases,IOS. 148-160 (1990)

[Publications] C.Zeng and S.Arikawa: "逆導出における2つの操作の完全性について" Proc.4th Annual Conference of JSAI. 139-142 (1990)

[Publications] H.Yuasa and S.Arikawa: "Pseudo Extension in Default Reasoning and Belief Revision by Model Inference" Lecture Notes in Artificial Intelligence,SpringerーVerlag. 383. 27-37 (1989)

[Publications] S.Arikawa et al.: "The text batabase management system SIGMA:An improvement of the main engine" Proc.Berliner InformatikーTage. 72-81 (1989)

[Publications] S.Arikawa et al.: "Elementary Formal System as a Unifying Framework for Language Learning" Proc.Computational Learning Theory,1989. 312-327 (1989)

[Publications] N.Zhou,T.Takagi,K.Ushijima: "A Matching Tree Oriented Abstract Machine for Prolog" Proc.of the 7th International Conference on Logic Programming,1990. 159-173 (1990)

[Publications] N.Zhou,T.Takagi,K.Ushijima: "Reducing the Cost of Backtracking for Prolog" Proc.of the International Conference on Information Thechnology,1990. 33-40 (1990)

[Publications] M.Hagiya: "Synthesis of rewrite programs by higherーorder and semantic unification" Proceedings of the First International Workshop on Algorithmic Learning Theory. 396-410 (1990)

[Publications] M.Hagiya: "Programming by example and proving by example using higherーorder unification" 10th Conference on Automated Deduction,Lecture Notes in Artificial Intelligence. 448. 588-602 (1990)

[Publications] M.Hagiya and 劉 樹令: "Model inference of constrained recursive figures" Proceedings of the First International Workshop on Algorithmic Learning Theory. 335-367 (1990)

[Publications] M.Hagiya: "Higherーorder unification as a theorem proving procedure" Eighth International Conterence on Logic Programming.

[Publications] M.Hagiya: "高階単一化と証明の一般化" 人工知能学会誌.

[Publications] 大芝 猛: "エルブランの定理の構成的証明" 名古屋工業大学学報. 41. 99-108 (1989)

[Publications] K.Hirose: "Formation and Developement of the concept of the algorithm" Advances in Software Science and Technology. 2. (1990)

[Publications] Y.Ichisugi and A.Yonezawa: "Distributed Garbage Collection Using Group Reference Counting" Tech.Rep.,Dept.of Inf.Sci.,University of Tokyo. 90ー014. (1990)

[Publications] S.Matsuoka,K.wakita and A.Yonezawa: "Synchronization constraints with inheritance:What is not possibleーSo what is?" Tech.Rep.,Dept.of Inf.Sci.,University of Tokyo. 90ー010. (1990)

[Publications] S.Matsuoka and A.Yonezawa: "Metaleval solution to inheritance anomaly in concurrent objectーoriented languages" Proceeidng of the ECOOP/OOPSLA'90 Workshop on Reflection and Metalevel Architectures in ObjectーOriented Programming. (1990)

[Publications] T.Watanabe and A.Yonezawa: "An actorーbased metalevel architecture for groupーwide reflection" Proceedings of the REX School/Workshop on Foundations of ObjectーOriented Languages,Noordwijkerhout,the Netherlands,Lecture Notes in Computer Science,SpringerーVerlag(to appear). (1990)

[Publications] T.Watanabe and A.Yonezawa: "An actorーbased metalevel architecture for groupーwide reflection" Proceeidng of the ECOOP/OOPSLA'90 Workshop on Reflection and Metalevel Architectures in ObjectーOriented Programming. (1990)

[Publications] 榎本 彦衛,加納 幹雄: "グラフの構造" 朝倉書店,

[Publications] 林 晋、小林 聡: "構成的プログラミングの基礎" 遊星社,

[Publications] A.Yonezawa: "ABCL:An ObjectーOriented Concurrent System" The MIT Press, 329 (1990)

佐藤雅彦東北大学, 電気通信研究所, 教授 (20027387)

[Publications] 龍田真: "型理論I" コンピュタソフトウェア. 8ー1. 25-33 (1991)

[Publications] 亀山幸義: "構成的数学体系RPTに基づく超数学定理の形式化" 情報処理学会第42回全国大会. 1. 47-48 (1991)

[Publications] M.Hagiya and 劉樹令: "Model inference of constrained recursive figures" Proceedings of the First International Workshop on Algorithmic Learning Theory. 335-367 (1990)

[Publications] 大芝猛: "エルブランの定理の構成的証明" 名古屋工業大学学報. 41. 99-108 (1989)

[Publications] 榎本彦衛,加納幹雄: "グラフの構造" 朝倉書店,

[Publications] 林晋、小林聡: "構成的プログラミングの基礎" 遊星社,