School of Computing

Determinacy Inference by Suspension Inference

Andy King, Lunjin Lu, and Samir Genaim

Technical Report 2-05, University of Kent, Computing Laboratory, University of Kent, October 2005.

Abstract

The aim of determinacy inference is to infer a class of calls to a given logic program, for which execution will generate at most one answer and generate the answer only once. Two serious impediments to accurate determinacy inference are: (1) the way bindings imposed by a rightmost goal can make a leftmost goal deterministic; (2) the way determinacy is often enforced with cut. Rather surprisingly, this paper shows how: problem (1) can be tackled by recasting determinacy inference as a problem in concurrency; problem (2) can be addressed within this concurrency framework. Experimental evaluation shows that the new analysis can infer richer classes of deterministic calls for many programs.

Download publication 382 kbytes (PostScript)

Bibtex Record

@techreport{2262,
author = {Andy King and Lunjin Lu and Samir Genaim},
title = {Determinacy {I}nference by {S}uspension {I}nference},
month = {October},
year = {2005},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2005/2262},
    publication_type = {techreport},
    submission_id = {17999_1129815612},
    number = {2-05},
    address = {University of Kent},
    institution = {University of Kent, Computing Laboratory},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014