Rephrasing your definition, if I understood it correctly, an application is a pair of a set of predicates, aka logics, and transaction-valued functions that refer only to these logics, forming the only two kinds for possible declarations. However, there is a lack of structure for the runtime behavior of these applications. Namely, transaction-value functions may change the state differently depending on the application order, affecting the valuations of the logics these functions may refer to. The same extends to the composition operations; is that really a union? In short, we might need to consider a strict order, i.e., ordered sets. It seems as it is, you might even define each set of objects, logics and trans. functioning as some sort of (symmetrical) monoidal category.
I see no need to introduce these notions to deal with cycles, but I might be wrong here. You can work on the specification, assuming that the declarative program associated with any application is terminating. In other words, an application is a well-typed program in a formal system such as the one in Juvix. You could even compute the graph associated with the call sites of the logic and the trans. functions, and strengthen the typechecker, and required your conditions, that is, that the trans. functions only refer to that logics declared in the scope, and not imported elsewhere.
The application composition operation I defined just includes transaction functions from each of the operands to composition - it doesn’t include any additional transaction functions which could be created by applying different combinations of those “base” transaction functions sequentially - it’s the latter which is order-dependent as you describe (if I understand correctly).
I think I agree, at least for now - I was more trying to clarify what I understood as the conceptual distinctions, I don’t think we need to necessarily implement anything specific here yet - and we should be able to use the Juvix typechecker (or additions thereof) to check/prove properties about applications such as these. That said, it’s worth noting that the concept of “cycles” here is a bit distinct from how it might be used in other PLT contexts, we just made it up.