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 IN Symbol is omitted, the type of the variable(s) is inferred from the variable’s declaration (if given), or from the quantified formula (to make it well-formed; an error is raised otherwise).

  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). It 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). It can also be written ∀ x1: φ.
∀ (x1, ..., xn) ∈ P: φ reduces to ∀ x1 ∈ T1, .., xn ∈ Tn: P(x1, .., xn) ⇒ φ.

Note

When inferring Symbol is difficult for a human because of the complexity of the quantified formula, it is recommended to declare the variable, or explicitly state the Symbol in Quantee.

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.