Automated Equational Reasoning with Twee Pt 1.
Manipulating equations on a computer is very tantalizing.
Twee is a very nice off the shelf equational prover. You can install it, get human readable equational proofs out, have it find interesting terms, and dump out a rewrite system that may have very useful properties.
Here is an example from the Twee tests of it using an equational specification of differentiation to derive an antiderivative. It’s very impressive in my opinion. The proof output is quite clean and it also returns the instantiation of the existential. Used in this manner, twee is an antidifferentiation engine, which is pretty cool.
%%bash
curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | BOOTSTRAP_HASKELL_NONINTERACTIVE=1 sh
apt install libgmp-dev
!PATH=~/.ghcup/bin:$PATH cabal install twee
%%file /tmp/deriv.p
% Axioms about arithmetic.
cnf('commutativity of +', axiom,
X + Y = Y + X).
cnf('associativity of +', axiom,
X + (Y + Z) = (X + Y) + Z).
cnf('commutativity of *', axiom,
X * Y = Y * X).
cnf('associativity of *', axiom,
X * (Y * Z) = (X * Y) * Z).
cnf('plus 0', axiom,
'0' + X = X).
cnf('times 0', axiom,
'0' * X = '0').
cnf('times 1', axiom,
'1' * X = X).
cnf('distributivity', axiom,
X * (Y + Z) = (X * Y) + (X * Z)).
cnf('minus', axiom,
X + -X = '0').
cnf('derivative of 0', axiom,
d('0') = '0').
cnf('derivative of 1', axiom,
d('1') = '0').
% Actually, i would claim this axiom is a misstep
% exterior derivative methodology could be useful.
% maybe d(E1)*d(E2) = 0 is a better axiom.
cnf('derivative of x', axiom,
d(x) = '1').
cnf('derivative of +', axiom,
d(T+U) = d(T) + d(U)).
cnf('derivative of *', axiom,
d(T*U) = (T*d(U)) + (U*d(T))).
cnf('derivative of sin', axiom,
d(sin(T)) = cos(T) * d(T)).
cnf('derivative of cos', axiom,
d(cos(T)) = -(sin(T)*d(T))).
fof(goal, conjecture,
?[T]: d(T) = x*cos(x)).
Overwriting /tmp/deriv.p
!twee /tmp/deriv.p --quiet --no-color
The conjecture is true! Here is a proof.
Axiom 1 (derivative of x): d(x) = 1.
Axiom 2 (commutativity of +): X + Y = Y + X.
Axiom 3 (plus 0): 0 + X = X.
Axiom 4 (commutativity of *): X * Y = Y * X.
Axiom 5 (times 1): 1 * X = X.
Axiom 6 (minus): X + -X = 0.
Axiom 7 (derivative of +): d(X + Y) = d(X) + d(Y).
Axiom 8 (associativity of +): X + (Y + Z) = (X + Y) + Z.
Axiom 9 (derivative of sin): d(sin(X)) = cos(X) * d(X).
Axiom 10 (derivative of cos): d(cos(X)) = -(sin(X) * d(X)).
Axiom 11 (derivative of *): d(X * Y) = (X * d(Y)) + (Y * d(X)).
Lemma 12: X * 1 = X.
Proof:
X * 1
= { by axiom 4 (commutativity of *) R->L }
1 * X
= { by axiom 5 (times 1) }
X
Goal 1 (goal): d(X) = x * cos(x).
The goal is true when:
X = cos(x) + (x * sin(x))
Proof:
d(cos(x) + (x * sin(x)))
= { by axiom 4 (commutativity of *) R->L }
d(cos(x) + (sin(x) * x))
= { by axiom 7 (derivative of +) }
d(cos(x)) + d(sin(x) * x)
= { by axiom 10 (derivative of cos) }
-(sin(x) * d(x)) + d(sin(x) * x)
= { by axiom 1 (derivative of x) }
-(sin(x) * 1) + d(sin(x) * x)
= { by lemma 12 }
-sin(x) + d(sin(x) * x)
= { by axiom 2 (commutativity of +) R->L }
d(sin(x) * x) + -sin(x)
= { by axiom 11 (derivative of *) }
((sin(x) * d(x)) + (x * d(sin(x)))) + -sin(x)
= { by axiom 1 (derivative of x) }
((sin(x) * 1) + (x * d(sin(x)))) + -sin(x)
= { by lemma 12 }
(sin(x) + (x * d(sin(x)))) + -sin(x)
= { by axiom 8 (associativity of +) R->L }
sin(x) + ((x * d(sin(x))) + -sin(x))
= { by axiom 2 (commutativity of +) }
sin(x) + (-sin(x) + (x * d(sin(x))))
= { by axiom 8 (associativity of +) }
(sin(x) + -sin(x)) + (x * d(sin(x)))
= { by axiom 6 (minus) }
0 + (x * d(sin(x)))
= { by axiom 3 (plus 0) }
x * d(sin(x))
= { by axiom 9 (derivative of sin) }
x * (cos(x) * d(x))
= { by axiom 1 (derivative of x) }
x * (cos(x) * 1)
= { by lemma 12 }
x * cos(x)
RESULT: Theorem (the conjecture is true).
Group Theory
Group theory provides some nice simple examples of equational proofs. For example, it is not at all obvious that the left inverse must be the same as the right inverse, or that the left and right identities must be the same. Instead of groups, you could also use rings, fields, or any other algebraic structure (more exotic things like loops and robbins algebra have had success used tools from the ATP world).
%%file /tmp/group.p
cnf(right_identity, axiom, X * id = X).
cnf(right_inverse, axiom, X * inv(X) = id).
cnf(associativity, axiom, (X * (Y * Z)) = ((X * Y) * Z)).
cnf(left_inverse, conjecture, inv(X) * X = id).
%cnf(left_identity, conjecture, id * X = X).
Overwriting /tmp/group.p
!twee /tmp/group.p --no-color
Here is the input problem:
Axiom 1 (right_identity): X * id = X.
Axiom 2 (flattening): *2 = id * x.
Axiom 3 (right_inverse): X * inv(X) = id.
Axiom 4 (associativity): X * (Y * Z) = (X * Y) * Z.
Goal 1 (left_identity): id * x = x.
1. X * id -> X
2. id * x -> *2
3. X * inv(X) -> id
4. (X * Y) * Z -> X * (Y * Z)
5. X * (id * Y) -> X * Y
6. X * x -> X * *2
7. id * *2 -> *2
8. X * inv(id) -> X
9. id * (x * X) -> *2 * X
10. *2 * inv(x) -> id
11. X * (inv(X) * Y) -> id * Y
12. id * inv(inv(X)) -> X
13. X * (x * Y) -> X * (*2 * Y)
14. X * inv(inv(Y)) -> X * Y
15. id * X -> X
16. x -> *2
The conjecture is true! Here is a proof.
Axiom 1 (right_identity): X * id = X.
Axiom 2 (right_inverse): X * inv(X) = id.
Axiom 3 (associativity): X * (Y * Z) = (X * Y) * Z.
Lemma 4: X * (inv(X) * Y) = id * Y.
Proof:
X * (inv(X) * Y)
= { by axiom 3 (associativity) }
(X * inv(X)) * Y
= { by axiom 2 (right_inverse) }
id * Y
Lemma 5: id * inv(inv(X)) = X.
Proof:
id * inv(inv(X))
= { by lemma 4 R->L }
X * (inv(X) * inv(inv(X)))
= { by axiom 2 (right_inverse) }
X * id
= { by axiom 1 (right_identity) }
X
Goal 1 (left_identity): id * x = x.
Proof:
id * x
= { by lemma 4 R->L }
X * (inv(X) * x)
= { by lemma 5 R->L }
X * (inv(X) * (id * inv(inv(x))))
= { by axiom 3 (associativity) }
X * ((inv(X) * id) * inv(inv(x)))
= { by axiom 1 (right_identity) }
X * (inv(X) * inv(inv(x)))
= { by lemma 4 }
id * inv(inv(x))
= { by lemma 5 }
x
RESULT: Theorem (the conjecture is true).
Egraphs and Ground Rewriting
I think it’s very interesting that if you give twee a ground system of equalities, the resulting rewrite system can be interpreted as an egraph.
If you give Twee an impossible to prove goal condition like true = false, it will fail. It prints out the normalized rewrite system when it does this though. This rewrite system is an egraph. The right hand side is a canonical term for that equivalence class and left hand sides are possible other terms in that eclass. You could fill out the system with “skolem” symbols for each eclass and made these low in the term ordering, the right hand sides would be eclasses and the left hand side would be enodes.
I wrote more about this perspective here https://www.philipzucker.com/egraph-ground-rewrite/
%%file /tmp/egraph.p
% egraph will find the greatest common divisor of a loopy set of equations
cnf(eq1, axiom, foo(foo(a)) = a).
cnf(eq2, axiom, foo(foo(foo(a))) = a).
cnf(false, conjecture, true = false).
Writing /tmp/egraph.p
!twee /tmp/egraph.p --no-color
Here is the input problem:
Axiom 1 (eq1): foo(foo(a)) = a.
Axiom 2 (eq2): foo(foo(foo(a))) = a.
Goal 1 (false): true = false.
1. foo(foo(a)) -> a
2. foo(a) -> a
Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
foo(a) -> a
RESULT: CounterSatisfiable (the conjecture is false).
Perhaps more simple, the resulting ground rewrite system is a normalized / compressed union find. The right hand side is a canonical element, and the left hand side are all the things in the same union find set.
%%file /tmp/unionfind.p
cnf(ax1, axiom, a = b).
cnf(ax2, axiom, b = c).
cnf(ax3, axiom, c = d).
cnf(ax4, axiom, d = e).
cnf(ax5, axiom, f = g).
cnf(false, conjecture, true = false).
Writing /tmp/unionfind.p
!twee /tmp/unionfind.p --no-color
Here is the input problem:
Axiom 1 (ax5): f = g.
Axiom 2 (ax1): a = b.
Axiom 3 (ax2): b = c.
Axiom 4 (ax4): d = e.
Axiom 5 (ax3): c = d.
Goal 1 (false): true = false.
1. g -> f
2. b -> a
3. c -> a
4. d -> e
5. e -> a
Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
b -> a
c -> a
d -> a
e -> a
g -> f
RESULT: CounterSatisfiable (the conjecture is false).
You can also use twee to do something analogous to egraph saturation if you add in the actual rewrite rules. This is particularly interesting because term rewriting sytems are more clear cut on how you could add theories, lambdas, etc, because things are just terms.
If you give Twee an early stopping criterion, it dumps out the currently discovered rewriting system. You can see the available early stopping criteria in –expert-help
Resource limits:
--max-term-size <num>
Discard rewrite rules whose left-hand side is bigger than this limit (unlimited by default).
--max-cps <num>
Give up after considering this many critical pairs (unlimited by default).
--max-cp-depth <num>
Only consider critical pairs up to this depth (unlimited by default).
Bits and Bobbles
What is equational search
Equational proof search is not that complicated in principle. You are given an initial term to start out with and you are seeking some goal term. This can be thought of as a graph search with reachable terms as nodes and applying some equation as an edge. You could apply all the regular depth first, breadth first, A*, Beam etc search algorithms.
There is more structure here though and it is typically perceived that a graph search like this is too brute force. I actually don’t think people try it that much before going to fancier techniques.
An alternate starting point is the idea of simplification by term rewriting. Some of your equations are orientable into rewrite rules that are obviously simplifying your term in some sense. Many equational problems do feel to be of the form “give me a term equivalent to term foo(x) that is simpler”. Most automated equational manipulation in the world is greedy rewriting of this form.
Simplifying rewrite rules are not incompatible with throwing some search on top, but it now takes more thoughts and concepts. If you have two rewrite rules that could fire, you could do a search considering both choices. This work is redundant if your system of rewrite rules is sufficiently nice. If your system of rules is confluent and terminating, then you can apply the rules greedily willy nilly and always end up at the same “simplest” result regardless of rule application order. In this case, you can also determined inequality of terms.
I keep my eye on the various solver competitions. https://www.tptp.org/CASC/29/WWWFiles/DivisionSummary1.html In 2023, for “unit equality CNF” Twee did very well. Unit equality CNF is is an unfortunately confusing jargon for pure equational. Twee is a theorem prover for equational logic. It is implemented in Haskell, not that that matters much to a user.
Twee is also a relatively simple system compared to Vampire and E, it’s more general and close competitors. This is importance when you want to use the solver in more ways than the strictly allows “proved such and such conjecture” more. The remnant rewrite system is of great interest in and of itself as shown from egraph rewriting.
Links
https://smallbone.se/papers/twee.pdf Twee system description
https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/waldmeister/implementation Waldmiester https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/waldmeister/primer CITIUS, ALTIUS, FORTIUS: Lessons learned from the Theorem Prover Waldmeister”. https://www.mpi-inf.mpg.de/fileadmin/inf/rg1/Documents/Hil03.ps
theory exploration. ruler.
mccune eqp
https://www.jaist.ac.jp/~mizuhito/thesis/DominikKlein.pdf inductionless induction. circular proofs. well founded induction.
https://github.com/leanprover-community/duper
https://www.philipzucker.com/juliacon-talk/
Command line options
It is useful to always look at the options available in any command line tool.
--expert-help
--conjecture n although it didn’t seem to work?
Python Metaprogramming
I don’t love the TPTP format. It’s a bit clunky and repetitive. Twee supports infix operations as an extension, but I would like other niceties and abstractions.
There are advantages I believe to having a metaprogrammble metalanguage. Python is a reasonable one.
Parsing the output of the proofs and rewrite systems is also useful. The rewrite systems are analagous to a final datalog database, or an egraph. Not every thing I want to do takes the form of “prove this two sided equation”. Term extraction is also of paramount interest for less theorem provy applications.
The Knuckledragger approach is to chain together solves to automated provers with a light trust framework gluing in between.
def tptp(sexp):
return f"{sexp[0]}({','.join(map(tptp, sexp[1:]))})" if isinstance(sexp, list) else str(sexp)
class Const(str):
#def __init__(self, name):
# self.name = name
def __eq__(self, other):
return Expr(["=", self, other])
def __add__(self, other):
return Expr(["+", self, other])
def __mul__(self, other):
return Expr(["*", self, other])
def __rshift__(self, other):
return Expr(["comp", self, other])
def __matmul__(self, B):
return Expr(["@", self, B])
def __neg__(self):
return Expr(["-", self])
class Expr(list):
def __repr__(self):
return tptp(self)
def __eq__(self, other):
return Expr(["=", self, other])
def __add__(self, other):
return Expr(["+", self, other])
def __mul__(self, other):
return Expr(["*", self, other])
def __rshift__(self, other):
return Expr(["comp", self, other])
def __matmul__(self, B):
return Expr(["@", self, B])
def __neg__(self):
return Expr(["-", self])
def function(name):
def res(*args):
return Expr([name, *args])
return res
def functions(names):
names = names.split()
return map(function, names)
def consts(x):
return map(Const, x.split())
X,Y,x = consts("X Y x")
f,g = functions("f g")
tptp(f(X))
type(f(X))
X + Y
+(X,Y)
Knuckledragger Calc
We can chain together calls to Twee or other equational provers with a protected theorem datatype or via keeping a recording of the trace of calls (a proof object).
There are examples of calc tactics elsewhere in lean and dafny. Rather than using the raw inference rules, we can write down an equational proof
You can also calc chain equalities of boolean expressions that are the same. Calc also supports an inequality modes
Adding forall.
from knuckledragger.kernel import infer
class Calc():
def __init__(self, lhs, rhs, ctx = []):
self.terms = [lhs]
self.thm = infer(ctx, lhs == lhs)
self.thms = []
self.goal = rhs
self.ctx = ctx
def then(self, rhs, by=[]): # step? rw?
thm = infer(by + self.ctx, self.terms[-1] == rhs)
self.thm = infer([thm, self.thm], self.terms[0] == rhs)
self.thms.append(thm)
self.terms.append(rhs)
return self
def __eq__(self,rhs): #sadly the way python expands multiple == this does not work that great. needs parens
return self.then(rhs)
def simp(): # use z3 simplify. Weak though becaus can't be context aware
self.
return self
def egg_simp(self):
return self
def __repr__(self):
return " == ".join(map(repr, self.terms))
def __str__(self):
return repr(self)
def sympy():
return self
pass # use sympy to simplify, use z3 to confirm
def qed(self, by=[]):
if self.terms[-1] is not self.goal:
self.then(self.goal, by=by)
return self.thm
def calc(*steps): # a different syntax for calc
pf = Calc(steps[0], steps[-1])
for t in steps[1:-1]:
pf = pf.then(t)
return pf
from knuckledragger.kernel import trust
from z3 import *
Atom = DeclareSort("Atom")
a,b,c,d = Consts("a b c d", Atom)
ab = trust(a == b)
bc = trust(b == c)
cd = trust(c == d)
pf = Calc(a, d).then(b, by=[ab]).then(c, by=[bc]).then(d, by=[cd])
ad = pf.qed()
ad
#Calc(a,d, ctx=[ab,bc,cd]) == b == c == d
#((Calc(a,d, ctx=[ab,bc,cd]) == b) == c) == d
Functional Programming
One of the appeals of pure functional programming a la Haskell is that you can manipulate programs with pen and paper as you would an algebraic expression. With a simple manipulation you can express loop rearrangements that are rather complex. This is analogous in some respects to manipulating matrix expressions. The associativity of matrix multiplication is actually a somewhat complicated loop rearrangement too.
https://leahneukirchen.org/caudex/equational-reasoning.html This is a nice pile of links.
https://www.cs.nott.ac.uk/~pszgmh/tpfa.pdf Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
Hutton calculating compiler
See hlint rules https://github.com/ndmitchell/hlint/blob/master/data/hlint.yaml
Quickspec https://hackage.haskell.org/package/quickspec
Algebra of programming
Bird and Gibbons Books https://www.cs.ox.ac.uk/publications/books/functional/
%%file /tmp/lists.p
cnf('append_nil', axiom, append(nil, X, X)).
cnf('append_cons', axiom, append(cons(X,Xs), Ys) = cons(X, append(Xs,Ys))).
cnf(append_assoc, axiom, append(append(Xs,Ys),Zs) = append(Xs,append(Ys,Zs))).
cnf(rev_rev, axiom, comp(rev,rev) = id).
cnf(comp_assoc, axiom, comp(comp(X,Y),Z) = comp(X,comp(Y,Z))).
cnf(comp_id, axiom, comp(id,X) = X).
cnf(comp_id2, axiom, comp(X,id) = X).
cnf(map_fuse, axiom, map(comp(F,G)) = comp(map(F), map(G))).
cnf(map_id, axiom, map(id) = id).
length, app, cons, rev = functions("length app cons rev")
nil, X, Y, Z, Xs = consts("nil X Y Z Xs")
cons(X,nil)[2]
[length(nil) == 0,
length(cons(X,Xs)) == 1 + length(Xs),
app(nil, Y) == Y,
app(cons(X,Xs), Y) == cons(X, app(Xs, Y)),
rev(nil) == nil,
rev(cons(X,Xs)) == app(rev(Xs), cons(X,nil)),
]
%%file /tmp/compile.p
% https://www.cs.nott.ac.uk/~pszgmh/tpfa.pdf section 5
cnf(eval_val, axiom, eval(val(X)) = X).
cnf(eval_add, axiom, eval(add(X,Y)) = eval(X) + eval(Y)).
% code = list Op
% exec : code -> stack -> stack
% maybe I should use fof.
cnf(exec_nil, axiom, exec(nil, S) = S).
cnf(exec_push, axiom, exec(cons(push(N),Xs), Y) = exec(Xs, exec(X,Y))).
cnf(exec_add, axiom, exec(cons(add,Xs), cons(X,cons(Y,Z))) = cons(X+Y,Z)).
cnf(comp_val, axiom, comp(val(N)) = cons(push(N),nil)).
cnf(comp_add, axiom, comp(add(X,Y)) = append(comp(X), append(comp(Y), cons(add,nil)))).
% This won't prove I assume. It requires induction? The closure of the datatype?
% But it will come back saying it is consistent this is true?
cnf(comp_correct, conjecture, exec(comp(E), nil) = cons(eval(E), nil)).
Logic
Boolean (or otherwise) logic itself can be encoded as equational manipulation. This is perhaps not surprising, since boolean algebra is an algebra, and has it’s roots in analogy the the equational manipulation of polynomials. Boole himself I believe noted that true ~ 1, false ~ 0 and ~ time or ~ plus not ~ 1 - x and so on.
- Gries Logic https://www.cs.cornell.edu/gries/Logic/intro.html
- Mathmeth http://www.mathmeth.com/read.shtml
- https://www.cs.nott.ac.uk/~pszgmh/tpfa.pdf Theorem Proving for All: Equational Reasoning in
- https://smallbone.se/papers/horn.pdf Twee extended with Horn clauses via an equational encoding of if-then-else. Very interesting alternatives. This is of some relation to tricks in egglog for contextual rewriting. It is a form of tagging.
https://en.wikipedia.org/wiki/Boolean_algebra_(structure)
Algebra and Trig
You can encode trig and algebraic identities. This may be distressingly inefficient though. Maybe mixing a grobner basis system and a knuth bendix system better would work?
When I was more focussed on physics, basically all mathematics was equational manipulation. The generic facilities of sympy and Mathematica fall into this category (they also have massive piles of domain specific smarts about odes, pdes, special functions, etc).
The manipulations of algebraic equations or trigonometric identities. Things like cos(X)^2 + sin(X)^2 = 1
https://en.wikipedia.org/wiki/Category:Mathematical_identities anything called an identity is probably equational.
Some of the most interesting applications (integrals, summation) seem to require bound variables to model naturally. This is a perpetual bummer. The antiderivative example above is kind of a counterexample though. There are “coordinate free” styles that don’t use indices or bound variables. These seem more appropriate
%%file /tmp/trig.p
cnf(pythag, axiom, cos(X) * cos(X) + sin(X) * sin(X) = '1').
cnf(sin_sum, axiom, sin(X + Y) = sin(X) * cos(Y) + cos(X) * sin(Y)).
cnf(cos_sum, axiom, cos(X + Y) = cos(X) * cos(Y) - sin(X) * sin(Y)).
cnf(sin_diff, axiom, sin(X - Y) = sin(X) * cos(Y) - cos(X) * sin(Y)).
cnf(cos_diff, axiom, cos(X - Y) = cos(X) * cos(Y) + sin(X) * sin(Y)).
cnf(sin_double, axiom, sin('2' * X) = '2' * sin(X) * cos(X)).
cnf(cos_double, axiom, cos('2' * X) = cos(X) * cos(X) - sin(X) * sin(X)).
%%file /tmp/vector_calc.p
% https://en.wikipedia.org/wiki/Vector_algebra_relations
% https://en.wikipedia.org/wiki/Vector_calculus_identities
cnf(dot_comm, axiom, dot(X, Y) = dot(Y, X)).
cnf(add_comm, axiom, X + Y = Y + X).
cnf(add_assoc, axiom, X + (Y + Z) = (X + Y) + Z).
cnf(dot_distrib, axiom, dot(X, Y + Z) = dot(X, Y) + dot(X, Z)).
cnf(cross_antisym, axiom, cross(X, Y) = -cross(Y, X)).
% curl div grad
Writing /tmp/vector_calc.p
!twee /tmp/vector_calc.p --no-color
RESULT: Satisfiable (the axioms are consistent).
Syntax, Semantics, and Cost
We often want to talk about the “cost” of a term and extract a minimal one. There are a few approachest to this.
The system can’t internally differentiate between metalevel. If x + 0 = x for serious then size(x + 0) = 3 and size(0) = 1 are inconsistent. You can easily derive 3 = 1 via substitution. At the meta level we can recognize this though. So we could perhaps build our desires into the metalevel term ordering.
Another approach is to perform reflection of terms into our logic. We can make a distinction between the term (x + 0) and the related semantic value sem(x + 0) = sem(x) +_sem sem(0) = x_sem +_sem 0_sem = x_sem. We do equational reasoning on the semantic values, but can still internally talk about the cost of terms. The terms x + 0 != x aren’t equal but their semantic interpretations are. Then the question we want to ask is exists T, cost(T) <= 10 & sem(T) = sem(original_term). We can turn down 10 until it is no longer satisfiable to get a minimal cost term.
A related doubling approach has come up in the context of egglog when we have discussed using internal egglog functionality to program custom extraction criteria.
A function reify : Sem -> Term is also intriguing.
This approach does seem like it will be tough on our reasoning engine.
Set Theory
Some aspects of set theory can be easily modelled as equational manipulations. Not all though. The comphrehension principle is a pretty impportant part. I suspect it will be difficult to do this principle elegantly with equations. https://en.wikipedia.org/wiki/Category:Mathematical_identities https://en.wikipedia.org/wiki/List_of_set_identities_and_relations
%%file /tmp/set.p
cnf(union_empty, axiom, X ∪ ∅ = X).
cnf(idemp_union, axiom, X ∪ X = X).
cnf(comm_union, axiom, X ∪ Y = Y ∪ X).
cnf(assoc_union, axiom, X ∪ (Y ∪ Z) = (X ∪ Y) ∪ Z).
cnf(involution, axion, diff(X, diff(X, L)) = L).
Writing /tmp/set.p
Category Theory
An application I’ve been interested in for a while is category theory proof rewriting. This is kind of an offshoot of interest in functional programming and matrix expressions.
As a metasystem, we want to know that the type equations cannot be broken
GATs
# tp_eqs |- t : typ
# typ_eqs |- e1 = e2 : typ
class GAT:
t:
typ_eqs:
A,B,C,F,G,H = consts("A B C F G H")
id_, cod, dom, swap, dup, del_, pair, proj1, proj2 = functions("id cod dom swap dup del_ pair proj1 proj2")
axioms = [
id_(cod(F)) @ F == F,
F @ id_(dom(F)) == F,
F @ (G @ H) == (F @ G) @ H,
]
axioms
counter = 0
def tptp_axiom(axiom, name = None):
if name == None:
global counter
counter += 1
name = f"axiom{counter}"
return f"fof({name}, axiom, {axiom})."
def tptp_axioms(axioms):
return "\n".join(map(tptp_axiom, axioms))
print(tptp_axioms(axioms))
fof(axiom1, axiom, =(@(id(cod(F)),F),F)).
fof(axiom2, axiom, =(@(F,id(dom(F))),F)).
fof(axiom3, axiom, =(@(F,@(G,H)),@(@(F,G),H))).
https://www.cs.nott.ac.uk/~pszgmh/tpfa.pdf Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
Yea, equational definitions are really nice.
def define(eqs):
# first symbol is the same
# check termination
"""
let mut rules : Vec<Rewrite<CatLanguage, ()>> = vec![
vec![rw!( "dom(hom(a, b)) => a" ; "(dom (hom ?a ?b))" => "?a" )],
vec![rw!( "cod(hom(a, b)) => b" ; "(cod (hom ?a ?b))" => "?b" )],
vec![rw!( "type(id(a)) => hom(a, a)" ; "(type (id ?a))" => "(hom ?a ?a)" )],
vec![rw!( "type(f . g) => hom(dom(type(f)), cod(type(g)))" ; "(type (. ?f ?g))" => "(hom (dom (type ?f)) (cod (type ?g)))" )],
vec![rw!( "type(f om g) => hom(dom(type(f)) oo dom(type(g)), cod(type(f)) oo cod(type(g)))" ; "(type (om ?f ?g))" => "(hom (oo (dom (type ?f)) (dom (type ?g))) (oo (cod (type ?f)) (cod (type ?g))))" )],
vec![rw!( "type(a oo b) => :ob" ; "(type (oo ?a ?b))" => "ob" )],
vec![rw!( "type(munit()) => :ob" ; "(type munit)" => "ob" )],
vec![rw!( "type(swap(a, b)) => hom(a oo b, b oo a)" ; "(type (swap ?a ?b))" => "(hom (oo ?a ?b) (oo ?b ?a))" )],
vec![rw!( "type((del)(a)) => hom(a, munit())" ; "(type (del ?a))" => "(hom ?a munit)" )],
vec![rw!( "type(dup(a)) => hom(a, a oo a)" ; "(type (dup ?a))" => "(hom ?a (oo ?a ?a))" )],
vec![rw!( "type(pair(f, g)) => hom(dom(type(f)), cod(type(f)) oo cod(type(g)))" ; "(type (pair ?f ?g))" => "(hom (dom (type ?f)) (oo (cod (type ?f)) (cod (type ?g))))" )],
vec![rw!( "type(proj1(a, b)) => hom(a oo b, a)" ; "(type (proj1 ?a ?b))" => "(hom (oo ?a ?b) ?a)" )],
vec![rw!( "type(proj2(a, b)) => hom(a oo b, b)" ; "(type (proj2 ?a ?b))" => "(hom (oo ?a ?b) ?b)" )],
vec![rw!( "f . id(b) => f" ; "(. ?f (id ?b))" => "?f" )],
vec![rw!( "id(a) . f => f" ; "(. (id ?a) ?f)" => "?f" )],
vec![rw!( "a oo munit() => a" ; "(oo ?a munit)" => "?a" )],
vec![rw!( "munit() oo a => a" ; "(oo munit ?a)" => "?a" )],
rw!( "f . (g . h) == (f . g) . h" ; "(. ?f (. ?g ?h))" <=> "(. (. ?f ?g) ?h)" ),
vec![rw!( "id(munit()) om f => f" ; "(om (id munit) ?f)" => "?f" )],
vec![rw!( "f om id(munit()) => f" ; "(om ?f (id munit))" => "?f" )],
rw!( "a oo (b oo c) == (a oo b) oo c" ; "(oo ?a (oo ?b ?c))" <=> "(oo (oo ?a ?b) ?c)" ),
rw!( "f om (h om j) == (f om h) om j" ; "(om ?f (om ?h ?j))" <=> "(om (om ?f ?h) ?j)" ),
rw!( "id(a oo b) == id(a) om id(b)" ; "(id (oo ?a ?b))" <=> "(om (id ?a) (id ?b))" ),
vec![rw!( "(f . g) om (p . q) => (f om p) . (g om q)" ; "(om (. ?f ?g) (. ?p ?q))" => "(. (om ?f ?p) (om ?g ?q))" )],
rw!( "swap(a, b) . swap(b, a) == id(a oo b)" ; "(. (swap ?a ?b) (swap ?b ?a))" <=> "(id (oo ?a ?b))" ),
rw!( "(swap(a, b) om id(c)) . (id(b) om swap(a, c)) == swap(a, b oo c)" ; "(. (om (swap ?a ?b) (id ?c)) (om (id ?b) (swap ?a ?c)))" <=> "(swap ?a (oo ?b ?c))" ),
rw!( "(id(a) om swap(b, c)) . (swap(a, c) om id(b)) == swap(a oo b, c)" ; "(. (om (id ?a) (swap ?b ?c)) (om (swap ?a ?c) (id ?b)))" <=> "(swap (oo ?a ?b) ?c)" ),
rw!( "swap(a, munit()) == id(a)" ; "(swap ?a munit)" <=> "(id ?a)" ),
rw!( "swap(munit(), a) == id(a)" ; "(swap munit ?a)" <=> "(id ?a)" ),
vec![rw!( "swap(munit(), munit()) => id(munit() oo munit())" ; "(swap munit munit)" => "(id (oo munit munit))" )],
rw!( "dup(a) . ((del)(a) om id(a)) == id(a)" ; "(. (dup ?a) (om (del ?a) (id ?a)))" <=> "(id ?a)" ),
rw!( "dup(a) . (id(a) om (del)(a)) == id(a)" ; "(. (dup ?a) (om (id ?a) (del ?a)))" <=> "(id ?a)" ),
rw!( "dup(a) . swap(a, a) == dup(a)" ; "(. (dup ?a) (swap ?a ?a))" <=> "(dup ?a)" ),
rw!( "(dup(a) om dup(b)) . ((id(a) om swap(a, b)) om id(b)) == dup(a oo b)" ; "(. (om (dup ?a) (dup ?b)) (om (om (id ?a) (swap ?a ?b)) (id ?b)))" <=> "(dup (oo ?a ?b))" ),
rw!( "dup(a) . (dup(a) om id(a)) == dup(a) . (id(a) om dup(a))" ; "(. (dup ?a) (om (dup ?a) (id ?a)))" <=> "(. (dup ?a) (om (id ?a) (dup ?a)))" ),
rw!( "(del)(a oo b) == (del)(a) om (del)(b)" ; "(del (oo ?a ?b))" <=> "(om (del ?a) (del ?b))" ),
rw!( "dup(munit()) == id(munit())" ; "(dup munit)" <=> "(id munit)" ),
rw!( "(del)(munit()) == id(munit())" ; "(del munit)" <=> "(id munit)" ),
vec![rw!( "pair(f, k) => dup(dom(type(f))) . (f om k)" ; "(pair ?f ?k)" => "(. (dup (dom (type ?f))) (om ?f ?k))" )],
rw!( "proj1(a, b) == id(a) om (del)(b)" ; "(proj1 ?a ?b)" <=> "(om (id ?a) (del ?b))" ),
rw!( "proj2(a, b) == (del)(a) om id(b)" ; "(proj2 ?a ?b)" <=> "(om (del ?a) (id ?b))" ),
vec![rw!( "f . (del)(b) => (del)(dom(type(f)))" ; "(. ?f (del ?b))" => "(del (dom (type ?f)))" )],
vec![rw!( "f . dup(b) => dup(dom(type(f))) . (f om f)" ; "(. ?f (dup ?b))" => "(. (dup (dom (type ?f))) (om ?f ?f))" )],
vec![rw!( "dup(a) . (f om f) => f . dup(cod(type(f)))" ; "(. (dup ?a) (om ?f ?f))" => "(. ?f (dup (cod (type ?f))))" )],
].concat();
"""
- Functional Programming
- Manifold differentiation
- simplicial sets
-
database migration
- nonstandard analysis - an equational theorem prover purpose built would be cool
Homotopy
path. It makes sense rewriting and homotopy/homology might be related.
https://www.philipzucker.com/z3-and-the-word-problem/ I discussed this here.
paths are string rewriting a(b(c(X))) homology makes the strings commutative.
%%file /tmp/path.p
% simple normalization
cnf(stayput, axiom, path(A,path(A, P)) = path(A,P)).
cnf(backup, axiom, path(A,path(B, path(A, P))) = path(A, P)).
%cnf(disjoint1, axiom, a != b). % not really necessary
%cnf(disjoint2, axiom, b != c).
%cnf(disjoint3, axiom, a != c).
cnf(circle, conjecture, path(a,path(b, path(c, path(a, nil)))) = path(a,nil)).
%cnf(null_loop, conjecture, path(a, path(c,path(b, path(c, path(a, nil))))) = path(a,nil)).
Overwriting /tmp/path.p
!twee /tmp/path.p
Here is the input problem:
Axiom 1 (stayput): path(X, path(X, Y)) = path(X, Y).
Axiom 2 (backup): path(X, path(Y, path(X, Z))) = path(X, Z).
Goal 1 (circle): path(a, path(b, path(c, path(a, nil)))) = path(a, nil).
1. path(X, path(X, Y)) -> path(X, Y)
2. path(X, path(Y, path(X, Z))) -> path(X, Z)
Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
path(X, path(X, Y)) -> path(X, Y)
path(X, path(Y, path(X, Z))) -> path(X, Z)
RESULT: CounterSatisfiable (the conjecture is false).
%%file /temp/edge.p
cnf(edge, axiom, edge(a,b)).
Countersatisfiable means there exists a model in which this is not true. If i ask !=, there is also a model in which it is true, which is not of interest to me. Yes. Models is the wrong language of discussion.
"""
"""
%%file /tmp/group1.p
%pg 5 of traat
cnf(assoc, axiom, mul(mul(X,Y),Z) = mul(X,mul(Y,Z))).
cnf(left_inv, axiom, mul(i(X), X) = e).
cnf(left_id, axiom, mul(e, X) = X).
%cnf(rightinv ,conjecture, mul(X, i(X)) = e).
cnf(rightid ,conjecture, mul(X, e) = X).
Overwriting /tmp/group1.p
!twee /tmp/group1.p
Here is the input problem:
Axiom 1 (assoc): mul(mul(X, Y), Z) = mul(X, mul(Y, Z)).
Axiom 2 (left_inv): mul(i(X), X) = e.
Axiom 3 (left_id): mul(e, X) = X.
Goal 1 (rightid): mul(sK1_rightid_X, e) = sK1_rightid_X.
1. mul(mul(X, Y), Z) -> mul(X, mul(Y, Z))
2. mul(i(X), X) -> e
3. mul(e, X) -> X
4. mul(i(X), mul(X, Y)) -> Y
5. mul(i(e), X) -> X
6. mul(i(i(X)), e) -> X
7. mul(i(i(X)), Y) -> mul(X, Y)
8. mul(X, e) -> X
The conjecture is true! Here is a proof.
Axiom 1 (assoc): mul(mul(X, Y), Z) = mul(X, mul(Y, Z)).
Axiom 2 (left_inv): mul(i(X), X) = e.
Axiom 3 (left_id): mul(e, X) = X.
Lemma 4: mul(i(X), mul(X, Y)) = Y.
Proof:
mul(i(X), mul(X, Y))
= { by axiom 1 (assoc) }
mul(mul(i(X), X), Y)
= { by axiom 2 (left_inv) }
mul(e, Y)
= { by axiom 3 (left_id) }
Y
Goal 1 (rightid): mul(sK1_rightid_X, e) = sK1_rightid_X.
Proof:
mul(sK1_rightid_X, e)
= { by lemma 4 }
mul(i(i(sK1_rightid_X)), mul(i(sK1_rightid_X), mul(sK1_rightid_X, e)))
= { by lemma 4 }
mul(i(i(sK1_rightid_X)), e)
= { by axiom 2 (left_inv) }
mul(i(i(sK1_rightid_X)), mul(i(sK1_rightid_X), sK1_rightid_X))
= { by lemma 4 }
sK1_rightid_X
RESULT: Theorem (the conjecture is true).
Early Termination
Give it a conjecture it can’t possibly prove. There are a couple early stoppage criteria. But also if you give it a ground system it Must stop.
This ground system is an egraph.
Can I explicitly show this via the “skolemization”.
Introduce a new constant for every greater than depth 1 term. These represent the eclasses Probably KBO will rewrite to this term. Hence the eclasses eclass to eclass rewrites represent the union find. e1 -> e6 f(e1,e2,e3) -> e4 represent the enode f(e1,e2,e3) is in eclass e4
%%file /tmp/ground.p
cnf(ax1, axiom, add(one,two) = three).
cnf(ax2, axiom, add(two,one) = three).
cnf(ax3, axiom, add(one,three) = four).
cnf(ax4, axiom, add(three,one) = four).
cnf(ax5, axiom, add(two,three) = five).
cnf(ax6, axiom, add(three,two) = five).
cnf(ax7, axiom, add(four,one) = five).
cnf(ax8, axiom, add(one,four) = five).
%cnf(assoc, axiom, add(add(X,Y),Z) = add(X,add(Y,Z))).
%cnf(comm, axiom, add(X,Y) = add(Y,X)).
cnf(conj, conjecture, x = y).
Overwriting /tmp/ground.p
! twee /tmp/ground.p
Here is the input problem:
Axiom 1 (ax1): add(one, two) = three.
Axiom 2 (ax2): add(two, one) = three.
Axiom 3 (ax3): add(one, three) = four.
Axiom 4 (ax4): add(three, one) = four.
Axiom 5 (ax5): add(two, three) = five.
Axiom 6 (ax6): add(three, two) = five.
Axiom 7 (ax7): add(four, one) = five.
Axiom 8 (ax8): add(one, four) = five.
Goal 1 (conj): x = y.
1. add(one, two) -> three
2. add(two, one) -> three
3. add(one, three) -> four
4. add(three, one) -> four
5. add(two, three) -> five
6. add(three, two) -> five
7. add(four, one) -> five
8. add(one, four) -> five
Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
add(one, two) -> three
add(one, three) -> four
add(one, four) -> five
add(two, one) -> three
add(two, three) -> five
add(three, one) -> four
add(three, two) -> five
add(four, one) -> five
RESULT: CounterSatisfiable (the conjecture is false).
–expert-help –conjecture 2 –root tpt root path –trace file module. print prolog trace.
ok, give it an impossible equality goal + max-cps
let
state' = interreduce config state
score rule =
(KBO.size (lhs rule), lhs rule,
KBO.size (rhs rule), rhs rule)
actives =
sortBy (comparing (score . active_rule)) $
IntMap.elems (st_active_set state')
forM_ actives $ \active ->
putStrLn (" " ++ prettyShow (canonicalise (active_rule active)))
putStrLn ""
simp_db = []
def match(pattern, expr):
env = {}
stack = [(pattern, expr)]
while len(stack) > 0:
p, e = stack.pop()
if isinstance(p, str)
if isUpper(p[0]):
if p in env:
if env[p] != e:
return False
else:
env[p] = e
else:
if p != e:
return False
elif isinstance(p, list):
if isinstance(e, list):
if len(p) != len(e):
return False
stack.extend(zip(p, e))
else:
return False
def simp(name, *args):
# https://www.cs.utexas.edu/users/moore/acl2/v8-5/combined-manual/index.html?topic=ACL2____BUILT-IN-THEOREMS
def builtin_simp(expr):
match expr:
case ("and", "true", *args):
return args
case ("or", "true", *args):
return "true"
case ("or", "false", *args):
return args
def parse_expression(expr):
# finds a stream of tokens. Ignores whitespace and ignores commas. Clever
# But also misparses bad input?
tokens = re.findall(r'\(|\)|[^\s(),]+', expr)
def parse():
ast = []
while tokens:
token = tokens.pop(0)
if token == '(':
ast.append(parse()) # Parse nested expression
elif token == ')':
return ast # End current expression
else:
ast.append(token) # Add identifier/literal to current list
return ast
return parse()
expr = 'foo(bar(biz boz,baz), X)'
ast = parse_expression(expr)
ast
# https://docs.python.org/3/library/re.html#writing-a-tokenizer
['foo', ['bar', ['biz', 'boz', 'baz'], 'X']]
spec = [
("LPAREN", r"\("),
("RPAREN", r"\)"),
("ID", r"[a-zA-Z_][a-zA-Z0-9_]*"),
("NUMBER", r"\d+"),
("PLUS", r"\+"),
("TIMES", r"\*"),
("EQUALS", r"="),
("WS", r"\s+"),
]
tok_regex = '|'.join(f"(?P<{name}>{regex})" for name, regex in spec)
for mo in re.finditer(tok_regex, "foo(bar(biz boz,baz), X)"):
print(mo.lastgroup, mo.group(), mo.start())
ID foo 0
LPAREN ( 3
ID bar 4
LPAREN ( 7
ID biz 8
WS 11
ID boz 12
ID baz 16
RPAREN ) 19
WS 21
ID X 22
RPAREN ) 23