Theory.md

@@ -2,13 +2,63 @@
 
 In the heart of the NDL language lies a specific representation of Constraint Programming Problems. Instead of using a common Constraint (Hyper-) Graph formalization, we introduce a Typed Constraint Graph, that enriches the Constraint Graphs with types, representing the higher level structure of the problem.
 
-Typed Constraint Graph is a Labeled Directed Multigraph with no self-loops. Formally, it's an 8-tuple $`G = \left \langle V, A, s, t, \Sigma, \Theta, l, \theta \right \rangle`$, where:
-*  $`V`$ is a set of vertices
-*  $`A`$ is a set of edges
+Typed Constraint Graph is a Labeled Directed Multigraph with no self-loops. Formally, it's an 8-tuple $`G = \left \langle V, A, s, t, \Sigma_V, \Sigma_A, l_V, l_A \right \rangle`$, where:
+*  $`V`$ is a set of vertices representing variables and constants occurring in the problem
+*  $`A`$ is a set of edges representing binary constraints occurring in the problem
 *  $`s`$ and $`t`$ are both maps $`A \rightarrow V`$ pointing at the *source* and *target* vertices of an arc  
-* $`\Sigma`$ is a set of the arc labels
-* $`\Theta`$ is a set of the vertex labels 
-* $`l: A \rightarrow \Sigma`$ maps arcs to their labels
-* $`\theta: V \rightarrow \Theta`$ maps vertices to their labels
+* $`\Sigma_V`$ is a set of the vertex labels 
+* $`\Sigma_A`$ is a set of the arc labels
+* $`l_V: V \rightarrow \Sigma_V`$ maps vertices to their labels
+* $`l_A: A \rightarrow \Sigma_A`$ maps arcs to their labels
+
+
+
+The following section will focus on semantics of the graph, most notably on the label sets and constraints that have to satisfied by the multigraph to be a well Typed Constraint Graph 
+
+## Typing
+
+There are three kinds of types in the Typed Constraint Graph, two related to vertices, and one related to the arcs.
+
+### Sets
+
+*Set Type* corresponds to the finite set of integers, as known from the MiniZinc language.  Formally every *Set* is a tuple: $`\left \langle {ID}, {S} \right \rangle`$, where:
+*    $`ID`$ is an unique type ID
+*    $`S`$ is set of all integers inhabiting the type.
+
+Inhabitant of the *Set Type* $`\left \langle {ID}, {S} \right \rangle`$ is a pair $`\left \langle ID, c \right \rangle`$, where $`c \in S`$.
+
+### Variables 
+
+*Variable Type* corresponds to an array of Constraint Programming variables, as known from the MiniZinc language. Similarly to the arrays, inhabitants of the same *Variable Type* share domain and have unique indexes. Formally, every $`n`$-dimensional *Variable Type* is defined by a tuple $` \left \langle {ID}, \left \langle I_1, I_2, \ldots, I_n \right \rangle, {D} \right \rangle`$, where:
+*    $`ID`$ is an unique type identifier
+*    $`I_k`$ is a type ID of a *Set* used as the index set in the $`k`$th dimension
+*    $`D`$ is a type ID of a *Set*, defining possible valuations of the type inhabitants 
+  
+Inhabitant of the $`n`$-dimensional *Variable Type* $`\left \langle {ID}, \left \langle I_1, I_2, \ldots, I_n \right \rangle, {D} \right \rangle`$ is represented by a $`n+1`$-tuple: $` \left \langle {ID}, i_1, i_2, \ldots, i_n \right \rangle`$, where $`i_k`$ is an inhabitant of the corresponding $`I_k`$ type. 
+
+### Constraints
+
+*Constraint Type* corresponds to a group of constraints occurring in the problem, grouped according to:
+*  aggregation functions (e.g. `forall` as in MiniZinc language),
+*  binary decomposition of global constraints used in the model.    
+All constraints inhabiting the same *Constraint Type* share types of the arguments.
+
+*Constraint Type* is represented as a tuple $`\left \langle {ID}, \theta_s, \theta_t \right \rangle`$, where:
+*  $`Id`$ is unique type identifier
+*  $`\theta_s`$ and $`\theta_t`$ are type IDs of *Variable*/*Set* types, and represent what are the types of the constraint's arguments.
+
+Constraints are not first order citizens of the NDL language, and are only used as the labels in the Typed Constraint Graph.  
+
+## Labeling 
+
+Taking into consideration the types introduced in the previous section, the labeling of the Typed Constraint Graph is defined in the following way:
+*  $`\Sigma_V`$ contains all inhabitants of *Variable* and *Set* types defined in the problem
+*  $`\Sigma_A`$ contains all *Constraint Types* defined in the problem
+*  $`l_V`$ is an injective function
+*  the graph is well typed regarding to the constraints arguments, i.e. $`\forall a \in A \left(l_A(a) = \left \langle ID, \theta_s, \theta_t \right \rangle \implies \theta(s(a)) = \theta_s \wedge \theta(t(a)) = \theta_t \right )`$, where $`\theta`$ is a projection function mapping label to it's first element (type ID)
+
+
+
+