Previous Up Next

11  Concrete syntax

Although the concrete syntax of Bedwyr was originally derived from that of λProlog in the Teyjus implementation[NM99], it has now evolved in such a way that, by design, it resembles that of the Abella proof assistant [Gac10]. This explains the lack of syntactic compatibility with versions earlier than 1.3.

11.1  Formulae

Formulae are described in 5, separately from terms, as it is customary to have the former contain the later and not the other way around. However, one can actually write ((x\ (p x /q x)) c) instead of (p c /q c), and the parser takes it into account by allowing a formula to be interpreted as a term.

Quantifiers are n-ary, and their scope extends to the right as far as possible:

(forall x yf y x = g x y)(forall x y, (f y x = g x y))

formula::=<term> = <term>equality
 |<formula> /\ <formula>conjunction
 |<formula> \/ <formula>disjunction
 |<formula> -> <formula>implication
 |<quantifier> <bound_variable>+ , <formula> 
quantifier::= foralluniversal
 | existsexistential
 | nablageneric
Figure 5: Grammar of formulae.

11.2  Terms

Within terms, the highest priority goes to the regular application (6). In particular, it has precedence over the application of an infix constant:

(w x ** y z)(w x** (y z)

All infix constants have the same priority, and are right-associative, to mimic the behavior of ->.

An infix constant usually has to be at least of arity 2 to be read: (x **) raises a parsing error, while (x ** y) can be applied to another term if ** is of arity 3 or more. It is also possible to use the prefix version of an infix constant by surrounding it with parentheses, in which case any arity is permitted: ((**x) and ((**x y z) are both syntactically legal.

The abstraction over variable x in term is denoted by xterm – which is read as λ x. term. The scope of the infix λ-abstraction extends to the right as far as possible inside of a term, but not across formula operators:

(xyf y x = g x y)((x\ (y\ (f y x))) = (g x y))

 |<atom>* <abstraction>application on an abstraction
 |<term> <infix_id> <term>(partial) infix application
abstraction::=<bound_variable> \ <term> 
atom::= true prop
 | false prop
 | "<string>" string
 |[0-9]+ nat
 | (<formula> ) 
 | (<infix_id> )prefix form of an infix constant
 |<id>declared object
 |<bound_variable>bound (or free) variable
Figure 6: Grammar of terms.

11.3  Tokens

Names for objects such as types, predicates, constants and variables are character strings built with letters, digits and the special characters { -^<>=~+*&:|}, { `'\$?} and { _/@#!} (7). Names must be separated by space characters (SPACE, TAB, CR, LF), parentheses or C-style inline nested comments ( /* */). As a general rule, the first character of a name determines the kind of name it is, and cannot be a digit.

More precisely, we divide the special characters into three categories:

which gives us three token categories:

upper names
start with A- Z; contain any letter, digit, prefix character or tail character (i.e. anything but an infix): Foo?0, B@r, My_Var'
prefix names
start with a- z or a prefix character; contain any letter, digit, or prefix or tail character (i.e., anything but an infix): l33t, h#sh, ?Your_Var
infix names
contain only infix characters: -->, |=, ^^

Keywords are implicitly excluded from those definitions.

Types and predicates must have prefix names, constants can have either prefix or infix names, and bound variables (from quantifiers of λ-abstractions) can have either upper or prefix names, though it is customary to use an upper name for an existentially quantified variable and a prefix name for the others.

In a term or a type, all unbound infix or prefix names must be declared, and unbound upper names (which cannot be declared objects) are free variables. Those are implicitly universally quantified in files (i.e. in types and clauses), and existentially quantified in queries. Though no name can begin with the special character _2, it can serve as a placeholder: it is a fresh one-time free variable, except when used instead of a variable name in a binding, where it denotes a vacuous abstraction.

One more constraint restrict the range of names. As already said, names must be separated by space characters or comments. This is true even if they are not names of the same kind, e.g. infix characters and other characters cannot be contiguous. This explains why the spaces are mandatory in (X -> Y) or even (X = Y). The only allowed exceptions are the special sequences /* and */, which can appear right after (resp. before) a prefix name, and which always start (resp. end) a level of inline comment3, except when in a quoted string or a single-line comment.

upper_name::= [ A-Z][ a-zA-Z0-9`'\$?_/@#!]*
prefix_name::= [ a-z`'\$?][ a-zA-Z0-9`'\$?_/@#]*
infix_name::=[ -^<>=~+*&:|]+
Figure 7: Grammar of type declarations.

Previous Up Next