Generalization from partial parametrization in higher-order type theory
type: Item
instance of: scholarly article
title: Generalization from partial parametrization in higher-order type theory
zbMATH Open document ID: 0676.68008
DOI: 10.1016/0304-3975(89)90074-1
author: Masami Hagiya
published in: Theoretical Computer Science
publication date: 1989-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68N99
Mathematics Subject Classification ID: 03B15
zbMATH DE Number: 4108144
zbMATH Keywords: software reusability
zbMATH Keywords: generalizing a program
zbMATH Keywords: formulae-as-types
zbMATH Keywords: typical higher-order type theory
zbMATH Keywords: longest up segment problem
zbMATH Keywords: largest sum segment problem
describes a project that uses: ML
MaRDI profile type: Publication
full work available at URL: 0304-3975(89)90074-1
OpenAlex ID: W2025821017
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Proofs as programs
cites work: Pebble, a kernel language for modules and abstract data types
cites work: The Type Theory of PL/CV3
cites work: Q3703866
cites work: Q3922646
cites work: Program abstraction and instantiation
cites work: Q4099613
cites work: A theory of type polymorphism in programming
cites work: Q3880323
description: scientific article; zbMATH DE number 4108144