On types and type consistency in logic programming (Diss., FernUniv. Hagen, 1999) (Q2726299)

The objective of this thesis is to add a type system to logic programming that allows a compiler to find automatically as many programming errors as possible by static analysis, fits well with the declarative and non-procedural nature of logic programs, is expressive enough to support rich modelling and various programming techniques, and, additionally, is applicable to standard Prolog, incl. its non-logical features. A summary from the back cover: ``This thesis investigates various aspects of using types in logic programming. These are classified into three dimensions: types for proving partial correctness, types as constraints, and types as approximations. Type checking for languages with hierarchies of both features types and constructor types is presented. Based on the notion of type consistency, a general method for the detection of useless expressions is developed. It is implemented in the Typical system that supports expressive type annotations including subtypes and parametric polymorphism. Type checking and type inferencing algorithms for Typical are defined, which, for example, implement automatic detection of type errors in standard Prolog programs enriched with type annotations.'' NEWLINENEWLINENEWLINEThe content of the thesis, briefly: Ch. 1 is a brief introduction. Ch. 2 discusses three dimentions of typing in logic programming. Ch. 3 presents polymorphic feature types. Ch. 4 reconsiders type constraints. Ch. 5 discusses types as approximations and consistency annotations. Ch.6 studies type consistency with subtypes and parametric polymorphisms. Ch. 7 is devoted to type inferencing. The last ch. 8 contains conclusions and summary. The thesis ends with appendices with basic definitions and terminology and presents the grammar for type definitions in LOT syntax.