FO[Int]

The goal of FO[Int] is to allow expressing knowledge about integer quantities using the 4 arithmetic operators and comparisons. It extends FO[PF].

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	Int|ℤ
INTEGER	[+-]?\d+	-123
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].

flowchart LR subgraph Conjunction direction LR start{ } --> Comparison([Comparison]); Comparison --> END{ }; Comparison --> AND; AND --> Comparison2([Comparison]); Comparison2 --> AND; Comparison2 --> END; end;

flowchart LR subgraph Comparison direction LR start{ } --> SumMinus([SumMinus]); SumMinus --> END{ }; SumMinus --> COMPARISON; COMPARISON --> SumMinus2([SumMinus]); SumMinus2 --> COMPARISON; SumMinus2 --> END; end;

flowchart LR subgraph SumMinus direction LR start{ } --> MultDiv([MultDiv]); MultDiv --> END{ }; MultDiv --> SUM_MINUS; SUM_MINUS --> MultDiv2([MultDiv]); MultDiv2 --> SUM_MINUS; MultDiv2 --> END; end;

flowchart LR subgraph MultDiv direction LR start{ } --> Power([Power]); Power --> END{ }; Power --> MULT_DIV; MULT_DIV --> Power2([Power]); Power2 --> MULT_DIV; Power2 --> END; end;

flowchart LR subgraph Power direction LR start{ } --> Unary([Unary]); Unary --> END{ }; Unary --> POWER; POWER --> Unary2([Unary]); Unary2 --> POWER; Unary2 --> END; end;

Well-formedness

1. Division must be well-guarded to prevent division by 0 (e.g., if y ≠ 0 then x/y else 1).

2. Quantification over ℤ is not allowed (relaxed in FO[Infinite]).

Semantics

The arithmetic and comparison operators have their usual meaning.

Range

Syntax

FO[Int] adds these production rules:

    TypeInterpretation ← '{' INTEGER '..' INTEGER '}';
    Quantee ← VARIABLE {',' VARIABLE} IN '{' INTEGER '..' INTEGER '}';
    Enum    ← Base IN '{' INTEGER '..' INTEGER '}';
    Identifier ← INTEGER;

Well-formedness

The first INTEGER must be below the second INTEGER.

If the interpretation of a range is not given in the vocabulary block (but in the theory or structure block), it is required to state that the declared type is a subtype of Int.

Semantics

{1..8} represents the set {1, 2, 3, 4, 5, 6, 7, 8}. The type that it interprets is automatically inferred to be a subtype of Int.

Date

Lexicon

Token	Pattern	Example
DATE	#\d{4}-\d{2}-\d{2}	#2022-01-01

Syntax

FO[Int] adds these production rules:

    Type ← 'Date';
    Identifier ← DATE | '#TODAY' ['(' INTEGER, INTEGER, INTEGER ')'];

Well-formedness

1. Dates can occur wherever integers can occur.

2. DATE must be a valid date.

3. 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.