untype the variables

[johnyf]

Quantifier bounds and dynamic type hints in omega

As of f4aa8f8459c65d5491aadef1fef80db23944a792, the formula \A x: P(x) means different things, depending on whether it is given to omega.symbolic.fol.Context.add_expr with x declared as an "integer" with "domain" 2..7 in Automaton.vars, "domain" -15..100, or x declared as a "Boolean". In transition to mathematics (following [1]), bounds will be introduced (as anticipated by this note in the module fol.py). All sentences will then have the same meaning in any Context.

In principle, this should allow automatically inferring what refinement to use (for satisfiability and construction of witnesses for a variable quantified over a known finite set 0..N, using variables that are restricted to take only Boolean values--also known as "bits"). In other words, utilizing the quantifier bounds as type hints [1]. This kind of refinement process is colloquially known as "bitblasting".

Thus, we could imagine "dynamically" extending the domain of variables (in terms of the current implementation, this means dynamically changing the "domain" of an integer stored in Context.vars), depending on what bounds are used in a sentence that contains quantifiers.

Quantifier bounds aren't obligatory. If P(x) is of the form (x \in Foo) => Q(x), then the formula \A x: P(x) is equivalent to \A x \in Foo: Q(x), where the quantifier is bounded. The antecedent form is more difficult to handle, because the bound has to be (syntactically) detected in the formula P(x), and there are infinitely many formulae equivalent to P(x). For this reason, bounded quantification will be syntactically required in omega.

Formulae with free variables (i.e., not sentences) will still remain differently encoded between Contexts. That shouldn't be a problem, because whenever one wants to quantify the variables in a formula, they should bound the quantifiers. In the presence of static Boolean refinements (type hint declarations), if too large a bound is used, then an error will be raised.

The methods Context.pick, pick_iter, count, forall, exist should be understood as (implicitly) bounded using the type hint declarations. From a programming perspective, it is cumbersome to pass a bound every time these methods are called within a solver. So, the explicit bounds will be required in syntax, but not in each method's signature, because the method is attached to a Context instance, unlike a formula as string.

The above will introduce a limited amount of set theory (0..N and {0, 1, 3}) and syntactic definitions (Foo == 0..N or Foo == P(x)), so a small amount of TLA+. This additional expressive power should be regarded as a paradigm change, rather than full-fledged support for set theory.

I'm not sure whether it even makes sense to think of recognizing bounds within P(x) semantically (via BDDs or other model-theoretic means), because by the time one has converted the proof-theoretic object (the formula) to a BDD, they have already made assumptions about the domain of interpretation (i.e., they have bounded the values that the variables can take, in order to represent them. This isn't an artifact of infinite sets--different finite ranges suffice to cause problems).

TLC supports only quantifiers that are explicitly bounded, likely because the bound is then readily available, and because any specification that we want to write in practice will contain bounds, either as antecedents, or on the quantifiers, so better to place them directly on the quantifiers. A formula that contains "genuinely unbounded" quantifiers probably doesn't mean what the specifier intended.

Quantifier bounds in dd?

dd is limited to propositional reasoning (single type for all variables), and its parsing capabilities are intended more for convenience, rather than specification. Also, its computation involves primarily BDDs, which belong to the semantic level. Requiring from users to keep writing \A x \in BOOLEAN: ... for all variables is unnecessarily cumbersome, given that the bound BOOLEAN is the same for all BDD variables.

Explicit is better than implicit, but simple is better than complex. Special cases aren't special enough to break the rules, although practicality beats purity [PEP 20]. So, I will let quantifier syntax omit bounds in dd, and antecedents of the form x \in BOOLEAN aren't supported either, making dd syntax typed (all BDD variables typed as BOOLEAN).

References

[1] Leslie Lamport, Lawrence C. Paulson "Should your specification language be typed?" ACM Transactions on Programming Languages and Systems Vol.21, No.3, pp.502--526, 1999

[2] Hernán Vanzetto "Proof automation and type synthesis for set theory in the context of TLA+", PhD Thesis, Computer Science. Université de Lorraine, 2014