Arend's specification syntax is based on Prolog, but is more flexible, with fewer predefined operators.

#Lexical syntax

Arend's lexical syntax is largely defined in terms of Unicode character categories. Only a few characters are treated specially.

Whitespace is ignored, but required to separate some tokens. Comments normally count as whitespace.

Comments come in two forms:

// Single-line comment
/* Multi-line comment */

Tokens are broken into three groups:

• Atomic tokens start with a lowercase alphabetic (Ll or Lo) or numeric (Nd, Nl, or No) character, and are followed by any contiguous sequence of zero or more non-separator (see below) characters. As a special case, the empty list [] is considered to be an atomic token.

• Variable tokens start with an uppercase (Lu) alphabetic character or an underscore, and are followed by any contiguous sequence of zero or more non-separator (see below) characters.

• Symbolic tokens are those that start with a character in one of the following classes: Sc, Sm, Sk, So, Pc, Pd, Po. This includes most symbolic and punctuation characters. This can be followed by any contiguous sequence of zero or more non-separator characters. (Grammatically, all symbolic tokens are assumed to be infix operators.)

• Separator tokens are the following: :- ( ) [ ] { } : , and . This list may be extended to include all bracketing (Ps, Pe) and paired quoting (Pi, Pf) characters.

A raw token is any other type of token enclosed in backquotes. A raw token is exactly equivalent to the unquoted token, except that for symbolic tokens it is not assumed to be infix. Thus, the following are equivalent (assuming the term-based parsing described below):

a + b
`+`(a,b)

#Grammatical syntax

Although Arend's specification language has only a handful of built-in operations, it's syntax includes support for a number of common extensions, under the assumption that specifications will want to use them in their natural forms. Thus, e.g., arithmetic operators are parsed according to the usual precedence, even though there are no built-in arithmetic operations.

The specification parser outputs a list of terms, from the terms module. Atomic and variable tokens are translated into Atoms and Variables, respectively. Compound terms of the form head(args...) or the infix form lhs OP rhs are translated into Compounds; for infix operators, the OP becomes the head.

Bracket-enclosed lists are parsed specially. The internal syntax for lists is a:b:c:[], being equivalent to [a,b,c]. The elements of the list can be any term.

Curly-braces are currently reserved for future extension, as are single- and double-quoted strings.

The grammatical syntax of Arend's specification language is roughly

specification = definition* 

definition = head ":-" body "."
           / head "."

head = term

body = term

term = atomicTerm
     / infixTerm
     / prefixTerm
     / listTerm
     / "(" term ")"

atomicTerm = atom

infixTerm = term OP term   // oversimplification

termList = (term ("," term)*)?

prefixTerm = atom "(" termList ")"

listTerm = "[" termList "]"

Note that, due to the ambiguity with ,, infix terms with , as their head inside lists must either be enclosed in parentheses or use the raw form of ,.

Operator precedence

Infix operators are parsed according to the following precedence table, from lowest to highest. The second column lists associativity.

Operator          Assoc.  Description
================= ======= ==============================
h(...)   (t)              Compounds, parenthesized terms

- !                       Prefix minus, not
^                 right   Exponentiation
* / %             left    Multiplication, division, mod
+ -               left    Addition, subtraction
< <= > >= == !=   non     Comparison
:                 right   Cons

<user-defined infix operators>

=                 other* Unification
, &               r,l    Conjunction
| ;               left   Disjunction
:-                left   Predicate definition

Note that in the first group of operators, the descriptions are just the "standard" interpretations. These operators have no predefined meaning in Arend. The second group of operators includes those which have some semantic meaning in Arend.

Associativity of unification: A = B = C is parsed as A = B, B = C, except that the entire unification is setup all at once, so it's slightly more efficient.

Also note that while , is right associative, & is left associative.

Note that, in its current state, Arend's grammar requires memoization to be enabled in order to avoid exponential parsing time in some cases. Hopefully this will be remedied in the future.