# mOTTR: Concepts and Abstract Model for OTTR

top

examples:
/

#### Table of Contents

# Concepts and Abstract Model for OTTR (mOTTR)

**
Specification of the concepts and abstract model of OTTR templates.
**

- Version
- PRE-0.1
- Authors
- Leif Harald Karlsen

Martin G. Skjæveland - Issues
- https://gitlab.com/ottr/language/mOTTR/issues

**Notation**

This is a *defined term*.

This is a mention of a defined term.

## 1 Fundamentals

### 1.1 Types

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.

There is a type named *Top*, which is supertype of every other type,
and a 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<P>** for all types **P**.

For every non-list type **P** there is also a type **Sub<P>**,
such that **Sub<P> subtype P** and **Sub<Sub<P>> = Sub<P>**.

*Compatible* is the least relation between types such that

**P**is compatible with all supertypes of**P**.**Sub<P>**is compatible with all subtypes of**P**.

### 1.2 Terms

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<Sub<P>>** where
**P** is the **subtype**-least type such that each element's type is subtype of **P**.

No term has type **Bot**.

### 1.3 Templates

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

### 1.4 Template instances

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.

Any argument with an associated list expander
must be compatible with a type of the form **List<P>** or **NonEmptyList<P>**, where
**P** is a type. All list expanders contained in the parameter
list must have the same token.

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

## 2 Collections of templates and instances

### 2.1 Template library and dataset

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.

#### Consistent use of terms

For a term **v**, we say that **v** has *inferred type* **P** if:

**v**is an argument with a corresponding parameter with type**P**, or**v**occurs in a list term which has inferred type either**NonEmptyList<P>**or**List<P>**.

A term **v** is *consistently typed* in a set of instances
if there exists a type **P** unequal **Bot** such that

**P**is a subtype of all inferred types of**v**, and- the type of
**v**is compatible with**P**.

A set of instances is consistently typed if every term occing in it is consistently typed.

A template library is *consistently typed*
if every term occuring in the library is consistently typed
if the set of all instances occuring in it is consistently typed.

A template library is called *variable safe* if

- no variable occurs in two different templates in the library;
- no template has a variable which equals a constant used in a template which it depends upon;

#### Correct instantiation of templates

*Directly depends* is a relation between a set of templates and a
set of template signatures such that **T** directly depends on **S** if
an instance of **S** occurs in the pattern of **T**.

A template library is *acyclic* if the
direcly depends relation is *acyclic*.

A set of instances is said to have *referential integrity*
with respect to a template library
every instance has a name corresponding to a template signature
in the library, and that the arity of the instance
equals the arity of the corresponding template signature.

A template library is said to have *referential integrity*
if no two templates have the same name and the set of
all instances occuring in it has *referential integrity*
with respect to it.

### 2.2 Valid template library

A *valid template library* is a template library that:

- is consistently typed,
- is variable safe,
- is acyclic, and
- has refential intergrity.

### 2.3 Valid template dataset

A *valid template dataset* is a template dataset where:

- its template library is valid, and
- its set of instances is consistently typed and has refential 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.

## 3 Expansion

### 3.1 Instance Expansion

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

if one or more arguments of

**I**has a list expander, we generate new instances of**T**from**I**by considering every argument without a list expander as a singleton list containing its argument value, and then applying an operation determined by the list expander on the lists in the 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.- 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. - 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**. otherwise, we build the

*induced substitution*by considering each argument**S**of**T**and**I****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**.- if

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 base template—in which case the expansion naturally terminates, or
- it is underspecified, which occurs in two cases:
- an argument has a variable as value and has a list expander, or
- 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.

### 3.2 Template Expansion

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.