Theory.md

 # Typed Constraint Graph
 
-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.
+In the heart of the NDL language lies a specific representation of the Constraint Programming Problems. Instead of using a common Constraint (Hyper-) Graph formalization, we introduce a Typed Constraint Graph (or TCG), that enriches the Constraint Graphs with types, representing the high 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_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_V`$ is a set of the vertex labels 
-* $`\Sigma_A`$ is a set of the arc 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 
+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 Typed Constraint Graph 
 
 ## Typing
 
@@ -21,7 +19,7 @@ There are three kinds of types in the Typed Constraint Graph, two related to ver
 
 ### 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:
+*Set Type* corresponds to a 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.
 
@@ -47,15 +45,37 @@ All constraints inhabiting the same *Constraint Type* share types of the argumen
 *  $`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.  
+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_V = \Sigma_\mathit{var} \cup \Sigma_\mathit{set}`$, where $`\Sigma_\mathit{var}`$ contains all inhabitants of *Variable* types and $`\Sigma_\mathit{set}`$ contains all inhabitants of the *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)
+*  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)
+
+Additionally, for every *Variable* type identifier $`\mathit{id}`$ we define a set of its' inhabitants $`\Theta_\mathit{id} = \left \{ \left \langle ID, I_1, \ldots I_n \right \rangle \in \Sigma_\mathit{var} : ID = \mathit{id} \right \}`$.
+
+# Neighborhood Definition Language
+
+NDL language was designed to be a small Domain Specific Language, allowing to exploit information encoded in the Typed Constraint Graph to modify an existing problem solution in an intelligent manner.
+
+## Solution
+
+Solution $`\mathit{sol}`$ is an assignment of all the variables to the values from their corresponding domains. Set of all possible solutions will be written as $`\mathit{Sol}`$.
+
+For every *Variable* type with identifer $`id`$, we define following set of functions to manipulate the solution:  
+*   $`\mathit{get}: \mathit{Sol}, \Theta_{id} \rightarrow D(id)`$
+
+
+## Turing Incompleteness
+
+Due to lack of unbounded recursion, the NDL is **not** Turing complete. Every program written in NDL is total and will always eventually end. 
+
+## Independence from TCG
+
+Programs written in the Neighborhood Definition Language are independent of the specific problem instance (specifically: domains, index sets and the TCG structure) and depend only on the types occurring in the problem, as the pattern matching refers to the labels in the underlying TCG.