- 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.

- projection: x = x
_{i} - zero: x = 0
- successor: x >> x' = x' + 1
- composition: Let g
_{1}(x), ... , g_{k}(x) be programs that use input variables x_{1}, ... , x_{n}. Let f(x) be a program that uses input variables y_{1}, ... , y_{k}. Then composition f(g_{1}, ... , g_{n}) is given by:g

_{1}(x); x = y_{1}; 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

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.

- 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.

- 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).

- 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

- 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.

- 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.

Jan van Eijck Last modified: Tue Nov 30 00:06:08 CET 1999