Constructing infinite models for non-implications

Stream: Equational

[Daniel Weber]

(This is a follow-up to #Equational > Dynamically detecting useful implications to decide )
From the results of equational#230, many of the remaining open implications are false, but seemingly don't have finite models showing that (at least Vampire couldn't find them, and in one random case I manually proved the implication for finite models).
How can these non-implications be automatically formally proven?
Vampire outputs something along the lines of

% # SZS output start Saturation.
cnf(u12,axiom,
    mul(X0,X1) = mul(mul(X2,X3),mul(mul(X0,X1),mul(X2,X3)))).

cnf(u9,axiom,
    mul(X0,X1) = mul(mul(X2,mul(X0,X1)),X2)).

cnf(u10,negated_conjecture,
    mul(sK0,sK1) != mul(sK2,mul(mul(sK0,sK1),sK2))).

% # SZS output end Saturation.

and formalizing that would require, as far as I can tell, formalizing superposition calculus, proving its completeness, and then proving for each such output that these are truly saturated -- this sounds quite unpleasant, and will probably take a really long time for the kernel to verify as well.
What are other automated approaches that could be used for proving such non-implications?

[Terence Tao]

Do you have an example of such a non-implication that we could play with directly?

[Will Sawin]

One could attempt a brute force approach similar to what's successful for finite models: First assemble a list of infinite models that have been used to prove non-implications, then come up with a means of constructing infinite models that can construct all of those, use it to construct a bunch of models, see which equations seem to hold by plugging in small or random values for the variables, see if this gives any non-implications, then try to automate the proof that these equations actually hold. Most steps of that seem tricky.

[Will Sawin]

Alternately one could try to understand the theory of saturation in superposition calculus and extract from it some procedure for producing proofs in specific cases (by some complicated induction? By producing tailor-made models?) and formalize and then automate that.

[lyphyser]

my egraph-based tool also reports saturation with no solutions for several of the post-Vampire unknown implications, and can output the egraph

I think there is already a proof that refl+trans+congr+symm+hyp is complete in the metatheory code, so perhaps one can present the egraph to Lean, show that it doesn't solve the problem and show that no further moves are possible

probably not going to do this myself though except maybe for printing the egraphs if they are useful

[Daniel Weber]

Terence Tao said:

Do you have an example of such a non-implication that we could play with directly?

There is x ∘ y = (z ∘ (x ∘ y)) ∘ z -> x ∘ y = z ∘ ((x ∘ y) ∘ z), the saturation above the is the output for it

[Daniel Weber]

lyphyser said:

my egraph-based tool also reports saturation with no solutions for several of the post-Vampire unknown implications, and can output the egraph

I think there is already a proof that refl+trans+congr+symm+hyp is complete in the metatheory code, so perhaps one can present the egraph to Lean, show that it doesn't solve the problem and show that no further moves are possible

probably not going to do this myself though except maybe for printing the egraphs if they are useful

Could you give an example of how such an egraph looks? I must admit that I don't quite understand how to interpret the output of Vampire, perhaps using egraphs will be easier

[Will Sawin]

a ∘ b = a xor b if a,b are both even, b+2a if a odd and b even, max(a-2b,0) if a even and b odd, a+b if a,b odd should do it: then x ∘ y is even and if z is even then multiplying by z on either side is an inverse but if z is odd multiplying by z is an inverse one way and not the other.

[Daniel Weber]

Will Sawin said:

a ∘ b = a xor b if a,b are both even, b+2a if a odd and b even, max(a-2b,0) if a even and b odd, a+b if a,b odd should do it: then x ∘ y is even and if z is even then multiplying by z on either side is an inverse but if z is odd multiplying by z is an inverse one way and not the other.

Yes, a model for this is already formalized (it's almost exactly what you've written, even)

[Will Sawin]

Oh, sorry.

[Will Sawin]

An interesting thing about that example from a human perspective, is if I was going to do a proof from the other angle, a syntactic proof based on rewriting formulas or somewhat equivalently a semantic proof based on a free model, it would make sense to add two more equations, those being (x ∘ y) ∘ (z ∘ w) = (z ∘ w) ∘ (x ∘ y) and the associativity for terms of the form (x ∘ y) which I won't write out. Then the terms of the form x ∘ y form a commutative group where every element has order 2 and the other terms act by permutations. It's not so hard to write out in a human-readable way the description of the equivalence classes of formulas / the elements of a free algebra on k generators. So one could try the general strategy of adding more equations, checking that the implication still doesn't hold in vampire, and trying to generate a proof of the new implication which might be easier. But this seems not so likely to help on the formalization side - presumably trying to find the right equations to add is harder than everything else about the problem.

[Amir Livne Bar-on]

Did the Vampire proofs merge include the non-implications as conjectures then? Or not at all?

[Daniel Weber]

It didn't include the non-implications. I have equational#276 with finite counterexamples generated by Vampire, but the conjectures are currently a draft (as I need to remove the implications/non-implications that were proven from there)

[Amir Livne Bar-on]

(deleted)

[Amir Livne Bar-on]

(I now realize that my tone wasn't very nice, and it's a useless thing to say anyway; apologies)

[Daniel Weber]

Will Sawin said:

One could attempt a brute force approach similar to what's successful for finite models: First assemble a list of infinite models that have been used to prove non-implications, then come up with a means of constructing infinite models that can construct all of those, use it to construct a bunch of models, see which equations seem to hold by plugging in small or random values for the variables, see if this gives any non-implications, then try to automate the proof that these equations actually hold. Most steps of that seem tricky.

A potential method to construct infinite models is to have a finite automaton with output read two words interlaced. Checking equations over this is decidable, which is good, but I'm not sure if it's expressive enough (we can't do stuff like x ◇ y = if x = y then 0 else x, for example)

[lyphyser]

so it seems a lot of the egraphs have just the goal, indicating that no moves are possible from the beginning and the others that I have found so far running on the post-Vampire unknowns are also very small

this is one of the biggest saturated ones found so far, for 3279 => 3659
3279_3659.pdf
3279_3659.dot

[Daniel Weber]

lyphyser said:

so it seems a lot of the egraphs have just the goal, indicating that no moves are possible from the beginning and the others that I have found so far running on the post-Vampire unknowns are also very small

this is one of the biggest saturated ones found so far, for 3279 => 3659
3279_3659.pdf
3279_3659.dot

How many of the implications are you able to resolve, if you add these as conjectures?

[lyphyser]

haven't tried that yet

[lyphyser]

4407 => 4343 is e.g. one where no moves are possible at all

[lyphyser]

646 => 630 has a large saturated egraph

[Daniel Weber]

Will Sawin said:

One could attempt a brute force approach similar to what's successful for finite models: First assemble a list of infinite models that have been used to prove non-implications, then come up with a means of constructing infinite models that can construct all of those, use it to construct a bunch of models, see which equations seem to hold by plugging in small or random values for the variables, see if this gives any non-implications, then try to automate the proof that these equations actually hold. Most steps of that seem tricky.

This seems like a good idea, but intuitively I feel like for infinite models you need to be a lot more "intentional", especially as implications which are only refuted on infinite models hold "often"

[lyphyser]

I'm working on the Lean code to provide egraph-based counterexamples, I think it should work at least with native_decide

[Daniel Weber]

From saturation? Nice! Do you have a prediction for how many implications it'll resolve?

[David Renshaw]

I think native_decide will trip this axiom check: https://github.com/teorth/equational_theories/blob/05138bbe6816e64322a6ddd71202516413e61b5b/equational_theories/EquationalResult.lean#L77-L78
(which we could discuss relaxing)

[Daniel Weber]

If it works with native_decide then I could try to write a tactic to prove it, perhaps that'll be fast enough for the kernel

[Will Sawin]

Daniel Weber said:

s seems like a good idea, but intuitively I feel like for infinite models you need to be a lot more "intentional", esp

It's kind of an empirical question. It's actually not clear to me that the implications only refuted on infinite models hold that often. I mean, it's rare for any complicated equation to hold, but if one equation holds, and some natural injective map fails to be surjective, it might be pretty likely for the second equation to fail. So if one has a model which frequently produces injective-not-surjective maps (or other "signatures" of an infinite magma?) one might be in good shape. The automaton idea you suggested might be good for this. The thing that makes sense to me to do is to take 5 or 10 random examples of implications believed to be true in the finite case and false in the infinite case and search for infinite models by hand, then use insights from that to see if the brute force method is viable and then to power the brute force method.
But this all might be moot if lyphyser or anyone else can get the vampire proofs of nonimplications into Lean (unless it comes up later for the ones undecided by vampire).

[lyphyser]

If I'm not mistaken I realized that I think that (finite) saturated egraphs give finite models, not infinite models, where the elements are Option (Fin C) where C is the number of eclasses, and the operation is none if any operands are none or if the operation is not in the egraph, and the resulting eclass otherwise

I wonder if I'm missing something though (I think the argument may only work if the set of variables in the axiom lhs and rhs are the same)

[Notification Bot]

A message was moved here from #Equational > Automatically generating magma laws & proofs from equations by lyphyser.

[Andrés Goens]

lyphyser said:

If I'm not mistaken I realized that I think that (finite) saturated egraphs give finite models, not infinite models, where the elements are Option (Fin C) where C is the number of eclasses, and the operation is none if any operands are none or if the operation is not in the egraph, and the resulting eclass otherwise

I wonder if I'm missing something though (I think the argument may only work if the set of variables in the axiom lhs and rhs are the same)

what's the construction precisely? note that a saturated egraph can represent an infinite set of terms if there's cycles

[Andrés Goens]

really cool idea by the way!

[Cody Roux]

Terms != elements of the model though

[Andrés Goens]

(that's why I'm asking what the construction is precisely)

[Daniel Weber]

Could you perhaps explain how this works for the non-implication x = x * y -> x = y? The only model with a none such that x * none = none which satisfies the equation is the trivial one

[lyphyser]

I think it only works when the set of variables in the lhs and the rhs are the same (which means that any variable being none makes both the lhs and rhs none and thus the equation true)

[David Renshaw]

I formalized theorem 3.10 from blueprint.pdf, constructing an infinite model to prove that Eq3944 does not imply Eq3588: equational#388.

[David Renshaw]

and the dual: equational#390

[Daniel Weber]

David Renshaw said:

I formalized theorem 3.10 from blueprint.pdf, constructing an infinite model to prove that Eq3944 does not imply Eq3588: equational#388.

It already exists: https://github.com/teorth/equational_theories/blob/main/equational_theories/InfModel.lean#L147

[David Renshaw]

d'oh. Needed to tag it with @[equational_result].

[David Renshaw]

I suppose I should merge InfiniteModels.lean into InfModel.lean. (clearly I must have seen this file earlier, based on the name I chose. :man_facepalming:)

[David Renshaw]

@Daniel Weber is there some kind of procedure you followed to come up with this model? How can we replicate it for the other missing refutations?

[Daniel Weber]

I found it from the proof for finite models, by looking at what breaks there in infinite models

[David Renshaw]

equational#391

[Will Sawin]

I'm pretty sure the proof used in InfModel.lean for Equation3994_not_implies_Equation3588 works verbatim for Equation3994_not_implies_Equation3456 since the counterexample part uses 1,1,1 so it still holds if you set the variables even. Similarly the proof of Equation3588_not_implies_Equation3944 in fact shows Equation3588_not_implies_Equation3862. By transitivity, I think this resolves all implications of these two equations.

[Daniel Weber]

I wonder if untyped lambda calculus can provide an interesting model

[Phil]

One of the theories further on a scale of expressiveness that models infinite data and is still computable is tree automata. I don't have much experience in Lean, but here's a rough idea.

There's a library called qpf that allows to define codata in Lean.

Consider (fixpoint of) random polynomial functor F and (fixpoint of) random function g of type forall a. F a -> F a -> F a to be magma operation.

Values of Fix F are equivalent to tree automata with every edge ascribed with a triple (i1, i2, o) of 2 expected constructors and another constructor of F as output.

After magma operation (bifix g) is applied on either side of equation, we're left with 2 tree automata. Equality on tree automata is well-defined, because they have normal forms by Hopcroft's minimization.

So on Python side it's possible to generate F/g and check if axiom of equational theory works, on Lean side encoding of F and g will be just codata of Fix F and function g, and there won't be any need to explicitly define either tree automata or their theory.

[Daniel Weber]

The data itself doesn't have to be infinite - $\mathbb{N}$ is enough, the problem is describing the operation on it

[Daniel Weber]

S2S can't quantify over functions, right? Is there any decidable theory which can quantify over a reasonably expressive set of functions?