Generalization from partial parametrization in higher-order type theory (Q1122980)

The author introduces the syntax and notation used in the paper, and defines the formal system of the paper by giving its inference rules. The formal system is a simplified version of Martin Löf's constructive type theory [\textit{P. Martin-Löf}, An intuitionistic theory of types: predicative part (Logic Colloquium III, North-Holland, Amsterdam) (1973)], which is a typical higher-order type theory. Then, the author formalizes the problem of generalizing a program expressed in the formal system. He defines what is a generalization problem, and what is a solution to a generalization problem (a generalization). On this basis, he defines an order between generalizations so that a generalization whose program is the most instantiated and whose variables are the most distinct becomes maximal. The author proposes a generalization procedure which computes a maximal generalization with respect to this order. The procedure is based on an equivalence relation between occurrences in the original program. It successively selects an occurrence and tries to instantiate it; if it succeeds, the equivalence relation is updated. In the next section, the author describes some problems of the generalization procedure. If the procedure can produce many generalizations, one needs certain methods to resolve the ambiguity. Moreover, in many cases, the procedure constructs a generalization that is instantiated too much. These problems can be solved by determining the characteristic part of a program. Finally, an example is considered: a program solving the longest up segment problem is generalized with the intention of reusing it to the largest sum segment problem.