Algebraic databases II

In the last post we generalized spatial logic. Recalling the construction, if A = (A₀,...,A_N;R)is an algebra with A_i denoting operators of arity i (thus, A₀are the constants, A₁are the unary operations, etc) with term language T(A)and relations R the we have a logic over A whose syntax and semantics are simultaneously specified by

• Boolean operations
  

[| true |] = T(A)
[| ~φ |] = T(A)\[| φ |]

[| φ₁ & φ₂ |] = [| φ₁ |] ∩ [| φ₂ |]

• Operations induced from the algebra
  

a ∈ A_k ⇒ [| a(φ₁,...,φ_k) |] = { b ∈ T(A) | ∃ a_i ∈ [| φ_i |]. b ≡ a(a₁,...,a_k) }
where ≡is the smallest congruence containing R

Notice that these operations provide observations of structure only. They have no intrinsically behavioral content. Following Milner,Leifer and Sewell, though, we can extend the interpretation to include behavioral observations. First, we expand our framework to include dynamics, in this case, a rewrite relation, →, modulo ≡. That is, we are working with DA = (A₀,...,A_N;R;→). Next, we recall, when 〈 l,r 〉 ∈ →, l = K(a), K(b) = r we say K labels the transition, a →^K b .

Then we may deduce behavioral operators of the form and function:

• Behavioral operations

[| 〈 K 〉φ |] = { b ∈ T(DA) | ∃ a. a →^K b, b ∈ [|φ|] }

As Milner and Leifer point out, there are a lot of contexts and it's useful to have a collection of minimal ones. Because this issue is orthogonal to the definition proposed above it is not necessary to address machinery needed to ensure minimality. Moreover, there are a number of connection points between that theory and the framework under consideration here. For example Sassone and Sobocinksi propose groupoidal relative pushouts to address locating the reaction in the presence of a structural congruence. What is the best relationship between the groupoidal structure and the structural equivalence relation relative to it's use in the logic? Some investigation of these issues has gone on in BiLog. But, the approach is somewhat different. In particular, they do not lift the logical operations from the underlying algebra+dynamics. Rather, they seek to pick a particular framework, bigraphs, and conduct the construction over that.

In the next post we revisit the issue of modeling state we raised in the previous posting with the suggestion of changing the base or ambient lattice hosting the interpretation. In particular, we compose the interpretation with a state monad. This allows us to derive the database language and execution semantics.