Dynamo-A Language for Dynamic Logic Programming

Dynamo is a language for dynamic logic programming based on a dynamic interpretation of first order logic familiar from Dynamic Predicate Logic or DPL. Dynamo implements an executable process interpretation of DPL, suitably augmented with constructs for bounded iteration and bounded choice. The process interpretation is faithful to the dynamic interpretation of predicate logic, in the following sense:

If Dynamo computes output b for formula F on input a, then any extension of a to a full valuation (defined on all variable of the language) will be related by the FOL dynamic interpretation of F to a full extension of b.
If Dynamo yields failure for formula F on input a, then F will fail under the FOL dynamic interpretation for any full extension of a.

The two main sources of inspiration for Dynamo are DPL , a language originally designed for natural language semantics, and Alma-0 , a hybrid language for imperative programming mixed with logic programming developed by Krzysztof R. Apt c.s..

Dynamo programs have a purely declarative dynamic semantics. There are no side effects, and no control features. Dynamo is pure dynamic logic. Because of this logical purity, weakest precondition reasoning for Dynamo is completely straightforward.

Example Dynamo Programs

Marriage program: marriage .
Stable Matching program: stable .
8 Queens program: 8queens .

Expressive Power of Dynamo

Dynamo computes all primitive recursive functions:

projection: x = x_i
zero: x = 0
successor: x >> x' = x' + 1
composition: Let g₁(x), ... , g_k(x) be programs that use input variables x₁, ... , x_n. Let f(x) be a program that uses input variables y₁, ... , y_k. Then composition f(g₁, ... , g_n) is given by:
g₁(x); x = y₁; some x; ... ; g_k(x); x = y_k; some x; f(x)
primitive recursion, with program f for the basis case, program g for the recursive step (assume the programs use y for input):
f(x); do n times begin x = y; some x; g(x) end

This does not mean, however, that all primitive recursive functions have obvious counterparts in first order logic.

Primitive recursion is modelled using the Dynamo construction for bounded iteration do n times .... This is an extension of dynamic FOL. If we extend the translation instruction instructions to translate this into standard FOL, we arrive at translations that are not UNIFORM in the recursion parameter. For every choice for n we get a FOL translation of do n times ..., but all these translations are different. In other words: the FOL translation of do n times ... does not contain n as a free variable.

This is not an accident. Indeed, there can be no uniform FO translation of bounded iteration in dynamic FOL. For recall that the FO theory of the natural numbers with just successor is decidable, but the FO theory of the natural numbers with + and * is not. Thus, + and * are not FO definable in terms of successor.

Certainly, + and * are primitive recursive, so these operations are definable in Dynamo. If there were a uniform FOL translation for do n times ..., then this translation would yield a FOL definition of + and + in terms of just successor, and we know that such a translation cannot exist. On the other hand, if f(x) is a primitive recursive function with input parameter x, then for every specific value m that one substitutes for x there is a FOL formula F(y) that computes f(m) in y (in the obvious sense that a variable state s satisfies F(y) in the natural numbers iff s(y) = f(m)). The snag is that if m and m' are different, the translations that compute f(m) and f(m') may look very different.

Source code

Dynamo is implemented in Haskell . To experiment with the language, you need a Haskell interpreter or compiler, e.g., Hugs , and the files below.

Lexical Scanner: L.lhs .
Syntax Definition: D.y . Only needed if you want to modify the parser module.
Parser Module: D.hs . This code is generated from D.y by the Haskell parser generator Happy .
Main Module: dynamo.lhs . This is literate Haskell code. If you feed it to Haskell, you get the compiled code for Dynamo , if you run it through LaTeX you get the documentation of the implementation.

Publications

Jan van Eijck Programming with Dynamic Predicate Logic Postscript . CWI report (INS-R9810) and ILLC report (CT-1998-06), 1998. Presents the executable interpretation, and proves its faithfulness with respect to DPL.
Jan van Eijck Dynamo - A Language for Dynamic Logic Programming Postscript Documents the implementation.
Jan van Eijck Computing with Dynamic First Order Logic Postscript Under submission.
Jan van Eijck and Juan Heguiabehere and Breanndan O Nuallain Theorem Proving and Programming with Dynamic First Order Logic - Full Version Postscript Manuscript.
Jan van Eijck Dynamo with Shift and Reduce Postscript Paper presented at DGNMR99 (March 25-27, 1999).
Jan van Eijck Powering Decision Machines with Dynamo Postscript Appeared in JFAK, Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday , Summer 1999.
Jan van Eijck and Juan Heguiabehere Dynamo with Constraint Handling Postscript On how to add constraints to Dynamo (Work in progress, Fall 1999).

Papers of Related Interest

K.R. Apt, J. Brunekreef, V. Partington, A. Schaerf Alma-0: An Imperative Language that Supports Declarative Programming ACM Toplas. In press. Postscript Describes syntax, semantics and implementation of Alma-0.
K.R. Apt, A. Schaerf Search and Imperative Programming Proc. 24th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '97), ACM Press, pp. 67-79. Postscript Describes the principles behind Alma-0.
Jan van Eijck, Axiomatizing Dynamic Logics for Anaphora Postscript Among other things, this describes a sound and complete axiomatisation of DPL. Appeared in the First Volume of the Journal of Language and Computation (Spring 1999)
Jeroen Groenendijk and Martin Stokhof Dynamic Predicate Logic Postscript Introduces DPL.
Albert Visser, Prolegomena to the Definition of Dynamic Predicate Logic with Local Assignments Postscript Utrecht Logic Group Preprint 178, October 1997

Work in Progress

Refine the Dynamo execution mechanism, by maintaining a stack of unresolved literals.
Combine Dynamo with Albert Visser's proposal for a dynamic treatment of argument places and brackets.

Future Work

Construct analysis tools for Dynamo programs: mapping Dynamo programs to their static meanings, analysing Dynamo programs to check whether they are pertinent (guaranteed not to generate the `I don't know' response).
Integrate Dynamo with other inference engines for first order logic.
Extend Dynamo with procedures and with a typing mechanism.
Put Dynamo to practical use: database query, Boolean constraint satisfaction, NL parsing, dynamic semantics for NL.
Analyse the way in which Dynamo programs function as queries. Link up with philosophical work on the semantics and pragmatics of questions.
Put Dynamo to theoretical use: construction of decision machines for fragments of first order and higher order logic.

Anyone who feels like helping with any of the above, or with further extensions of Dynamo , please get in touch with me.

Jan van Eijck

Last modified: Tue Nov 30 00:06:08 CET 1999