Animats comments on "Object Oriented Mathematics (1995) [pdf]"

By Animats

Way too many years ago, I was trying to invent what should have been “object oriented constructive mathematics”, but we didn’t have object oriented programming yet.

There was an actual reason for this. I was working on program verification [1], and we’d put together a system which used the Oppen-Nelson prover in combination with the Boyer-Moore prover. We needed to prove that their theories were consistent.

The Oppen-Nelson prover is a complete, fast, automatic, decision procedure for expressions composed of addition, subtraction, multiplication by constants, conditionals, logical operators, and structure and array access. This subset of mathematics is completely decidable. (If you add multiplication of two variables, it becomes undecidable.) It can also accept “rules”, which are identities that it accepts as true. In our system, the Boyer-Moore prover was used to prove any new rules needed, which could then be imported into the Oppen-Nelson prover. Anything complicated involving loops usually required a new rule.

The Boyer-Moore system is completely constructive, and is based on recursive functions. Numbers are defined as (add1 (add1 (add1 (zero))), for example. One can then write recursive functions for addition and subtraction, and work up to multiplication and division. A few hundred theorems cover basic number theory.

Arrays, though, were a problem. There are four classic axioms, from McCarthy, which define basic array semantics. The Oppen-Nelson prover has those built in, but the Boyer-Moore system does not. We thus wanted to prove them in the Boyer-Moore system. If we could do that, it became safe to prove new things about arrays and import those rules into the Oppen-Nelson prover.

The axioms: arrays have two operations, SELECT and STORE. SELECT(array, index) returns the appropriate element from an array. STORE(array, index, newvalue) returns a new array where newvalue has replaced the element previously at index. We then have rules such as

 SELECT(STORE(A, I, V), I) = V // what you store, you get back

or, in Boyer-Moore notation:

 (implies (and (arrayp! A) (numberp I))
 (equal (selecta! (storea! A I V) I)
 V))

The rest can be seen at p. 129 of the manual[1] if you care.

Arrays had to be defined in the Boyer-Moore system as a list of (subscript, value) tuples. Not a set, a list. A set isn’t a constructive construct, because, informally, a set is a collection of unique values, the order of which is not significant. In the Boyer-Moore world, two values are equal iff they are identical. Two sets of tuples with a different order would not be equal.

So we had to define an array in the Boyer-Moore world as a list of (subscript, value) tuples ordered by increasing subscript. This is a clunky notation, because then we have to prove that the STORE operation preserved the correctness of the ordered list. Then we had to prove that all the rules for arrays were always true for that clunky representation. This required about 50 pages of machine proofs.

Back then (this was around 1981-1982), long machine proofs were not acceptable in mathematics. I had a JACM paper rejected for that reason. The approach was just too ugly.

Years later, I realized that what was needed was a kind of object oriented version of constructive mathematics. The key concept is that two things are equal if there is no way they can be distinguished. This comes from the theory of uninterpreted functions:

 forall f, x: f(x) = f(y) implies x = y

So we would like to be able to define an type with public and private functions, one which exposes a new “equal” operation for the type. Then, if we can prove that the new “equal” function obeys the rule above for all public functions, and we disallow all further access to the private functions, we can construct a consistent theory with a new, more abstract notion of “equal”. Now we can write set theory in Boyer-Moore theory without adding new axioms.

Unfortunately, I figured this out about a decade too late. We didn’t really need that result to get a valid verification system, but it would have cleaned up the theory and made it publishable. But anyway, there’s a form of object oriented mathematics which could be potentially useful.

The verification system was never used much; it was for a dialect of Pascal for Ford engine control programs that was never used in production. We looked at extending it to Ada (too hard) and C (too ill-defined). DEC SRL did a similar system for Modula III, but that died with DEC SRL, DEC, and Modula III. Some of the ideas were reused, decades later, in Microsoft’s Spec#.

[1] http://www.animats.com/papers/verifier/verifiermanual.pdf

---

link

Read more here: https://news.ycombinator.com/item?id=10729510

Animats comments on "Object Oriented Mathematics (1995) [pdf]"