%mode

From The Twelf Project
Jump to: navigation, search

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.

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