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>.

We will 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>.

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

The set of constants include a special constant called none that denotes a missing value. The set of constants include lists which are ordered collections of terms. The constant nil denotes the empty list.

All constants have a type. The type of nil is List<Bot>, and the type of nonempty lists is NonEmptyList<LUB<Top>>. none has the type Bot and is the only constant with this type.

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.

Note: This specification does not say when two occurrences of a term are occurrences of (or represent) the same term. Such rules must be fixed by specifications that adapt mOTTR to a concrete representation of terms. It is in particular relevant for blank node scopes [2].

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 parameter name, which is a constant term, it may have a default value, which is a constant term, and it may 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 and all parameter names in a signature's list of parameters must be different.

A parameter variable belongs to the signature which declares it: two different signatures never have the same variable, and a variable does not occur outside the signature declaring it or, if the signature is a template, its pattern. A specification adapting this model to a concrete representation of terms must respect this, whatever notation it gives variables; in particular, two signatures written with the same notation for a variable declare two different variables.

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 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.

An argument with a list expander must have a value whose type is compatible with List<P> or NonEmptyList<P>, where P is the type of the corresponding parameter. List expander operations are defined on lists only.

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 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 are constructed as follows: The operation corresponding to the list expander (see below) is performed on all lists with a list expander, and for each list e in the result, an instance is created such that its i*th argument is equal to *I's if it does not have a list expander and equals the i*th element of *e otherwise. The operation corresponding to a list expander is as follows:

   • if the list expander is cross, the operation is the Cartesian 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 by appending none-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 value none 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 value none 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.