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
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.
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:
- Syntax Definition:
Only needed if you want to modify the parser module.
- Parser Module:
This code is generated from
the Haskell parser generator
- 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.
- 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
Documents the implementation.
- Jan van Eijck Computing with Dynamic First Order Logic
- Jan van Eijck and Juan Heguiabehere and Breanndan O Nuallain
Theorem Proving and Programming with Dynamic First Order Logic -
Full Version Postscript
- Jan van Eijck Dynamo with Shift and Reduce
Paper presented at DGNMR99 (March 25-27, 1999).
- Jan van Eijck Powering Decision Machines with Dynamo
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
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.
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.
Describes the principles behind Alma-0.
- Jan van Eijck, Axiomatizing Dynamic Logics for Anaphora
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
- 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.
Anyone who feels like helping with any of the above, or with further
extensions of Dynamo , please get in touch with me.
- 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
- Put Dynamo to theoretical use: construction of decision
machines for fragments of first order and higher order logic.
Jan van Eijck
Last modified: Tue Nov 30 00:06:08 CET 1999