Lambda the Ultimate

inactiveTopic Dynamo- Dynamic Logic Programming
started 10/30/2001; 1:05:58 PM - last post 11/3/2001; 4:29:47 AM
Ehud Lamm - Dynamo- Dynamic Logic Programming  blueArrow
10/30/2001; 1:05:58 PM (reads: 2040, responses: 7)
Dynamo- Dynamic Logic Programming
(via comp.lang.functional)

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

This seems to be related to hypothetical reasoning languages we mentioned here a long time ago.

I didn't really get into the theory, but the example programs on the site seem easy enough to understand...


Ken, can you tell us more on this?


Posted to Logic/Declerative by Ehud Lamm on 10/30/01; 1:08:22 PM

Ken Shan - Re: Dynamo- Dynamic Logic Programming  blueArrow
10/30/2001; 2:50:06 PM (reads: 1285, responses: 0)
Whoa, okay...

The research on dynamic logic that I know about mostly originates from natural language semantics, which studies what sentences mean and how. For example, consider the sentence 

  Every farmer who owns a donkey smokes.
A semantic theory might say that this sentence means something like 
  forall x. ( farmer(x) &&
              (exists y. donkey(y) && owns(x,y)) )
            => smokes(x).
Classical predicate logic works reasonable well here, in letting us write down and interpret this formula.

But now consider the sentence 

  Every farmer who owns a donkey beats it.
By analogy with the previous sentence, we might write down the formula 
  forall x. ( farmer(x) &&
              (exists y. donkey(y) && owns(x,y)) )
            => beats(x,y).
But this is not a well-formed closed formula, because the "y" in "beats(x,y)" is an unbound variable! Intuitively, the existential quantifier in "a donkey" somehow manages to scope beyond the restriction phrase "farmer who owns a donkey" into "beats it".

Dynamic logic proposes a different interpretation of logical formulas (leaving, for the most part, the syntax intact), so that the "y" in "beats(x,y)" above is no longer an unbound variable, and so some people think dynamic logic is more suitable for describing the semantics of natural languages such as English.

Jeroen Groenendijk and Martin Stokhof. Dynamic predicate logic. Linguistics and Philosophy, 14(1):39-100, 1991. http://turing.wins.uva.nl/~stokhof/

Ken Shan - Re: Dynamo- Dynamic Logic Programming  blueArrow
10/30/2001; 2:57:26 PM (reads: 1270, responses: 0)
Oh, and I should try to relate this dynamic logic stuff back to programming language semantics. The essence of dynamic logic as I see it is nondeterminism. Imagine a programming language in which you can say 
  {2,3,4} + {0,100} = {2,3,4,102,103,104}
Now add a construct 
  a_natural_number
which you can intuitively think of as 
  a_natural_number = {1,2,3,...}
Now we can write programs such as 
  fun is_prime n = not (non_trivially_divides a_natural_number n)
  where non_trivially_divides m n = m > 1 && m < n && n % m == 0
Neat, eh?

(I'm short on citations to the literature where this connection is explicitly stated, so any pointers would be greatly appreciated.)

Ehud Lamm - Re: Dynamo- Dynamic Logic Programming  blueArrow
10/31/2001; 2:23:57 AM (reads: 1252, responses: 0)
This sounds interesting so I'll as ask a couple of more questiosn...

1. So this is an extension of the work on the binding problem (aka anaphora)?

2. Isn't the programming language example simply showing what can be done with infinite data strctures (streams)?

Ken Shan - Re: Dynamo- Dynamic Logic Programming  blueArrow
10/31/2001; 6:04:13 PM (reads: 1224, responses: 1)
1. Yes.

2. Yes -- the example shows that streams, and more generally nondeterminism, are useful, especially when no special syntax is needed to access these features in a programming language, i.e., everything is a stream and determinism is a special case of nondeterminism. In natural language, we say "a number nontrivially divides 6", not (usually and certainly not mandatorily) "there exists a number x such that x nontrivially divides 6".

But my programming language example wasn't a terribly good one, because dynamic logic is more than just nondeterminism. Consider the sentences

12 is (nontrivially) divisible by a number that is a square of another number. The latter number divides 6, but not the former number.
In our programming language with nondeterminism, we are tempted to write 
    (a_natural_number ^ 2) non_trivially_divides 12
for the first sentence, but how shall we translate the second? Some kind of let-binding (ah! the word "binding"!) construct is necessary, and not just for the numbers that stand in the nontrivial-divisibility relation -- the number that the divisor is a square of also needs to be remembered for future use in the conversation. The "former number" here is analogous to the farmer who owns a donkey; the "latter number" is analogous to the donkey. The second feature of dynamic logic, then, is that the scope of an existential quantifier extends to the right indefinitely: Even after the first sentence ended (where the scope of an existential quantifier would have ended in classical logic), we can still talk about the two numbers.

(Note that the universal quantifier does not have this kind of "infinite scope"; in dynamic logic, "not forall" is not equivalent to "exists not". Compare:

  Some grandson of mine didn't come to the party. He was sick.
*Not every grandson of mine came to the party. He was sick.
So we seem to have a prediction about natural language that in this simple case is borne out.)

Ehud Lamm - Re: Dynamo- Dynamic Logic Programming  blueArrow
11/1/2001; 2:26:43 PM (reads: 1261, responses: 0)
Any references (online?!) about this quantifiers phenomenon?

Just to make sure I understand: When programming in Prolog, you can do something like:

foo(X) :- memeber(X,[1,2,3]), prime(X).

So essentially, we have the smae thing you describe. The X is existentialy quantified, and used later - prime(X). Indeed, Prolog will backtrack, if it needs to find a new X in order to satisfy prime.

Ken Shan - Re: Dynamo- Dynamic Logic Programming  blueArrow
11/2/2001; 11:05:39 PM (reads: 1196, responses: 0)
Ah, yes, writing the code in Prolog makes clear the connection between dynamic logic and "static" logic. Note that in Prolog you cannot translate "a farmer who owns a donkey beats it" to: 
  sentence :- farmer_who_owns_a_donkey(F), beats(F, D).
  farmer_who_owns_a_donkey(F) :- farmer(F), donkey(D), owns(F, D).
I should have said at the very beginning that Dynamo tries to be to dynamic logic what Prolog is to static logic.

Groenendijk and Stokhof are pretty well-known for their work on this stuff. Check http://turing.wins.uva.nl/~stokhof/ for some papers; I found "Dynamic Predicate Logic" to be a good first read.

Ehud Lamm - Re: Dynamo- Dynamic Logic Programming  blueArrow
11/3/2001; 4:29:47 AM (reads: 1198, responses: 0)
Thanks. This paper looks very promising (I read the first sections and they really cleared things up).

Since this is not really my field, but is fascinating none the less, I'd be happy if when you come across something interesting, you'd be willing to let us know around here.