1995 Fiscal Year Final Research Report Summary
Type Theory and its Application to Machine Learning
| Project/Area Number |
06680342
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | University 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
|
| Keywords | type 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.
|
