FO[Infinite]

Goal The goal of FO[Infinite] is to allow quantification over infinite domains. This extension extends FO[Int] and/or FO[Real].

Syntax

FO[Infinite] does not introduce new syntactic rules.

Well-formedness

  1. Contrary to FO[Core], constructors can be recursive in FO[Infinite]: a NAME_T occurring as argument of a CONSTRUCTOR does not have to be previously declared (but it has to be declared). As a result, a constructed type may have an infinite domain.

  2. Contrary to FO[Int], quantification over infinite types (ℤ, ℝ, Date) are allowed in FO[Infinite]. This also applies to binary quantifications using predicates over infinite domains (FO[Sugar].

Semantics

The formal semantics of a formula quantified over an infinite domain is a conjunction (or disjunction) of infinite length.

Example

The type for “lists of integers” can be declared as follows:

type List := constructed from { nil, cons(ℤ, List)}

cons(1, cons(2, nil)) represents the list [1,2].

Here is a quantification over integers:

∀ x ∈ ℤ: 0 ≤ x^2.