Type Theory and its Application to Machine Learning

点击翻译按钮获取中文摘要

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 constraintsBy 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 learningWe 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 inductionSynthesis 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 proversIn 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.