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.
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 y, f y x = g x y)≡
(forall x y, (f y x = g x y))
formula ::= <term>
equality | <formula>
conjunction | <formula>
disjunction | <formula>
implication | <quantifier> <bound_variable>+
| <term> quantifier ::=
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
The abstraction over variable
x\ term – 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:
(x\ y\ f y x = g x y)≡
((x\ (y\ (f y x))) = (g x y))
term ::= <atom>+ application | <atom>* <abstraction> application on an abstraction | <term> <infix_id> <term> (partial) infix application abstraction ::= <bound_variable>
prefix form of an infix constant | <id> declared object | <bound_variable> bound (or free) variable
Names for objects such as types, predicates, constants and variables are
character strings built with letters, digits and the special characters
(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:
Z; contain any letter, digit, prefix character or tail character (i.e. anything but an infix):
zor a prefix character; contain any letter, digit, or prefix or tail character (i.e., anything but an infix):
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
(X -> Y) or even
(X = Y). The only
allowed exceptions are the special sequences
*/, 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.
id ::= <prefix_name> | <infix_name> bound_variable ::= <upper_name> | <prefix_name> type_variable ::= <upper_name> infix_id ::= <infix_name> upper_name ::= [
prefix_name ::= [
infix_name ::= [