_{0},...,A

_{N};R) is an algebra with A

_{i}denoting operators of arity i (thus, A

_{0}are the constants, A

_{1}are the unary operations, etc) with term language T(CA) and relations R the we have a logic over CA whose syntax and semantics are simultaneously specified by

- Boolean operations

[| true |] = T(CA)

[| ~φ |] = T(CA)\[| φ |]

[| φ

_{1}& φ_{2}|] = [| φ_{1}|] ∩ [| φ_{2}|]- Operations induced from the algebra

a ∈ A

_{k}⇒ [| a(φ_{1},...,φ_{k}) |] = { b ∈ T(CA) | ∃ a_{i}∈ [| φ_{i}|]. b ≡ a(a_{1},...,a_{k}) } where ≡ is the smallest congruence containing RExample (free monoid):

- m ::= e | c | m*m generates the language L(m) which when quotiented by the identity relations (m*e = m = e*m), L(m)/=, gives the free monoid with generators, c, and identity e
- Boolean operations:

[| true |] = L(m)

[| ~φ |] = L(m)\[| φ |]

[| ~φ |] = L(m)\[| φ |]

[| φ

_{1}& φ_{2}|] = [| φ_{1}|] ∩ [| φ_{2}|]- Operations induced from the monoid

[| e |] = { m ∈ L(m) | m ≡ e }

[| c |] = { m ∈ L(m) | m ≡ c }

[| φ

[| c |] = { m ∈ L(m) | m ≡ c }

[| φ

_{i}* φ_{2}|] = { m ∈ L(m) | ∃ m_{i}∈ [| φ_{i}|]. m ≡ m_{1}*m_{2}}- Example usage: ~e & ~(~e*~e) denotes primality; it picks out nontrivial elements that cannot be factored into nontrivial elements.

^{*}) where S* denotes the set of finite length tuples of elements from S (i.e. ∪

_{i}S

^{i}) with concatenation of tuples as a monoid operation (distinct from any operation that may be operating on the algebra). This gives us a quantale. Thus, we have a place to interpret linear formulae as the ambient logical operations. More generally, we can build appropriate lattice structure over the term language to interpret the "ambient" or "embedding" logic into which we embed the operations induced from the algebra.

My interest runs as follows. Spse CA a (generalized) algebra(ic data type). i submit that with an ambient or embedding logic of classical connectives we may auto-generate a read-only database+query language where the contents of the store are elements inhabiting CA; and, we can auto-generate a database+query language + update semantics with the appropriate set-indexed-linear lattice structure.

Practical applications?

- To address a semantics for an XQuery with update you run this construction over the Schema schema using a set-indexed linear lattice structure.
- Suppose that someone has determined that the geometry of protein sequences is best represented by elements of Clifford algebra. Then you can auto-generate a database for query and update of geometric information regarding protein sequences directly from the Clifford algebra specification.

- The main challenge i see is that a word problem hiding inside the definitions for the logical definitions induced from the algebraic operations.

## No comments:

Post a Comment