Some effects of dynamic types on logic program execution
Shaun-Inn Wu · 1988
Most implementations of logic programming languages suffer from inefficiency of program execution. This research is devoted to finding ways to execute logic programs efficiently by using type information. Types have previously been introduced into logic programming systems for the sake of program reliability, but such systems still suffer from inefficiency. The advantage of our system is that reliable and yet efficient logic programs are possible. We first give a general introduction to logic programming and discuss their type systems and execution efficiency. Then, we review the control strategies, including parallelism, currently in use on many logic programming systems. We then discuss a number of new control strategies based on type information. The ordering of subgoals affects the shape of the search tree. Our ordering algorithm determines the optimal ordering of subgoals as measured by the number of internal nodes of the search tree. Its complexity is linear in the number of subgoals within a clause. Dynamic type controls and type tests are provided as programming tools on our system to specify more precise types. A special case of improving efficiency by dynamic type controls and type tests is the prevention of infinite loops, as shown here in the ancestor problem. Multiplicities of predicates are upper bounds of possible solutions to predicates. They can be used to stop fruitless searching in the solution space. They also affect our ordering algorithm by modifying cardinality products of subgoals based on probabilistic hypotheses. In addition, they can be used as programming tools to avoid most of the usages of cut and naturally to generate multiple (but not all) solutions. Algorithms for inferring multiplicities have been developed and proved to be sound. Finally, our approach of embedding control information into the type system is evaluated according to the desired properties of the computation rules of logic programming systems. Compared with related works, our system is more flexible because predicates are fully invertible. Our system is also simpler since there is not the complication of extra-logical controls. Moreover, a better degree of separation of logic and control is achieved on our system.