FO[Sugar]

Goal

The goal of FO[Sugar] is to add convenient notations: binary and direct quantifications, variable declaration, and the “in” operator.

It also supports reasoning with partial interpretation of symbols.

Binary Quantification and Variable Declaration

Syntax

FO[Sugar] adds these production rules:

    Declaration ← VARIABLE IN ( Type | Symbol );
    Quantee ← VARIABLE {',' VARIABLE} [ IN Symbol ];
    Quantee ← VarTuple {',' VarTuple} IN Symbol;
        VarTuple ← '(' VARIABLE { ',' VARIABLE } ')';
flowchart LR subgraph Quantee direction LR start{ } --> VARIABLE([VARIABLE]); VARIABLE --> comma["','"]; comma --> VARIABLE2([VARIABLE]); VARIABLE2 --> comma; VARIABLE --> IN[ ] --> endQ; VARIABLE2 --> IN --> in[IN]--> Symbol([Symbol]) --> endQ[ ]; start{ } --> VarTuple([VarTuple]); VarTuple --> comma2["','"]; comma2 --> VAR_TUPLE2([VarTuple]); VAR_TUPLE2 --> comma2; VarTuple --> in; VAR_TUPLE2 --> in; end;
flowchart LR subgraph VarTuple direction LR lp["'('"] --> VARIABLE([VARIABLE]); VARIABLE --> comma["','"]; comma --> VARIABLE2([VARIABLE]); VARIABLE2 --> comma; VARIABLE --> rp["')'"]; VARIABLE2 --> rp; end;

Well-formedness

  1. Type must be a declared type.

  2. Symbol must be a declared predicate.

  3. Symbol must be a unary predicate when quantifying a VARIABLE, and an n-ary predicate when quantifying a VarTuple.

  4. When the variable has been declared in the vocabulary, the IN Symbol can be omitted.

  5. When quantifying a VarTuple, the number of VARIABLE in VarTuple must match the arity of Symbol.

Semantics

Let’s assume that the type signature of P is T1 ⨯ ... ⨯ Tn → 𝔹.

∃ x1 ∈ P: φ reduces to ∃ x1 ∈ T1: P(x1) ∧ φ (where P is unary). When the vocabulary has the declaration var x in T1, the formula can also be written ∃ x1: φ.
∃ (x1, ..., xn) ∈ P: φ reduces to ∃ x1 ∈ T1, .., xn ∈ Tn: P(x1, .., xn) ∧ φ.

Similarly,∀ x1 ∈ P: φ reduces to ∀ x1 ∈ T1: P(x1) ⇒ φ (where P is unary). When the vocabulary has the declaration var x in T1, the formula can also be written ∀ x1: φ.
∀ (x1, ..., xn) ∈ P: φ reduces to ∀ x1 ∈ T1, .., xn ∈ Tn: P(x1, .., xn) ⇒ φ.

Example

Assuming that the type signature of man is Person → 𝔹, ∀ x in man: mortal(x). is equivalent to ∀ x in Person: man(x) ⇒ mortal(x).

Direct quantification

Syntax

FO[Sugar] adds these production rules:

    Quantee ← VARIABLE {',' VARIABLE} IN '{' Value { ',' Value } '}';
    Quantee ← VarTuple {',' VarTuple} IN '{' TupleValue { ',' TupleValue } '}';

Well-formedness

  1. The Values must have the same type; this type is the type of the VARIABLEs.

  2. The TupleValue must be of the same type; they must not have a TO Value. The VarTuple type is the type of the TupleValues.

Semantics

∃ x ∈ {1,2,3}: φ(x) reduces to φ(1) ∨ φ(2) ∨ φ(3).
∃ (x,y) ∈ {(a,1),(b,2)}: φ(x,y) reduces to φ(a,1) ∨ φ(b,2).

∀ x ∈ {1,2,3}: φ(x) reduces to φ(1) ∨ φ(2) ∨ φ(3).
∀ (x,y) ∈ {(a,1),(b,2)}: φ(x,y) reduces to φ(a,1) ∧ φ(b,2).

“in” operator

Syntax

FO[Sugar] adds these production rules:

      Unary        ← { UNARY }  Enum;
      Enum         ← Base IN '{' Value { ',' Value } '}';

Notice that this extension redefines the syntax of Unary in FO[Core].

Well-formedness

The type of Base must be the same as the type of Value.

Semantics

Base IN { Value1, ..., Valuen } is the same as Base=Value1 ∨ .. ∨ Base=Valuen.

Partial interpretation of symbols

The goal is to support reasoning with partial interpretations of functions and predicates.

Lexicon

Token

Pattern

Example

INCLUDE

:⊇|:>=

Syntax

FO[Sugar] adds these production rules:

    Enum ← NAME_S '(' Expression {',' Expression } ')' 'is' 'enumerated' ;
  Interpretation ← NAME_S INCLUDE SymbolInterpretation '.';

Well-formedness

  1. NAME_S must be declared in the vocabulary and must be given an Interpretation.

  2. The number and types of arguments of NAME_S in Enum must match its type signature.

  3. The number and type of values Interpretation must match the type signature of the NAME_S being interpreted.

  4. An Interpretation using INCLUDE must use a TO element after every tuple of values in its SymbolInterpretation. The SymbolInterpretation does not have to be total over its domain.

Semantics

  1. A symbol interpretation given using INCLUDE is a partial interpretation of the symbol: the interpretation of the symbol is left unspecified for the tuples that are not interpreted.

  2. NAME_S(e1, .. , en) is enumerated is true when the Interpretation of NAME_S is total or when the interpretation of the tuple (e1, .. , en) is specified in the Interpretation of NAME_S. It is falseotherwise.

Example

The following theory requires that material() has a known maximum temperature.

    Material := {A, B, C}.
    maxTemp :⊇ {A→100}.  // maxTemp: Material -> Int
    maxTemp(material()) is enumerated.  // material: () -> Material

material() is thus A in every model.