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

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

Lexicon

Token

Pattern

Example

POINT

[a-zA-Z]*\d+

R1

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

  1. The alphabetic prefix in the first POINT must be the same as the one in the second POINT. It must be declared only once in a TypeInterpretation.

  2. The natural number in the first POINT must be below the natural number in the second POINT.

For Quantee and Enum:

  1. The alphabetic prefix in the first POINT must be the same as the one in the second POINT. It must have been declared in a TypeInterpretation.

  2. The natural number in the first POINT must be below the natural number in the second POINT. They must be within the range declared by the TypeInterpretation.

For Identifier:

  1. The alphabetic prefix in the POINT must have been declared in a TypeInterpretation.

  2. The natural number in the POINT must be within the range declared by the TypeInterpretation.

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

#\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.