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:

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


Expressive Power of Dynamo

Dynamo computes all primitive recursive functions: 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.

Publications


Papers of Related Interest


Work in Progress


Future Work

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