I have the CHR book, in which is described all the sorts of semantics one might hope to find in a logical language. You can take a simple program and prove consistency, correctness, completeness, etc. without necessarily looking at the operations, provided you code within certain boundaries. (Pretty much you could make the same statement regarding Prolog code.) In practice in either language I tend to think operationally in constructing a predicate, and declaratively in using it.
2 Likes
CHR has two kinds of declarative semantics: First-order logic declarative semantics and Linear logic declarative semantics.
Because CHR can model changes by removing and adding constraints, not each CHR program has First-order logic semantics, but it has linear logic semantics.
For example,
duplicate @ X leq Y \ X leq Y <=> true.
reflexivity @ X leq X <=> true.
antisymmetry @ X leq Y , Y leq X <=> X=Y.
transitivity @ X leq Y , Y leq Z ==> X leq Z.
This CHR program has First-order logic reading:
∀ X,Y (X≤Y ∧ X≤Y ⇔ X≤Y) ∧
∀X (X≤X ⇔ true) ∧
∀ X,Y (X≤Y ∧ Y≤X ⇔ X=Y) ∧
∀ X,Y,Z (X≤Y ∧ Y≤Z ⇒ X≤Z)
However, the following CHR program has no First-order logic reading:
throw(Coin) <=> Coin = head
throw(Coin) <=> Coin = tail
If you insist on First-order logic reading, it will be
∀Coin.(throw(Coin) ⇔ (Coin=head)) ∧
∀Coin.(throw(Coin) ⇔ (Coin=tail))
This is obvious wrong.
But it has linear logic reading:
!∀Coin.(throw(Coin) ⊸ !(Coin=head)) ⊗
!∀Coin.(throw(Coin) ⊸ !(Coin=tail))
which logically equivalent to:
!∀Coin.(throw(Coin) ⊸ !(Coin=head)) ⊗
(throw(Coin) ⊸ !(Coin=tail))
which logically equivalent to:
!∀Coin.(throw(Coin) ⊸ !(Coin=head) & !(Coin=tail))
This formula reads as “Of course, consuming throw(Coin) produces: choose from Coin=head and Coin=tail”. In other words, we can replace throw(Coin) with either Coin=head or Coin=tail but not both at the same time, i.e. a committed choice takes place.
Note that the penultimate logical equivalence uses “universal quantifiers distribution over ⊗”, I haven’t see this theorem on the internet, but intuitively it ought to be the same as “universal quantifiers distribution over ∧” in first order logic.
1 Like
Perhaps this next question deserves (or has already received?) its own thread. Can anyone familiar with Prolog and Datalog explain their differences? I ask because I notice that the Clojure JVM language has been used to develop many datalog implementations. EDIT: found a partial answer here: What's the difference between Prolog and Datalog?
In the current implementation, the second rule tends to be moot, and in general it is advised not to write this pair of rules, because programs including them often don’t have clear semantics.
Yes.
When discussing declarative semantics, they (CHR book and lots of CHR papers) just use abstract operational semantics, not concrete implementation.
Here the 2nd rule will never be fired.
However, from wikipedia:
Additive conjunction (A & B) represents alternative occurrence of resources, the choice of which the consumer controls.
So from consumer’s perspective, we can make a choice by reordering the rule.