Type Theory and its Application to Machine Learning

本研究的主要目的是基于类型论（类型化lambda- calculus）的框架，开发一种从单例或多例中综合程序或证明的方法。在这项研究中，我们扩展了首席研究员之前的研究，并通过考察以类型论为中心载体的综合程序和实例证明的可能性，获得了以下结果。*具有算术约束的类型理论通过使用允许对算术约束进行隐式推理的类型系统，可以综合现有系统无法推广的迭代结构。我们将这种算法约束技术应用于函数程序的元串变换，尽管这与机器学习没有直接关系。*机器学习的用户界面我们开发了一个全国性的系统，可以在证明文本中指定迭代结构，并调用函数进行泛化。基于这个思想，我们还开发了一个电子表格程序，可以从例子中合成程序。归纳法的研究举例证明法是证明归纳法定理的一种方法。在这项研究中，我们证明了对算术约束的推断可以增强迭代结构的泛化。我们进一步指出，即使没有例子，算术约束对归纳定理的证明也是有用的。*自动化定理证明的泛化在本研究中，我们主要关注于手工编写的类型论证明的泛化。在研究的最后一步，我们研究了一种推广由自动定理证明者使用策略或解决方法获得的证明的方法。

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.