# On the Semantics of Hybrid ASP Systems Based on Clingo
## 4 Structured Theories and Answer Sets
### Structured and Compositional Theories  
We have seen that the set of satisfiable sentences \(Sat\) of an abstract theory \(\mathfrak{T}\) is treated as an oracle or a blackbox: knowing its inner structure or behavior (if it has so) is not required at all for defining \(\mathfrak{T}\)-stable models. There may be cases where deciding whether some set \(S\) of theory atoms is satisfiable (\(S\in Sat\)) depends on the whole set together and cannot be decided in a compositional way, that is, in terms of some constructive condition about the satisfiability of the elements \(s\in S\). For instance, most abstract theories based on non-monotonic formalisms are non-compositional. Example A1 in Appendix A illustrates the case in which we use _Equilibrium Logic_[17] as the external theory: since equilibrium models are a kind of minimal models of some theories, their existence depends on the whole set of formulas in that theory. However, in most cases, the set \(Sat\) is defined in a compositional way, the following conditions imposed on the structure and elements used inside the theory atoms, as happens with linear equations containing integer variables and arithmetic operations. Trying to keep as much generality as possible, we introduce the use of variables inside theory atoms but rather than describing the semantics of operations among them, we just require the existence of some denotational semantics. Such theory-specific structures allow us to establish properties of abstract theories and ultimately characterize their integration into ASP. **Definition 3** (Structure). : _Given an abstract theory \(\mathfrak{T}=\langle\mathcal{T},Sat,\widehat{\cdot}\rangle\), we define a structure as a tuple \((\mathcal{X},\mathcal{D},\mathit{vars},\llbracket\cdot\rrbracket)\), where_  
1. \(\mathcal{X}\) _is a set of variables,_
2. \(\mathcal{D}\) _is a set of domain elements,_
3. \(\mathit{vars}:\mathcal{T}\to 2^{\mathcal{X}}\) _is a function giving the set of variables contained in a theory atom such that_ \(\mathit{vars}(\mathbf{s})=\mathit{vars}(\widehat{\mathbf{s}})\) _for all theory atoms_ \(\mathbf{s}\in\mathcal{T}\)_,_
4. \(\mathcal{V}=\{v\mid v:\mathcal{X}\to D\}\) _is the set of all valuations over_ \(\mathcal{X}\) _and_ \(\mathcal{D}\)_, and_
5. \(\llbracket\cdot\rrbracket:\mathcal{T}\to 2^{\mathcal{V}}\) _is a function mapping theory atoms to sets of valuations such that_ \[v\in\llbracket\mathbf{s}\rrbracket\text{ iff }w\in\llbracket\mathbf{s}\rrbracket\] _for all theory atoms_ \(\mathbf{s}\in\mathcal{T}\) _and every pair of valuations_ \(v,w\) _agreeing on the value of all variables_ \(\mathit{vars}(\mathbf{s})\) _occurring in_ \(\mathbf{s}\)_._  
Whenever an abstract theory \(\mathfrak{T}\) is associated with such a structure, we call it _structured_ (rather than abstract). In what follows, we represent a valuation \(v\) as a set of pairs \(\{x_{1}=d_{1},\ \ldots,\ x_{n}=d_{n}\}\) where \(x_{i}\in\mathcal{X}\) and \(d_{i}\in\mathcal{D}\) for all \(i=1,\ldots,n\). Since the valuation stands for a function, we do not allow \((x=d)\in v\) and \((x=d^{\prime})\in v\) for two different values \(d\
eq d^{\prime}\). On the other hand, we are sometimes interested in _partial valuations_\(v:\mathcal{X}\rightsquigarrow\mathcal{D}\) that, when represented as sets of pairs happen to be incomplete. That is, there may be variables \(x\in\mathcal{X}\) for which no pair \((x=d)\) is included in \(v\) (and so the variable is undefined). Given any valuation \(v\), we define its domain as \(\mathit{domain}(v)\stackrel{{\textup{\tiny def}}}{{=}}\{x\in \mathcal{X}\ \mid\ \exists d\in\mathcal{D},(x=d)\in v\}\), that is, the set of variables that are defined in \(v\). Total valuations satisfy \(\mathit{domain}(v)=\mathcal{X}\). Given a set \(S\) of theory atoms, we define its denotation as \(\llbracket S\rrbracket\stackrel{{\textup{\tiny def}}}{{=}} \bigcap_{\mathbf{s}\in S}\llbracket\mathbf{s}\rrbracket\).