We assume that we have a set of types. Types are arranged by subtype relationships, where subtype is a reflexive and transitive relation over the set of types. Supertype is the inverse relationship of subtype.

A type is either a basic type, a list type or a LUB-type.

There is a basic type named Top, which is supertype of every other type, and a basic type named Bot which is subtype of every other type.

There are two list types List and NonEmptyList which take another type as argument. We assume that there is one type List<P> and one type NonEmptyList<P> per other type P. NonEmptyList<P> is a subtype of List<Q> for all types P and Q where P is a subtype of Q.

For every basic type P there is also a LUB-type LUB<P>, (least upper bound) such that LUB<P> subtype P.

Compatible is the least relation between types such that

• P is compatible with all supertypes of P.
• LUB<P> is compatible with all subtypes of P.

We define the occurs at depth as follows, for any types P and Q:

• P occurs at depth 0 in P
• if P occurs at depth n in Q, then P occurs at depth n+1 in List<Q> and NonEmptyList<Q>.

For example P occurs at depth 2 in NonEmptyList<List<P>>. We are only going to use this definition in order to relate depths of terms in lists to the type at corresponding depths in complex list types. However, note that for LUB<P>, P must be a basic type and can therefore not be a list type. It is therefore no n such that P occurs at depth n in LUB<P>, but e.g. LUB<P> occurs at depth 1 in NonEmptyList<LUB<P>>.

We assume that there are two sets, constants and variables, which are possibly overlapping. We call the union of these the sets terms.

The set of constants include lists which are ordered collections of terms. The constant nil denotes the empty list. The type of nil is List<Bot>, and the type of nonempty lists is NonEmptyList<LUB<Top>>.

No term has type Bot.

We define the occurs at depth over terms similarly as for types:

• a term a occurs at depth 0 in a,
• if a term a occurs at depth n in b, then a occurs at depth n+1 in any list where b is a member.

A template signature (or just signature) consists of a template name, which is a constant term, and a list of parameters.

A parameter consists of a parameter variable, which is a variable term, and a type. Additionally, a parameter may have a default value which is a constant term and be marked with one or more modifiers. The set of modifiers contains optional.

The arity of a signature is the size of its parameter list.

The type of a variable is the type of its parameter.

All parameter variables in a signature's list of parameters must be different.

Additionally, a template signature may be have annotations, which is a set of ground template instances (to be defined below); we call these annotation instances.

A template is a template signature with a pattern, which is a (possibly empty) set of template instances (to be defined below); we call these pattern instances.

A base template is a specific type of template signature that may not have a pattern.

A template instance (or just instance) consists of a template name and a list of arguments.

An argument consists of possibly an argument value (or just value), which is a term, and possibly a list expander.

The set of list expanders contains the tokens cross, zipmin and zipmax.

The arity of an instance is the size of its argument list.

A ground template instance is a template instance where the value of every argument, if present, is a constant.

We say that a template instance I is the instance of a template signature T with the same template name as I. For an argument a in instance I of signature T, we say that its corresponding parameter of T is the parameter with the same index in the parameter list as the index of a in the argument list of I.

A template library is a set of template signatures. (Note that templates and base templates are also template signatures.)

A template dataset consists of a template library and a set of ground template instances.

A semi-valid template library is a template library that:

• is consistently typed,
• is variable safe,
• is acyclic, and
• has referential integrity.

A valid template library is a semi-valid template library that is well founded.

A valid template dataset is a template dataset where:

• its template library is valid, and
• its set of instances is consistently typed and has referential integrity with respect to the template library.

A strict template dataset is a valid template dataset with the additional requirement that ground template instances must have value for arguments to corresponding parameters which are marked as optional.

The direct expansion of a template instance I of T is defined as follows:

1. if one or more arguments of I has a list expander, new instances of T from I in 2-step process:
   1. First, arguments are preprocessed:
      • an argument without a list expander treated as a singleton list containing its argument value,
      • an argument with no value and with a list expander is treated as just an argument with no value (the list expander is removed),
      • other arguments are left as-is.

   2. Then, an operation determined by the list expander is applied to argument list of I:

      • if the list expander is cross, the operation is the Cartisian product
      • if the list expander is zipmin, the operation is Convolution - stopping after the length of the shortest list
      • if the list expander is zipmax, the operation is Convolution - increasing the length of shorter lists to the length of the longest list, but appending no values.

      The result of the direct expansion of I is the union of the direct expansion of all the generated instances.

2. if one or more arguments of I has no value and its corresponding parameter is not optional and has no default value, then the result of the direct expansion of I is the empty set.
3. if T has no pattern, i.e., T is a base template or a signature (and not a template), then the direct expansion of I is I.

4. otherwise, we build the induced substitution S of T and I by considering each argument a of I and its corresponding parameter p in T:

   • if a has no value and p has a default value d, then S := S ∪ { p / d }
   • otherwise, S := S ∪ { p / a }

   The result of the direct expansion of I is the set of instances resulting from applying the substitution S to the pattern of T.

The expansion of an instance I of a signature T is the result of recursively applying direct expansion on I until each instance is either:

• an instance of a template without a pattern—in which case the expansion naturally terminates, or
• it is underspecified, which occurs in two cases:
  1. an argument has a variable as value and has a list expander, or
  2. an argument has a variable as value and the parameter to which the variable belongs is marked optional while the argument's corresponding parameter is not optional or has a default value.

The expansion of a template dataset is the expansion of the set of instances of the dataset, with respect to the signatures in the corresponding template library.

We call an expansion complete, if the result contains only instances of base templates or signatures.

We call an expansion ground, if the result contains only instances of base templates.

The annotation expansion of a template signature is the result replacing the annotation instances of the template signature with their expansion.

The pattern expansion of a template is the result replacing the pattern instances of the template with their expansion.

The expansion of a template is the result of performing both annotation expansion and pattern expansion on the template.