[Carpenter 1992] presents a logical formalism that comprises an algebra of feature structures and a syntax of descriptions. [Carpenter 1992] uses feature structures to model partial information about empirical objects, and interprets descriptions as true or false of feature structures. [Carpenter 1992] then presents a number of extensions to this formalism, and applies some of them to unification-based phrase structure grammars, definite clause programmes, and recursive type constraints.
[Carpenter 1992] imposes a condition called feature introduction in order to well define a function called type inference. In our paper, we argue that the feature introduction condition is undesirable. We slightly modify [Carpenter 1992]'s type inference function so that we can well define type inference regardless of the feature introduction condition, and we show that if the feature introduction condition holds then our modified type inference function reduces to [Carpenter 1992]'s original.
We structure our paper as follows. Section 1 retrospects, expands upon and illustrates those parts of [Carpenter 1992] relevant to our paper, section 2 criticises the feature introduction condition, and section 3 presents our type inference function. Appendix A contains the standard mathematical definitions and results needed for our paper.