Binding-Oriented Design (BOD)

[DavePearce]

The purpose of this discussion is to begin the process of redesigning WyTP. Specifically, to address all of the issues around quantifiers which, today, remain the biggest source of problems.

The rough outline is:

• Instantiation Engine. This instantiates quantifiers in a given state.

• Contradiction Engine. For a given state, this searches for a contraction by through congruence, inequalities, and other rules.

• State. The state consists of a a bunch of variable declarations (inc. quantified variables) and terms. There are no longer any specific quantifiers as before, leaving a flat hierarchy.

The instantiation engine drives this by instantiating quantifiers and then using the contradiction engine to search for a problem. There are a bunch of different heuristics it can use here (e.g. instantiate individual or in batches; depth-first on a single quantified variable or breadth-first across all variables).

This mostly seems like it will work, though it raises a bunch of questions:

• Efficiency. Can we incrementally update a State after more things are instantiated? For example, if a given State is expanded into a tree then we only need to propagate instantiated terms through to unresolved leaves.

• Axioms. Are these expanded in the contradiction engine, or can we do something else? Perhaps we can fit this together somehow with the interpreter.

[DavePearce]

An interesting question is what the complete list of transformation rules currently employed is:

1. Inequality Introduction. Apply transitive closure.

2. Array Equality Case Analysis. Break down array equality expressions.

3. Array Index Axiom. Infer requirements that index be within bounds.

4. Array Index Case Analysis. Break down accesses on array constants.

5. Function Call Axiom. Infer requirements that precondition be met.

6. Macro Expansion. Expand property macros and similar (non-recursively).

7. And and Or Elimination. Simple logical simplifications.

8. Exists Elimination. Skolemisation.

There must also be axioms for divide by zero and array (generator) length, etc.