Typed Constraint Graph
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 selfloops. Formally, it's an 8tuple 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
andt
are both mapsA \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 
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 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 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.
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 thek
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 = \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)
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.