Go to the first, previous, next, last section, table of contents.

3 Syntax

In LF, deductive systems are represented by signatures consisting of constant declarations. Twelf implements declarations in a straightforward way and generalizes signatures by also allowing definitions, which are semantically transparent. Twelf currently does not have module-level constructs so that, for example, signatures cannot be named. Instead, multiple signatures can be manipulated in the programming environment using configurations (see section 11.1 Configurations).

The LF type theory which underlies LF is stratified into three levels: objects M and N, types A and B, and kinds K. Twelf does not syntactically distinguish these levels and simply uses one syntactic category of term. Similarly, object-level constants c and type-level constants a as well as variables share one name space of identifiers.

In explanations and examples we will use letters following the mathematical conventions above to clarify the roles of various terms. We also use U and V to stand for arbitrary terms.

3.1 Grammar

The grammar below defines the non-terminals sig, decl, term and uses the terminal id which stands for identifers (see section 2.2 Identifiers). The comments show the meaning in LF. There are various special declarations %keyword such as %infix or %theorem which are omitted here and detailed in the appropriate sections.

sig  ::=                       % Empty signature
       | decl sig              % Constant declaration

decl ::= id : term.            % a : K  or  c : A
       | defn.                 % definition, usually d : A = M
       | %abbrev adecl.        % abbreviation
       | %infix ixdecl.        % operator declaration
       | %prefix pxdecl.       % operator declaration
       | %postfix pxdecl.      % operator declaration
       | %name namepref.       % name preference declaration
       | %query qdecl.         % query declaration
       | %clause defn.         % clause definition
       | sdecl.                % solve declaration
       | %tabled id.           % table declaration
       | %querytabled qtdecl   % tabled query declaration
       | %deterministic ddecl. % deterministic declaration
       | %mode mdecl.          % mode declaration
       | %terminates tdecl.    % termination declaration
       | %reduces rdecl.       % reduction declaration
       | %block id : bdecl.    % block declaration
       | %worlds wdecl.        % worlds declaration
       | %total tdecl.         % totality declaration
       | %freeze ids.          % freeze declaration
       | %theorem thdecl.      % theorem declaration
       | %prove pdecl.         % prove declaration
       | %establish pdecl.     % prove declaration, do not use as lemma later
       | %assert callpats.     % assert theorem (requires Twelf.unsafe)
       | %use domain.          % installs constraint domain

defn ::= id : term = term      % d : A = M or d : K = A
       | id = term             % d = M or d = A
       | _ : term = term       % anonymous definition, for type-checking
       | _ = term              % anonymous definition, for type-checking

sdecl ::= %define binding sdecl % term binding
        | %solve id : term      % solve with proof term
        | %solve _ : term       % solve without proof term

ids   ::=                      % empty sequence
        | id ids               % identifier follwed by more

term ::= type                  % type
       | id                    % variable x or constant a or c
       | term -> term          % A -> B
       | term <- term          % A <- B, same as B -> A
       | {id : term} term    % Pi x:A. K  or  Pi x:A. B
       | [id : term] term      % lambda x:A. B  or  lambda x:A. M
       | term term             % A M  or  M N
       | term : term           % explicit type ascription
       | _                     % hole, to be filled by term reconstruction
       | {id} term           % same as {id:_} term
       | [id] term             % same as [id:_] term

The constructs {x:U} V and [x:U] V bind the identifier x in V, which may shadow other constants or bound variables. As usual in type theory, U -> V is treated as an abbreviation for {x:U} V where x does not appear in V. However, there is a subtlety in that the latter allows an implicit argument (see section 4.2 Implicit Arguments) to depend on x while the former does not.

In the order of precedence, we disambiguate the syntax as follows:

  1. Juxtaposition (application) is left associative and has highest precedence.
  2. User declared infix, prefix, or postfix operators (see below).
  3. `->' is right and `<-' left associative with equal precedence.
  4. `:' is left associative.
  5. `{}' and `[]' are weak prefix operators.

For example, the following are parsed identically:

   d : a <- b <- {x} c x -> p x.
   d : ({x} c x -> p x) -> b -> a.
   d : ((a <- b) <- ({x:_} ((c x) -> (p x)))).

3.2 Constructor Declaration

New type families or object constructors can be introduced with

condec ::= id : term.    % a : K or c : A

Here a stands for a type family and K for its kind, whereas c is an objects constructor and A its type. Identifiers are resolved as follows:

  1. Any identifier x may be bound by the innermost enclosing binder for x of the form {x:A} or [x:A].
  2. Any identifer which is not explicitly bound may be a declared or defined constant.
  3. Any uppercase identifier, that is, identifier starting with `_' (underscore) or an upper case letter, may be a free variable. Free variables are interpreted universally and their type is inferred from their occurrences (see section 4 Term Reconstruction).
  4. Any other undeclared identifier is flagged as an error.

3.3 Definitions

Twelf supports notational definitions and abbreviations. Semantically, both are completely transparent, that is, both for type checking and the operational semantics, definitions may be expanded.

adecl ::= id : term = term         % d : A = M
        | id = term                % d = M

defn ::= adecl.                    % definition
       | %abbrev adecl.            % abbreviation

where the second form of declaration is equivalent to id : _ = term. Definitions or abbreviations at the level of type families are permitted, but are somewhat experimental in the present release.

In order to avoid the expansion of defined constants as much as possible, declarations id : term = term. must be strict (see section 4.4 Strict Definitions). A definition of a constant c is strict if all arguments to c (implicit or explicit) have at least one strict occurrence (see section 4.3 Strict Occurrences) in the right-hand side of the definition, and the right-hand side contains at least one constant. In practice, most notational definitions are strict. For some examples, see section 3.6 Sample Signature and section 4.4 Strict Definitions. Twelf tries to preserve strict definitions as much as possible, instead of expanding them.

The %abbrev declaration defines an abbreviation which need not be strict. However, it will be expanded immediately upon parsing and will not be used in output.

The power of definitions in Twelf, however, is severely limited by the lack of recursion. It should only be thought of as notational definition, not as a computational mechanism. Complex operations need to be defined as logic programs, taking advantage of the operational semantics assigned to signatures (see section 5 Logic Programming).

3.4 Operator Declaration

The user may declare constants to be infix, prefix, or postfix operators. Operator precedence properties are associated with constants, which must therefore already have been declared with a type or kind and a possible definition. It is illegal to shadow an infix, prefix, or postfix operator with a bound variable. We use nat for the terminal natural numbers.

assoc ::= none   % not associative
        | left   % left associative
        | right  % right associative

prec ::= nat     % 0 <= prec < 10000

ixdecl ::= assoc prec id

pxdecl ::= prec id

decl ::= ...
       | %infix ixdecl.
       | %prefix pxdecl.
       | %postfix pxdecl.

During parsing, ambiguous successive operators of identical precedence such as a <- b -> c are flagged as errors. Note that it is not possible to declare an operator with equal or higher precedence than juxtaposition or equal or lower precedence than `->' and `<-'.

3.5 Name Preferences

During printing, Twelf frequently has to assign names to anonymous variables. In order to improve readability, the user can declare a name preference for anonymous variables based on their type. Thus name preferences are declared for type family constants. Note that name preferences are not used to disambiguate the types of identifiers during parsing.

namepref ::= id        % existential variables
           | id id     % existential variables, parameters

decl ::= ...
       | %name id namepref.

Following our same conventions, a name preference declaration has the form %name a id, that is, the first identifier must be a type family already declared and the second is the name preference for variables of type a. The second identifier must be uppercase, that is, start with a letter from `A' through `Z' or an underscore `_'. Anonymous variables will then be named id1, id2, etc.

In the second form, we can give a separate name preference for free (existential) variables and parameters. The second one will typically be lowercase, as in %name exp E x.

3.6 Sample Signature

Below is a signature for intuitionistic first-order logic over an unspecified domain of individuals and atomic propositions. It illustrates constant declarations and definitions and the use of operator precedence and name preference declarations. It may be found in the file `examples/guide/nd.elf'.

%%% Individuals
i : type.                   %name i T

%%% Propositions
o : type.                   %name o A

imp    : o -> o -> o.       %infix right 10 imp
and    : o -> o -> o.       %infix right 11 and
true   : o.
or     : o -> o -> o.       %infix right 11 or
false  : o.
forall : (i -> o) -> o.
exists : (i -> o) -> o.

not : o -> o = [A:o] A imp false.

%%% Natural Deductions

nd : o -> type.             %name nd D

impi    : (nd A -> nd B) -> nd (A imp B).
impe    : nd (A imp B) -> nd A -> nd B.
andi    : nd A -> nd B -> nd (A and B).
ande1   : nd (A and B) -> nd A.
ande2   : nd (A and B) -> nd B.
truei   : nd (true).
% no truee
ori1    : nd A -> nd (A or B).
ori2    : nd B -> nd (A or B).
ore     : nd (A or B) -> (nd A -> nd C) -> (nd B -> nd C) -> nd C.
% no falsei
falsee  : nd false -> nd C.
foralli : ({x:i} nd (A x)) -> nd (forall A).
foralle : nd (forall A) -> {T:i} nd (A T).
existsi : {T:i} nd (A T) -> nd (exists A).
existse : nd (exists A) -> ({x:i} nd (A x) -> nd C) -> nd C.

noti : (nd A -> nd false) -> nd (not A)
     = [D:nd A -> nd false] impi D.
note : nd (not A) -> nd A -> nd false
     = [D:nd (not A)] [E:nd A] impe D E.

Go to the first, previous, next, last section, table of contents.