%name

A %name declaration allows us to direct STELF to name unnamed variables in a certain way, which can make it much easier to understand STELF’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 (guide §3.5).

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:

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term plus/z plus z N N %.
%term plus/s %pi (plus (s N1) N2 (s N3)) %<- (plus N1 N2 N3) %.

If we give STELF 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, STELF considers the second type to be an “anonymous” (or universally quantified) variable. If STELF is given no other information, it will automatically name all anonymous variables X1, X2, etc…

%define _ plus/s (plus/s plus/z) %.

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 STELF a different prefix for anonymous variables of different types using the %name declaration.

%name nat %.

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, STELF will change the prefix of anonymous variables from X to whatever was defined in the %name declaration.

%define _ plus/s (plus/s plus/z) %.

Example 2: Call-by-name lambda calculus

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

%sort exp %.
%term lam %pi (%pi exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.
%sort step {_ exp} {_ exp} %.
%term step/app %pi (step (app E1 E2) (app E1' E2)) %<- (step E1 E1') %.
%term 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.

%define _ step/app (step/app step/appabs) %.

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

%name exp %.
%define _ step/app (step/app step/appabs) %.

See also

• Name preferences (guide §3.5)