Case inference in resolution-based languages

Abstract

Informally, case inference is a type of inference that inherently involves disjunctions in deriving definite consequences. We show that a difficulty with efficient implementation of case inference in resolution-based languages stems from the fact that case inference always requires derived clauses to be reused as side clauses: in general, the number of derived clauses is quite large, and storing all of them seems unacceptably inefficient in programming language settings. However, our results also show that in retrieving definite information, this use of derived clauses is necessary only when case inference is required. This in turn leads to our next finding that storing a relatively small class of derived clauses, which is characterized in terms of certain properties of case inference, is sufficient for proving all definite consequences. We then show that a conservative approximation of this class can be, in effect, precomputed for clause sets not containing purely negative clauses.