BNF, aka Backus–Naur form.
- Syntax
- Semantics 语义
Meaning: this rule means that the left-hand-side lhs
(a non-terminal symbol) can expand to ANY of the forms rhs1 to rhsn
on the right-hand-side. "$::=$" means "equal by definition"/"定义相等". Can simply write "=" instead.
Name | Meaning |
---|---|
Arity (元数、数量) | Number of arguments |
Fixity (固定性) | Where is the operator prefix, infix & postfix |
Example:
- / 1 2
- Arity: 2 (1, 2)
- Fixity: Prefix
- 1 + 2
- Arity: 2 (1, 2)
- Fixity: Infix
- 1 2 *
- Arity: 2 (1, 2)
- Fixity: Postfix
if then else
/ | \
boolean exp exp
AST, aka Abstract Syntax Trees.
Example:
+
/ \
+ 2
/ \
0 1
Chinese: 结合
To be simple, it is the basic rule of direction of process: from left to right or right to left.
Chinese: 歧义
Example:
It is
We should define its associativity:
- left associativity:
$(0 + 1) + 2$ - right associativity:
$0 + (1 + 2)$
Chinese: 优先级
Example:
It is
We should define symbols' precedence:
-
$+$ has higher precedence:$(0 + 1) + 2$ -
$\times$ has higher precedence:$0 + (1 \times 2)$
To avoid ambiguities:
- define the associativity of symbols
- define the precedence between symbols
- use parentheses to avoid ambiguities or for clarity
Parentheses are sometimes necessary:
- using left associativity
$0 + 1 + 2$ stands for$0 + (1 + 2)$ - we need parentheses to express
$0 + (1 + 2)$
Aka schematic variables.
$$
P \to P
$$
Why is it called a “metavariable”?
A metavariable is a variable within the language, called the metatheory, used to describe and study a theory at hand.
Explanation: An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables appear.
Chinese: 公理模式:公理模式是个在公理系统的语言中的一个合式公式,其中有一个以上的模式变数出现。
Chinese: 代换
for the substitution that maps
Operation: [val]
.
Example: eq[s]
takes an equality eq
and a substitutions, and replaces all occurrences of the keys of s
by the corresponding values in eq
.
Example: