Skip to main content

Modes and Types in Logic Programming

Smaus, Jan-Georg (1999) Modes and Types in Logic Programming. Doctor of Philosophy (PhD) thesis, University of Kent at Canterbury. (KAR id:21739)

Language: English
Download this file
[thumbnail of modes_and_types_in_logic_programming_smaus.pdf]
Language: English
Download this file
[thumbnail of]


This thesis deals with two themes: (1) construction of abstract domains for mode analysis of typed logic programs; (2) verification of logic programs using non-standard selection rules. (1) Mode information is important mainly for compiler optimisations. The precision of a mode analysis depends partly on the expressiveness of the abstract domain. We show how specialised abstract domains may be constructed for each type in a typed logic program. These domains capture the degree of instantiation of a term very precisely. The domain construction procedure is implemented using the Godel language and tested on some example programs to demonstrate the viability and high precision of the analysis. (2) We provide verification methods for logic programs using selection rules other than the usual left-to-right selection rule. We consider five aspects of verification: termination; and freedom from (full) unification, occur-check, foundering, and errors related to built-ins. The methods are based on assigning a mode, input or output, to each argument position of each predicate. This mode is only fixed with respect to a particular execution. For termination, we first identify a class of predicates which terminate under the assumption that derivations are input-consuming, meaning that in each derivation step, the input arguments of the selected atom do not become instantiated. Input-consuming derivations can be realised using block declarations, which test that certain argument positions of the selected atom are non-variable. To show termination for a program where not all predicates terminate under the assumption that derivations are input-consuming, we make the stronger assumption that derivations are left-based. This formalises the ''default left-to-right'' selection rule of Prolog. To the best of our knowledge, this work is the first formal and comprehensive approach to this kind of termination problem. The results on the other four aspects are mainly generalisations of previous results assuming the left-to-right selection rule.

Item Type: Thesis (Doctor of Philosophy (PhD))
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 05 Sep 2009 09:12 UTC
Last Modified: 16 Nov 2021 10:00 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Smaus, Jan-Georg.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.