# %mode

The ** %mode** declaration specifies the way in which a relation is intended to be used, by specifying those arguments that are

*inputs*or

*outputs*. Twelf then checks that all constants defining the relation respect the mode specified (are "well-moded").

The `%mode` declaration is an important part of the specification of a totality assertion. In the "for all/exists" statement about a relation, the "for all" terms are the input arguments to the relation, and the "exists" terms are its outputs.

## Contents

## Syntax

A mode declaration for the family *id* with *n* arguments usually takes the following ("short") form:

`%mode id a1 ... an.`

Each argument `ai` is `+`*ID*, `-`*ID*, or `*`*ID* for some distinct identifier *ID*. `+` indicates that the argument is an input, `-` that it is an output, and `*` that the argument is unrestricted. (The `*` mode is rarely used.) For example, a natural mode for the `plus` relation on natural numbers is:

plus : nat -> nat -> nat -> type. %mode plus +N1 +N2 -N3.

The names `N1`..`N3` are arbitrary, but each must be distinct.

### Full form

The short mode declaration above only specifies the mode for explicit parameters; the modes for implicit parameters are then assigned automatically. Occasionally, one needs to use a "full" form to specify the modes of implicit parameters:

%mode p1 ... pm term.

Each parameter `pi` is `+{`*ID*` : term}`, `-{`*ID*` : term}`, or `*{`*ID*` : term}` for distinct identifiers *ID*. Terms may refer to the variables bound in the previous parameters. For example, the full mode declaration corresponding to the short one above would be:

plus : nat -> nat -> nat -> type. %mode +{N1:nat} +{N2:nat} -{N3:nat} plus N1 N2 N3.

This article or section needs an example where the full mode specification is actually needed. |

## Mode checking

### Basic mode checking errors

Say we give a definition of the natural numbers with addition in line with the descriptions above:

nat: type. z: nat. s: nat -> nat. plus: nat -> nat -> nat -> type. %mode plus +N1 +N2 -N3. pz: plus z N N. ps: plus (s N1) N2 (s N3) <- plus N1 N2 N3.

The input of plus is the first and second positions, and the output of plus is the third position, which means that for any ground objects in the first and second positions, there must only be a ground object in the third position. If one of the output arguments is not forced to be a ground, which would be the case if the output of plus no longer matched the output of the subgoal, then

px: plus (s N1) N2 (s N) <- plus N1 N2 N3.

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)px : {N1:nat} {N2:nat} {N3:nat} {N:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N). Error: Occurrence of variable N in output (-) argument not necessarily ground

%% ABORT %%

Another problem occurs when the *inputs* to a subgoal are not known to be ground, which would happen if we mis-named one of the inputs to the subgoal.

py: plus (s N1) N2 (s N3) <- plus N N2 N3.

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)py : {N:nat} {N2:nat} {N3:nat} {N1:nat} plus N N2 N3 -> plus (s N1) N2 (s N3). Error: Occurrence of variable N in input (+) argument not necessarily ground

%% ABORT %%

### Ordering subgoals

Mode checking considers subgoals *in order*, i.e. from top to bottom when the subgoals are written out in the standard style using backwards arrows. The order of subgoals matters very much for mode checking. Say we have an identity function that maps inputs (the first position) to outputs (the second position).

id: nat -> nat -> type. %mode id +N1 -N2. id/refl: id N N.

The rule `ps'` below passes the mode checker, because the call to `id` takes the ground argument `N1` and creates a ground output `N1'`, which is then used in the derivation for `plus N1' N2 N3`.

ps': plus (s N1) N2 (s N3) <- id N1 N1' <- plus N1' N2 N3.

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)ps' : {N1':nat} {N2:nat} {N3:nat} {N1:nat} plus N1' N2 N3 -> id N1 N1' -> plus (s N1) N2 (s N3).

%% OK %%

However, if we reverse the order of the two subgoals, even though the result is logically equivalent, Twelf considers `plus N1' N2 N3` before `id N1 N1'`, and so does consider `N1'` to be ground when it encounters it; thus, complaining accordingly:

ps': plus (s N1) N2 (s N3) <- plus N1' N2 N3 <- id N1 N1'.

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)ps' : {N1:nat} {N1':nat} {N2:nat} {N3:nat} id N1 N1' -> plus N1' N2 N3 -> plus (s N1) N2 (s N3). Error: Occurrence of variable N1' in input (+) argument not necessarily ground

%% ABORT %%

This article or section needs a more complete description of more interesting mode checking problems. |

## See also

- Modes in the User's Guide
- Proving totality assertions about the natural numbers in the tutorial Proving metatheorems with Twelf, particulary the section on Mode.