Logic continuations

Abstract

We develop a ‘complete’ embedding of logic programming into Scheme—a lexically scoped Lisp dialect with first-class continuations. Logic variables are bound in the Scheme environment and the success and failure continuations are represented as Scheme continuations. To account for the semantics of logic variables and failure continuations, the state-space model of control is modified in a novel way that generalizes the trail mechanism. This assures that logic variable bindings are properly restored when continuations are invoked to perform ‘lateral’ control transfers that are not possible in a traditional logic programming context. It is thereby possible to obtain greater control over logic program behavior by using continuations as first-class objects.