The specification makes reference to the
Unicode
character set which, at the time of writing, is at version 13.0.0. The specification often references specific
Unicode characters, and does so using the standard notation
U+NNNN, where
N
represents a hexadecimal digit. For example,
U+03BB
corresponds to the lowercase lambda symbol
λ.
The specification gives grammar definitions in
ISO/IEC 14977:1996
Extended Backus-Naur form.
Because EBNF was designed prior to the existence of Unicode, it is necessary to extend the syntax to be able to
refer to Unicode characters in grammar definitions. This specification makes use of the standard unicode
U+NNNN
syntax in grammar definitions, to refer to specific Unicode characters. It also makes use of the syntax
\p{t}
which should be understood to represent any Unicode character with the property
t. For example,
\p{Lowercase_Letter}
describes the set of characters that are both letters and are lowercase. The syntax
\P{t}
should be understood as the negation of \p{t}; it describes the set of characters
without the property t.
The Cedarbridge language uses s-expressions as the base for
all syntax. An s-expression is described by the following EBNF grammar:
As shown, the Cedarbridge language uses an extension of basic s-expressions that allow
for the optional use of either square brackets or parentheses to increase the readability of large nested
expressions. These should be treated as interchangeable, but must be correctly balanced as shown by the grammar.
For example, the expression [] is semantically equivalent to
(), but the expression [) is invalid.
Declarative type rules describe the precise rules for assigning types to terms. If no type rule matches a term,
then that term is considered ill-typed.
Type rules are given as zero or more premises, and a single
conclusion, separated by a horizontal line. For a given rule, when all of the premises
are true, then the conclusion is true. If a rule has no premises then the rule is taken as an
axiom.
The gamma symbol Γ (U+0393) represents the current typing environment and can be
thought of as a mapping from distinct variables to their types, with the set of variables in environment denoted
by dom(Γ) (the domain of Γ). The notation Γ ⊢ P reads
"Γ implies P" and is used in type rules to assign types to terms. The empty typing environment is represented by ∅
(U+2205). The diamond symbol ◇ (U+25C7) should be read as "is well-formed", so
Γ ⊢ ◇
should be read as "the current typing environment is well-formed". The concept of well-formedness is often
type-system-specific and is usually described when the rules are given.