%name

From The Twelf Project
Jump to: navigation, search

A %name declaration allows us to direct Twelf to name unnamed variables in a certain way, which can make it much easier to understand Twelf's output. Using a %name declaration is never required, but it often makes the task of proving metatheorems significantly easier. More information can be found in the section on name preferences in the User's Guide.

Two examples show the use of %name - the first shows its use to give a default name for universally quantified variables, and the second example shows its use to give a default name for both universally quantified variables and bound variables.

Example 1: Natural numbers

We start with a standard presentation of unary numbers and addition:

nat : type.

z : nat.
s : nat -> nat.



plus : nat -> nat -> nat -> type.

plus/z : plus z N N.

plus/s : plus (s N1) N2 (s N3) <- plus N1 N2 N3.


If we give Twelf a derivation, but do not give it information about the type of that derivation, it will infer the type. In order to return the most general possible type, Twelf considers the second type to be an "anonymous" (or universally quantified) variable. If Twelf is given no other information, it will automatically name all anonymous variables X1, X2, etc...

_ = plus/s (plus/s plus/z).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

_ : {X1:nat} plus (s (s z)) X1 (s (s X1)) = [X1:nat] plus/s (plus/s plus/z).

%% OK %%


These type reconstructions can become rather complicated, particularly when we are dealing with metatheorems that have multiple types. A good way to deal with this complexity is by giving Twelf a different prefix for anonymous variables of different types using the %name declaration.

%name nat N.


This identifier must start with an uppercase letter, and often only a single uppercase letter suffices; however, any identifier starting with an uppercase letter works. Given this information, Twelf will change the prefix of anonymous variables from X to whatever was defined in the %name declaration.

_ = plus/s (plus/s plus/z).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

_ : {N1:nat} plus (s (s z)) N1 (s (s N1)) = [N1:nat] plus/s (plus/s plus/z).

%% OK %%

Example 2: Call-by-name lambda calculus

We can also use the %name declaration to define the default name for bound variables.

exp : type. 

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



step : exp -> exp -> type.

step/app : step (app E1 E2) (app E1' E2) <- step E1 E1'.

step/appabs : step (app (lam E1) E2) (E1 E2).


The default prefix for universally quantified variables is again X. Also, observe that the default prefix for bound variables is x.

_ = (step/app (step/app step/appabs)).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

_ : {X1:exp -> exp} {X2:exp} {X3:exp} {X4:exp} step (app (app (app (lam ([x:exp] X1 x)) X2) X3) X4) (app (app (X1 X2) X3) X4) = [X1:exp -> exp] [X2:exp] [X3:exp] [X4:exp] step/app (step/app step/appabs).

%% OK %%


This %name declaration causes no output from Twelf, but it changes the prefixes of universally quantified and bound variables to E and e, respectively.

%name exp E e.

_ = (step/app (step/app step/appabs)).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

_ : {E1:exp -> exp} {E2:exp} {E3:exp} {E4:exp} step (app (app (app (lam ([e:exp] E1 e)) E2) E3) E4) (app (app (E1 E2) E3) E4) = [E1:exp -> exp] [E2:exp] [E3:exp] [E4:exp] step/app (step/app step/appabs).

%% OK %%

See also