FO[Int]¶
The goal of FO[Int] is to allow expressing knowledge about integer quantities using the 4 arithmetic operators and comparisons.
It also allows creating and using types containing a range of elements, and the comparison of dates, e.g., to determine the applicability of a law..
Integer arithmetic¶
Lexicon
Token |
Pattern |
Example |
---|---|---|
COMPARISON |
|
|
INT |
|
|
INTEGER |
|
|
MULT_DIV |
|
|
POWER |
|
|
SUM_MINUS |
|
|
UNARY |
|
Note that this extension extends the pattern of UNARY in FO[Core].
Syntax
FO[Int] adds these production rules:
Type ← INT;
Conjunction ← Comparison {AND Comparison};
Comparison ← { ANNOT }
SumMinus {COMPARISON SumMinus};
SumMinus ← MultDiv {SUM_MINUS MultDiv};
MultDiv ← Power {MULT_DIV Power};
Power ← Unary {POWER Unary};
Identifier ← INTEGER;
Symbol ← 'abs';
Note that this extension replaces the syntax of a Conjunction in FO[Core].
Well-formedness
Division must be well-guarded to prevent division by 0 (e.g.,
if y ≠ 0 then x/y else 1
).Quantification over ℤ is not allowed (relaxed in FO[Infinite]).
Semantics
The arithmetic and comparison operators have their usual meaning.
Range¶
Lexicon
Token |
Pattern |
Example |
---|---|---|
POINT |
|
|
Syntax
FO[Int] adds these production rules:
TypeInterpretation ← '{' POINT '..' POINT '}';
Quantee ← VARIABLE {',' VARIABLE} IN '{' POINT '..' POINT '}';
Enum ← Base IN '{' POINT '..' POINT '}';
Identifier ← POINT;
Well-formedness
For TypeInterpretation
The alphabetic prefix in the first
POINT
must be the same as the one in the secondPOINT
. It must be declared only once in aTypeInterpretation
.The natural number in the first
POINT
must be below the natural number in the secondPOINT
.
For Quantee
and Enum
:
The alphabetic prefix in the first
POINT
must be the same as the one in the secondPOINT
. It must have been declared in aTypeInterpretation
.The natural number in the first
POINT
must be below the natural number in the secondPOINT
. They must be within the range declared by theTypeInterpretation
.
For Identifier
:
The alphabetic prefix in the
POINT
must have been declared in aTypeInterpretation
.The natural number in the
POINT
must be within the range declared by theTypeInterpretation
.
A POINT
may participate in integer arithmetic operations and comparisons as an integer (ignoring the alphabetic prefix).
Semantics
{R1..R8}
represents the set {R1, R2, R3? R4, R5, R6, R7, R8}
.
Date¶
Lexicon
Token |
Pattern |
Example |
---|---|---|
DATE |
|
|
Syntax
FO[Int] adds these production rules:
Type ← 'Date';
Identifier ← DATE | '#TODAY' ['(' INTEGER, INTEGER, INTEGER ')'];
Well-formedness
Dates can occur wherever integers can occur.
DATE
must be a valid date.Quantification over
Date
is not allowed (except with the FO[Infinite] extension).
Semantics
Dates are converted to proleptic Gregorian ordinals, where January 1 of year 1 has ordinal 1.
#TODAY(y,m,d)
is today’s date shifted by y
years, m
month and d
days. #TODAY(-1, 0, 0)
is today last year.