Consider parsing and modeling facts as integer-linear inequalities

[reinerp]

I think the problem statement and applications of Wuffs are great, thanks for developing it!

---

I observe that:

1. Proving facts using the axioms in axioms.md is somewhat brittle, or something of a hassle. The logic checking system doesn't natively know many theorems that humans consider obvious, e.g. commutativity of addition, grouping of terms, etc. At least in my preliminary experience playing with Wuffs-the-language, I found this to be a sufficiently frustrating experience that it turned me away.

2. All of the axioms in axioms.md are theorems of linear programming, i.e. linear algebra plus inequalities. There are no axioms from more advanced theories, e.g. axioms from e.g. polynomial arithmetic.

3. The theory of linear programming is especially simple, in two key ways:
   a) Any facts (inequalities) that can be proved under this theory can be proved by just one derivation rule: the new fact (inequality) is a linear combination of existing facts (inequalities). See https://en.wikipedia.org/wiki/Farkas%27_lemma#Logic_interpretation.
   b) Efficient decision procedures exist for this theory: they are guaranteed to terminate (prove or disprove the theorem) in polynomial time, and they are fast in practice too. They are far more reliable in practice than the solvers on nonlinear arithmetic that you reference elsewhere as being problematic with e.g. SMT solvers like Z3.

Based on these I suggest that:

(i) Wuffs could parse facts into integer-linear form: normalize them into boolean ANDs of expressions equivalent to sum_i lhs_integer_literal[i] * expression[i] <= rhs_integer_literal.

(ii) Give users a syntax to prove assertions by the "this assertion is a linear combination of existing assertions" derivation rule. This single derivation rule is sufficient to subsume all axioms currently in axioms.md as well as the simplify function in assert.go.

(iii) [Much more weakly held position given the complexity and compile-time tradeoffs.] Consider automatically proving assertions using an LP solver.

---

Some further commentary:

• wrt (i), the normal form would be something like: struct { LHS map[Expr]int; RHS int }. The mere act of parsing into this normal form produces a stronger set of simplifications than assert.go's simplify function can perform: for example, it can simplify terms like (x + y) - x down to y.

• wrt (ii), note that most LP solvers can produce an "infeasibility certificate", i.e. exactly the linear inequality needed to prove a theorem as a linear combination of the hypotheses as described in (ii). The existence of a certificate, allows separating into two Wuffs compilation modes: a "checker" mode which requires that all assertions have certificates present, i.e. specify the linear combinations of other assertions that prove this assertion; and a separate "LP-solver" mode which produces such certificates for the assertions in the code which don't have them already. This split into modes allows the "checker" to be very fast and simple. Happily, the LP solver does not need to be part of the trusted computing base.

• Wrt (iii), even though the theorems we're talking about are integer-linear inequalities, I'm suggesting here to use the real relaxation (LP) rather than modeling it as an integer linear programming (ILP) problem. The latter is NP-hard to decide; the former is polynomial-time to decide.

• Wrt (iii): I would guess that on small problems like the theorems in Wuffs programs, the LP solvers are extremely fast -- likely meeting your compile time goal of "subsecond" by far. That said, I haven't done the exercise of writing out the theorem statements from an actual Wuffs program and timing the solver on them.

[nigeltao]

That's a very interesting comment. I hadn't thought of canonicalizing to integer-linear form but it makes sense.

Re-doing the axioms system isn't a short-term priority, but I'll keep thinking about it. Thanks!