FO[Real]¶
Goal
The goal of FO[Real] is to allow expressing knowledge about real quantities using the 4 arithmetic operators and comparisons.
Lexicon
Token |
Pattern |
Example |
|---|---|---|
DIGIT |
|
|
REAL |
|
|
REALVAL |
|
|
Syntax
FO[Real] adds these production rules:
Type ← REAL;
Identifier ← REALVAL;
flowchart LR
subgraph Identifier
direction LR
start{ } --> SUM_MINUS;
start --> DIGIT;
SUM_MINUS --> DIGIT;
DIGIT --> DIGIT;
DIGIT --> END{ };
DIGIT --> dot["'.'"];
dot --> END;
dot --> DIGIT2[DIGIT];
DIGIT2 --> DIGIT2;
DIGIT2 --> END;
DIGIT2 -->e["'e'"];
e --> sum2[SUM_MINUS];
e --> DIGIT3[DIGIT];
sum2 --> DIGIT3;
DIGIT3 --> DIGIT3;
DIGIT3 --> END;
end;
Well-formedness
Division must be well-guarded to prevent division by 0 (e.g.,
if y ≠ 0 then x/y else 1.0).An arithmetic expression cannot mix integer and real numbers.
Quantification over ℝ is not allowed (relaxed in FO[Infinite]).
Semantics
The arithmetic and comparison operators have their usual meaning.
TODO: discuss approximations