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.
