Page 284 - Artificial Intelligence for the Internet of Everything

262 Artificial Intelligence for the Internet of Everything

associated with an architecture d. The requisite property of a valid decom-
position is that the component contracts together with the architecture
entail the system contract, which we may now write:

⟦d⟧^⟦C 1 ⟧^⋯^⟦C n ⟧ ‘ ⟦S⟧
In addition to assigning an interpretation to each component of the
operad, one must also ensure that these interpretations are coherent with
respect to composition. For contracts this is fairly straightforward. Compos-
ing d with a family of subdecompositions e i : K ij ! C i , we get the resulting
constraint by taking a conjunction of all the constraints in the
decomposition:
⟦ðe 1 ,…,e n Þ d⟧ :¼ ⟦e 1 ⟧^⋯^⟦e n ⟧^⟦d⟧
One version of the cut rule from logic says that if A and B entail C, while
C and D entail E, then A, B, and D together also entail E. Using a multi-
argument generalization of this rule we can easily show that the leaf condi-
tions ⟦K ij ⟧ together with the constraints ⟦e i ⟧ and ⟦d⟧ suffice to entail the
system contract:

⎛ ⎞
e i ∧ ⎝ K ij ⎠ C i
j

d ∧ C i S
i
⎛ ⎛ ⎞⎞
d ∧ ⎝ e i ∧ ⎝ K ij ⎠⎠ S
i j

To summarize, contract semantics on an operad of architectures are
defined by:

Syntax Semantics
Component State(C)
C ⟦C⟧ StateðCÞ
Q
Architecture
i StateðC i Þ
⟦d⟧ StateðSÞ
d : C i ! S ⟦d⟧^⟦C 1 ⟧^⋯^⟦C n ⟧ ‘ ⟦S⟧
Similarly, we should be able to produce design semantics for the
decomposition operad, but producing even a toy version of such a