From The Twelf Project
(Redirected from Regular worlds)
Jump to: navigation, search

A world (or worlds) is a set of LF contexts.

The representation of an object language in LF is specified not just by an LF signature, but also by the world in which that signature is considered. This is because a representation that is adequate in one set of contexts may not be adequate in another. Similarly, a totality assertion about an LF type family may be true in one set of contexts but false in another.

Twelf includes a %worlds declaration that serves two purposes. First, it declares the world for which a totality assertion about a type family is proved. Second, it verifies that the constants inhabiting a type family stay within contexts in the specified world.

In Twelf, a world is specified by first defining a set of blocks using a %block declaration. A block is a pattern that describes a fragment of an LF context. Then a world is specified by a regular expression (b1 | b2 | ... | bn)* for blocks b1 through bn. This regular expression matches any LF context consisting of any number of these blocks in any order. Hence, Twelf supports the specification of regular worlds.

Specifying the world of a totality assertion

We can define natural numbers and a relation max that defines the larger of two natural numbers.

nat : type.
z : nat.
s : nat -> nat.

max : nat -> nat -> nat -> type.
mzz : max z z z.
mzs : max z (s N) (s N).
msz : max (s N) z (s N).
mss : max (s N1) (s N2) (s N)
      <- max N1 N2 N.

As discussed in the introduction article on Representing the judgments of the natural numbers, the type nat in this signature adequately represents the natural numbers only if the LF context does not contain variables of type nat.

Totality of max in the empty context

The judgement max defined in this signature is a total relation on natural numbers, or LF terms of type nat in the empty LF context. We specify this totality assertion in Twelf with the following declarations:

%mode max +N1 +N2 -N3.
%worlds () (max _ _ _).
%total T (max T _ _).
See Twelf's output

The %worlds declaration does not mention any blocks; the world ()* describes only the empty LF context.

Non-totality of max in an extended context

What happens if we consider max in an LF context that includes variables of type nat? (Note that in this world nat no longer represents the natural numbers.)

The following %block declaration defines the block random_nat, which allows such variables:

%block random_nat : block {x: nat}.

%mode max +N1 +N2 -N3.
%worlds (random_nat) (max _ _ _).

If we attempt to verify the totality assertion for max in these worlds, Twelf reports an error: max is not defined in the "natural numbers" arising from LF variables in the context.

%total T (max T _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Coverage error --- missing cases: {X1:nat} {#random_nat:{x:nat}} {X2:nat} |- max X1 #random_nat_x X2, {#random_nat:{x:nat}} {X1:nat} |- max #random_nat_x z X1, {#random_nat:{x:nat}} {X1:nat} {X2:nat} |- max #random_nat_x (s X1) X2.

%% ABORT %%

World checking

Up until this point, we have focused on the role of a %worlds declaration has in specifying a totality assertion. However, just as %mode both specifies the mode of a totality assertion and mode-checks a type family, %worlds both specifies the world of a totality assertion and world checks a type family.

What property does a world declaration specify? Intuitively, a world declaration for a type family circumscribes the contexts in which we consider inhabitants of that type family. For example, the world declaration for max says that we should only ever consider terms of type max in the empty LF context. Thus, it is a world error if some piece of Twelf code introduces a variable relevant to max. World checking ensures that we only consider a term in the contexts declared for its type.

When Twelf processes a %worlds declaration, it world checks each constant in the type family. A constant world checks under the following condition: whenever the ambient LF context is of the form specified by the world declaration, each premise of the constant occurs in an LF context that is within the world specified for the premise's type family.

Example world violation

For example, consider the following signature for the lambda-calculus:

exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

We define a height relation on open lambda-terms as a hypothetical judgement; note that the height rule for variables is represented as an LF assumption:

height : exp -> nat -> type.

height/lam : height (lam ([x] E x)) (s N)
              <- {x: exp} height x (s z) -> height (E x) N. 
height/app : height (app E1 E2) (s N)
              <- height E1 N1
              <- height E2 N2 
              <- max N1 N2 N.

If we try to declare height to be defined in the closed world, as we did for max, Twelf will fail with a World violation error message:

%worlds () (height _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%worlds () (height _ _). Error: While checking constant height/lam: World violation for family height: {x:exp} {_:height x (s z)} </: 1

%% ABORT %%

This is because height/lam adds variables to the LF context, so saying that the context should always be empty is wrong! Additionally, this world declaration is incorrect for another reason: the adequacy argument for exp says LF terms in contexts including variables of type tm adequately represent open object language terms; so if we wish height to represent a judgement on open terms, it must be declared in a world including such variables. Declaring height as above, even if it succeeded, would not capture the idea we have in mind that height is a relation on open terms.

Example world success

The correct world for this type family consists of blocks of the form defined in the following %block declaration called var-height. These blocks specify that whenever a new variable with type exp is added to the context, it is added along with a derivation of height x (s z). The type family height adequately represents the notion of height that we have in mind in this world. Moreover, it also world-checks in this world:

%block var-height : block {x: exp}{_: height x (s z)}.

%mode height +E -N.
%worlds (var-height) (height _ _).
See Twelf's output

Indeed, the type family is total in this world as well:

%total T (height T _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%total T (height T _).

%% OK %%

Subordination and world subsumption

It should be interesting that max can be called by height, even though height is defined for non-empty LF contexts. Technically, these contexts are not in the world for max, so the call to max from height would seem to be a world violation. However, Twelf knows, by keeping track of the subordination relation, that any var-height blocks can never change the canonical forms of nat or max. The Twelf server will print out the current subordination relation if you type in Print.subord. For the example above, this is the subordination relation:

%% OK %% Print.subord nat #> nat max #> max nat exp #> exp height #> height exp max nat %% OK %%

The line max #> max nat means that the canonical forms (i.e. the possible derivations) of max will not change unless the definitions of max or nat are changed. Because the block var-height does not add any declarations that are subordinate to either of these types, it is permissible to call max from within an LF context that includes blocks of the form var-height. This is an instance of what is called world subsumption, which is the criterion under which a type family in one world can be called from a type family in another.

See also