• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Type Theory and its Application to Machine Learning

Research Project

Project/Area Number 06680342
Research Category

Grant-in-Aid for General Scientific Research (C)

Allocation TypeSingle-year Grants
Research Field Intelligent informatics
Research InstitutionUniversity of Tokyo

Principal Investigator

HAGIYA Masami  The University of Tokyo, Graduate School of Science, Professor, 大学院・理学系研究科, 教授 (30156252)

Co-Investigator(Kenkyū-buntansha) HARAO Masateru  Kyushu Institute of Technology, Faculty of computer Science & System Engineering, 情報工学部, 教授 (00006272)
Project Period (FY) 1994 – 1995
Project Status Completed (Fiscal Year 1995)
Budget Amount *help
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 1995: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 1994: ¥1,200,000 (Direct Cost: ¥1,200,000)
Keywordstype theory / typed lambda-calculus / machine learning / induction / functional programming / automated deduction / 型付きλ計算 / 制約 / 算術制約 / 帰納推論 / 定理証明 / ユーザ・インタフェース
Research Abstract

The main purpose of this study is to develop a method for synthesizing a program or proof from its single example or multiple examples, based on the framework of type theory (typed lambda-calculi). In this study, we extended the head investigator's previous research and obtained the following results by examining possibilities to synthesize programs and proofs from examples with type theory as a central vehicle.
*type theory with arithmetical constraints
By using a type system that allows implicit inferences on arithmetical constraints, one can synthesize iterative structures which could not be generalized with an existing system.
We applied this technique for arithmetical constraints to tupling transformation of functional programs, though this is not directly related to machine learning.
*User-interface for machine learning
We developed a natational system with which one can specify iterative structures in proof text and invoke the function for generalization.Based on this idea, we also developed a spread-sheet program that can synthesize programs from examples.
*Investigation on induction
Synthesis of proofs from examples can be regarded as a method for inductive theorem proving. In this study, we showed that inferences on arithmetical constraints could enhance generalization of iterative structures. We further pointed out that arithmetical constraints are also useful for inductive theorem proving even without examples.
*Generalization with automated theorem provers
In this study, we mainly focused on generalization of proofs in type theory written by hand. In the last step of the study, we examined a method for generalizing proofs that are obtained by sutomated theorem provers using tactics or resolution.

Report

(3 results)
  • 1995 Annual Research Report   Final Research Report Summary
  • 1994 Annual Research Report
  • Research Products

    (24 results)

All Other

All Publications (24 results)

  • [Publications] Masami Hagiya: "A Typed lambda-Calculus for Priving-by-Example and Bottom-Up Generalization Procedure" Theoretical Computer Science. 137. 3-23 (1995)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] Wei-Ngan Chin, Masami Hagiya: "Tupling and Lambda Abstraction yield Dynamic-Sized Tabulation" Acta Informatica. 32. 93-115 (1995)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] 萩谷昌己,白取知樹: "「計算=編集」パラダイムにおける例によるプログラミング" コンピュータ・ソフトウェア. 13-3. 64-78 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] 萩谷昌己: "制約付き型理論の実現" 関数プログラミングII,レクチャーノート/ソフトウェア学,近代科学社. 63-77 (1994)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] Wei-Ngun Chin, Masami Hagiya: "A Bounds Inference Method for Vector-Based Memoization" International Conference on Functional Programing '97. 176-187 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] Masami Hagiya, Tomoki Shiratori: "Programming by Example in Computing-as-Editing Paradigm" Proceedings of the 11th International IEEE Symposium on Visual Languages. 275-283 (1995)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] Masami Hagiya: "A Typed lambda-Calculus for Priving-by-Example and Bottom-Up Generalization Procedure" Theoretical Computer Science. Vol.137. 3-23 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] Wei-Ngan Chin and Masami Hagiya: "Tupling and Lambda Abstraction yield Dynamic-Sized Tabulation" Acta Informatica. Vol.32. 93-115 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] Wei-Ngun Chin and Masami Hagiya: "A Bounds Inference Method for Vector-Based Memoization" International Conference on Functional Programming '97. 176-187 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] Masami Hagiya and Tomoki Shiratori: "Programming by Example in Computing-as-Editing Paradigm" 11th International IEEE Symposium on Visual Languages. 275-283 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] Masami Hagiya, Hiroshi Watanabe and Toshiko Kitamura: "On Merging Resolution and Induction" IPSJ. PRO-6-12. 67-72 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] Masami Hagiya: "Unification and Inductive Theorem Proving by Transformation of Equations with Recursors" JSSST'96. 97-100 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1995 Final Research Report Summary
  • [Publications] 萩谷昌己,白取知樹: "「計算=編集」パラダイムにおける例によるプログラミング" コンピュータ・ソフトウェア. (掲載予定). (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] 萩尾昌己,渡辺洋,北村敏子: "導出法と帰納的証明の融合について" 情報処理学会,プログラミング研究会. (掲載予定). (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] Masami Hagiya,Tomoki Shiratori: "Programming by Example in Computing-as-Editing Paradigm" Proceedings of the 11th International IEEE Symposium on Visual Languages. 275-283 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] M.Yamamoto,S.Nishizaki,M.Hagiya,Y.Toda: "Formalization of Planar Graphs" High-Order Logic Theorem Proving and Its Applications,Lecture Notes in Computer Science,Springer-Verlag. 971. 369-384 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] 山本光晴,萩谷昌己,白取知樹,西崎真也: "図的対象を扱う証明チェッカのための視覚化ツール" インタラクティブシステムとソフトウェアIII,レクチャーノート/ソフトウェア学,近代科学社. 12. 85-92 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] Masami Hagiya,Kouhei Iino: "Binding Time Analysis for Data Type Specialization" Fuji International Workshop on Functional and Logic Programming,World Scientific. 254-269 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] Masami Hagiya: "A Typed lambda-Calculus for Priving-by-Example and Bottom-Up Generalization Procedure" Theoretical Computer Science. 137. 3-23 (1995)

    • Related Report
      1994 Annual Research Report
  • [Publications] 萩谷昌己: "制約付き型理論の実現" 関数プログラミングII,JSSST'94,レクチャーノート/ソフトウェア学,近代科学社,. 63-77 (1994)

    • Related Report
      1994 Annual Research Report
  • [Publications] Wei-Ngan Chin,Masami Hagiya: "Tupling and Lambda Abstraction yield Dynamic-Sized Tabulation" Acta Informatica. (発表予定). (1995)

    • Related Report
      1994 Annual Research Report
  • [Publications] Masami Hagiya: "On Reduction and Projection in Type Theory with Inductive Definitions" 12th International Conference on Automated Deduction,Workshop 1B:Proof Search in Type-Theoretic Languages. 31-38 (1994)

    • Related Report
      1994 Annual Research Report
  • [Publications] Masanori Arita,MasamiHagiya,Tomoki Shiratori: "GEISHA System:An Environment for Simulating Protein Interaction" Genome Informatics Workshop. V. 80-89 (1994)

    • Related Report
      1994 Annual Research Report
  • [Publications] Masami Hagiya,Yozo Toda: "On Implicit Arguments(TR-95-1)" Department Information Science,University of Tokyo, 31 (1995)

    • Related Report
      1994 Annual Research Report

URL: 

Published: 1994-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi