Forum and its Implementation

Christian Urban

A thesis submitted to (1996) and accepted by (1997) the University of St Andrews in partial fulfilment of the requirements for the degree of Master of Philosophy.

Supervisor: Dr Roy Dyckhoff (St Andrews)
Examiners: Prof. Ursula Martin (St Andrews), Dr David Pym (London)

133 pages.

Abstract and contents as postscript. (74 Kby)

Table of Contents

  1. Introduction
  2. Foundations of Logic Programming an Forum
  3. Efficient Context Management
  4. Examples
  5. Related Work
  6. Conclusions, Open Problems and Further Work
  7. Proofs
  8. Source Code

Abstract

Miller presented Forum as a specification logic: Forum extends several existing logic programming languages, for example Lambda-Prolog, LO and Lolli. The crucial change in Forum is the extension from single succedent sequents, as in intuitionistic logic, to multiple succedent sequents, as in classical logic, with a corresponding extension of the notion of uniform proof.

Forum uses the connectives of linear logic. Languages based on linear logic offer extra expressivity (in comparison with traditional logic languages), but also present new implementation challenges. One such challenge is that of context management, because the multiplicative linear connectives `times', `par' and `lollipop' require context splitting. Hodas and Miller presented a solution (the IO model) to this in 1991 for the language Lolli based on minimal linear logic. This thesis presents a technique which is an adaptation of the aforementioned approach for the language Forum and following a suggestion of Miller that the `?' constant be treated as primitive in order to avoid looping problems arising from its use as a derived symbol. Cervesato, Hodas and Pfenning have presented a technique for managing the `top' constant, dividing each input context into a ``slack'' part and a ``strict'' part; the main novel contribution of this thesis is to modify this technique, by dividing instead the output context. This leads to a proof system with fewer rules (and consequent ease of implementation) but enhanced performance, for which we present some experimental evidence.