Links2Go Key Resource Logic Topic |
|
Links2Go Key Resource Logic Topic |
Lygon is a logic programming language that is based on linear logic. It can be viewed as Prolog extended with features derived from linear logic. These features include a declarative notion of state and the ability to express problems involving concurrency. Also, the availability of use once predicates allows simple solutions to problems such as graph manipulation. Although the design of Lygon relies on a delicate proof-theoretic analysis of linear logic, programmers need have no knowledge of proof theory.
Linear logic can be used to model the consumption of resources. Whereas clauses in Prolog, based on classical logic, can be used many times during the execution of a program, clauses in Lygon, based on linear logic, must (by default) be used exactly once. Since both classical and intuitionistic logic can be embedded in linear logic, Lygon generalizes pure Prolog. Indeed, pure Prolog code (Edinburgh syntax) can be executed by Lygon's interpreter.
A description of Lygon, including design, implementation and applications, can be found in technical report 96/36: Hitch Hiker's Guide to Lygon 0.7. It is also available in postscript and pdf formats.
Lygon has a wide range of applications including graph problems (such as path-finding and Hamiltonian cycles), concurrent programming, modelling state, representing actions (e.g., the Yale shooting problem) and agent-oriented programming.
Another thread of research concerns bottom-up computation. Most logic programming languages, and all known logic programming languages based on linear logic, use top-down computation. That is, a computation begins with a goal and seeks to prove it using the program. In bottom-up computation, we start with a program and seek to determine what goals will succeed from this program. In classical logic, the bottom-up computation mechanism is used, for example, by deductive databases. Our current work in this area is foundational: identifying a calculus of bottom-up computation in linear logic (and in BI, the logic of bunched implications, developed by David Pym and Peter O'Hearn), and ensuring that the calculus satisfies various desirable properties.
The first Lygon implementation appeared in the following year, although there were still some technical problems with the operational semantics, which were ironed out in early 1994, and a prototype implementation was completed later that year. Subsequently, the Lygon implementation was refined and extended, including a debugger and a graphical user interface.
J. Harland and D. Pym, The Uniform Proof-theoretic Foundation of Linear Logic Programming (Extended Abstract), Proceedings of the International Logic Programming Symposium 304-318, San Diego, October, 1991 (gzipped postscript)This foundational work was extended in a number of subsequent papers culminating in a journal article appearing in 1994 which presented a detailed analysis leading to a suitable class of formulae, a resolution rule, a completeness proof, and some ideas for the implementation of the resulting language.
D. Pym and J. Harland, A Uniform Proof-theoretic Investigation of Linear Logic Programming, Journal of Logic and Computation 4:2:175-207, April, 1994. (gzipped postscript)The theoretical foundation having been set, attention turned to implementing the language and to the language's applications. The general development of the language was documented in a number of conference publications at ACSC. A discussion of the issues involved in implementing Lygon was presented at ILPS'95.
M. Winikoff and J. Harland, Implementing the Linear Logic Programming Language Lygon, Proceedings of the International Logic Programming Symposium (ILPS) 66-80, December, 1995. (gzipped postscript, pdf; presentation slides: pdf, postscript)M. Winikoff and J. Harland, Deterministic resource management for the linear logic programming language Lygon, Technical Report 94/23, Melbourne University, 1994. (postscript)
A description of Lygon together with a discussion of its applications was presented at AMAST'96.
J. Harland, D. Pym and M. Winikoff, Programming in Lygon: An Overview, Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology (AMAST) 391-405, July, 1996. (gzipped postscript, pdf; presentation slides: pdf)The Hitch Hiker's Guide to Lygon, a technical report, is more pragmatic: it contains directions for installing the Lygon implementation, a programmer-oriented description of the Lygon language and its semantics, and examples of Lygon's applications.
Michael Winikoff, Hitch Hiker's Guide to Lygon 0.7, Technical Report 96/36, Melbourne University, 1996. (postscript, pdf, html)The above list of publications isn't complete. Other Lygon related publications can be found in Michael's publications page, James' publications page and David's publications page.