Beluga Syntax

We discuss on a high-level the idea behind Beluga's concrete syntax. Beluga is a two-level system: 1) it supports specifications of formal systems in the logical framework LF 2) it supports programming with LF specifications. Hence, Beluga programs consist of two kinds of declarations: LF constant declarations and computation-level declarations.

sig ::=                   % Empty signature
     | lf_decl sig        % LF constant declaration
     | c_decl  sig        % Computation-level constant declaration

Warning:

Beluga is a protype and work in progress. As such, some of the subtleties in the syntax may still change over time. While we try to ensure backwards compatibility, this may not always be possible.
This description of the source-level syntax for Beluga below is not exhaustive. It tries to provide a high-level description and intuition for Belgua programs.

LF declarations

LF declarations in Beluga follow closely the syntax used in the Twelf system. There are however a few differences which we will mention below.

lf_decl ::= id : term.         % a : K  or  c : A
       | %name id id.          % name preference declaration

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            % lambda x. M 
       | term term             % A M  or  M N
       | _                     % hole, to be filled by term reconstruction

The constructs {x:U} V and \x. 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.

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

Juxtaposition (application) is left associative and has highest precedence.
-> is right and <- left associative with equal precedence.
: is left associative.
{} and \ are weak prefix operators.
Bound variables and constants must be written with lower-case letters.
Free variables can be written with upper-case letters or lower case letters; but we use the convention to write them with upper-case letters.
All terms need to be written in beta-normal form, i.e. no redeces can occur in terms. However, variables do not need to be eta-expanded.

Next, we give a few simple examples illustrating what terms Beluga parses and which ones it does not. For example, the following are parsed identically:

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

The following term parses:

      d : p x <- a <- b <-  c x.  % against our convention but parses
      d : p X <- a <- b <-  c X.  % Better code: uses convention 

      P:term -> type              % Parse error

The following will not parse:

  d: p ((\x.x) a) .    % this will give an error since there is a redex
  d: p a.              % this will parse.

More differences to Twelf syntax: We summarize a few more differences here. These restrictions may be addressed in the future.

Lambda-abstractions cannot be annotated with the type of the input. Writing \x:nat.x is illegal in Beluga.
Omitting the type in a Pi-type is illegal in Beluga. One cannot simply write ({x}foo x T) -> foo E T'.. One must give the type of the variable x.
We do not at this point support arbitrary type annotations, i.e. one cannot write M : A.

Computation-level declarations

In addition to LF declarations, we support three additional kinds of declarations: schema declarations, which describe the structure of contexts, declarations of recursive functions (including mutual recursive functions), and value declarations.

c_decl ::= 
       | schema ctx_schema;            % schema declaration
       | rec_prog ;                    % recursive programs
       | let id = exp ;                % computation-level variable declaration


rec_prog ::= rec id : c_typ = exp      % recursive program id 
       | rec_prog and id : c_typ = exp

To embed LF terms into computations, we extend the LF term language to support contextual variables and projections on bound variables and contextual variables. These extensions cannot be used when declaring an LF signature, but only when we use LF objects within computation-level programs and declarations.

% Terms
term ::=  .. 
        | id . k               % k-th projection of a bound variable x
        | cvar sigma           % contextual variable    
        | block s_decl . term  % Sigma x:A.B

s_decl ::= id:term | s_decl , id_term

% Contextual variable

cvar   ::= 
        | id                % context variable, meta-variable 
        | #id               % parameter variable 
        | #id . k           % proj_k 

% Substitutions 

sigma ::= 
      |                     % Nothing denotes the empty substitution
      | ..                  % Identity substitution
      | sigma term          % substitution sigma , M

We impose the following restrictions:

Context variables always occur on their own (i.e. sigma is always empty).

Schemas and Contexts

Schemas classify context. We allow contexts to be built up not only by single declarations, but also by Sigma-types, i.e. dependent tuples. Logically, this means we can have not only atoms in our context, but also conjunctions of atoms (where the conjunction corresponds to the Sigma-type type-theoretically).

% Schema
ctx_schema  ::= term | some [some_decls] block decls
some_decls  ::=                    % NOTHING
            | id:term              % Single declaration
            | id:_term, some_decls % Multiple declarations
decls       ::= . term             % Single declaration
            | {id:term}decls       % Multiple declarations  

% Context
ctx         ::=                    % NOTHING denoting the empty context
            | id                   % Context variable
            | x:block_type         % Context with one declaration x:block_type
            | ctx, id:block_type   % Psi, x:block_type  

block_type ::= term                % Single type
            | block decls          % Sigma-type.

A ctx_hat is a context where we erase the type declarations.

ctx_hat ::= 
        | id                      % Context variable or variable name
        |                         % NOTHING denoting the empty context
        | ctx_hat, id             % psihat, x

Computation-level types

% Computation-level Types
c_typ   ::= 
        | term [ctx]               % Contextual type A[Psi]
        | c_typ -> c_typ           % Functions
        | {id::term[ctx]} c_typ    % Dependent function type U::A[Psi]} tau
        | {id:ctx_schema} c_typ    % Implicit quantification over context variables 
        | {id:(ctx_schema)*} c_typ % Explicit quantification over context variables

In the order of precedence, we disambiguate the syntax:

-> is right associative.
: is left associative.
{} and \ are weak prefix operators.
Bound LF variables and constants must be written with lower-case letters.
Free meta-variables must be written with upper-case letters.
Context variables are written with lower-case letter.
All LF terms need to be written in beta-normal form, i.e. no redeces can occur in terms. LF terms occurring as part of a contextual object must be written in eta-expanded form. For example, one must write [g] lam \x.E .. x and writing [g] lam E is currently rejected.
In the contextual type A[Psi], the type A must be a base type. This can always be achieved by translating a type (B -> A)[Psi] to A[Psi,x:B]. By applying this translation, any function type can be lowered.

Computation-level Expressions

exp    ::= 
       | [ctx_hat] term                % Contextual object: [g] M
       | [ctx] term                    % Contextual object where we provide
                                       % the full context as a type annotation
       | FN id => exp                  % Context abstraction FN g => e
       | fn id => exp                  % Computation-level functions: fn x => e 
       | mlam id => exp                % Abstraction over dependent type argument
       | exp exp                       % Application: e1 e2
       | exp [ctx]                     % Context application: e [g]
       | exp A < ctx_hat . term >      % Application of a dependent argument
       | exp A < ctx . term >          % Application of a dependent argument
                                       % with full context as type annotation
       | let [ctx] term = exp in exp   % Let expression
       | case exp of branch | .. | branch


% Branches
branch ::= 
       | delta  [ctx] term => exp
       | delta  [ctx] term : term[ctx] => exp   
                                       % with explicit type annotation on pattern

% Declarations of contextual variables
delta  ::= 
       |                               % NOTHING
       | {id::block_type[ctx]}         % Single contextual declaration
       | {id:(schema)*}                % Single context variables declaration
       | delta, {id::block_type[ctx]}  % Contextual declaration
       | delta, {id:(schema)*}         % Quantification over context variables

The constructs {X::A[Psi]} tau the identifier X must be an upper-case letter. It may overshadow other contextual variables in tau. Note that A[Psi] -> tau is NOT just an abbreviation for {X::A[Psi]} tau . where X does not appear in tau. On the computation-level we retain the difference between quantification and implication. It is however worth noting that there is a simple translation between programs of these two types which involves lifting universally quantified elements to become proper stand-alone computation-level expressions.

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

Juxtaposition (application) is left associative and has highest precedence.
Bound variables and constants must be written with lower-case letters.
Free meta-variables must be written with upper-case letters.
All LF terms need to be written in beta-normal form, i.e. no redeces can occur in terms. LF terms occurring as part of a contextual object must be written in eta-expanded form. For example, one must write [g] lam \x.E .. x and writing [g] lam E is currently rejected.

Emacs mode

There is an emacs mode for Beluga, which is distributed with the Beluga code and example base. This will display the the source-syntax in a nicer format.

Beluga

Computation and Logic Group School of Computer Science McGill University