07/01/1996 09:00 AM
Computer Science
One way to prove termination of a logic program is to show that input terms passed to each recursive procedure decrease in size between successive calls to the same procedure with respect to some appropriately defined norms. Except when all the input terms are ground, finding the appropriate norms is generally not easy. Barring the use of numbers and arithmetics, recursive calls are controlled by recursively constructed terms. Thus, one way to automatically find the appropriate norms would be to automatically identify recursive structures in term types. This report describes a work in progress that attempts to infer such recursive structures using abstract interpretation.
