Group theory crash #519
Comments
|
Right, rule like |
|
Thanks! egglog accepts that just fine. But how do I get it to check equality of ground terms? I try:
(check (= (id) (id)))
But it says check failed.
… On Feb 10, 2025, at 11:00 PM, Yihong Zhang ***@***.***> wrote:
Right, rule like a -> (plus a (id)) is supported in egg, but not directly in egglog. As egglog translates rules to Datalog/chase-like rules, all variables need to be bound. A standard workaround is to use a universe relation:
(datatype G
(id)
(inv G)
(plus G G)
)
(relation universe (G))
(rule ((= e (id))) ((universe e)))
(rule ((= e (inv a))) ((universe e)))
(rule ((= e (plus a b))) ((universe e)))
(birewrite (plus (plus a b) c) (plus a (plus b c)))
(birewrite (plus a (id)) a :when ((universe a)))
(birewrite (plus (inv a) a) (id) :when ((universe a)))
;; which gets translate to two (slightly inefficient) rules
;; (rule ((= e (plus (inv a) a)) (universe a)) ;; we don't need (universe a) here
;; ((union a (id))))
;; (rule ((= e (id)) (universe a))
;; ((union a (plus (inv a) a))))
—
Reply to this email directly, view it on GitHub <#519 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA2QKN4T2KKM6TFZBQENWP32PGNZVAVCNFSM6AAAAABW35WJYCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMNBZHE3TCNZZGY>.
You are receiving this because you authored the thread.
|
|
In this case, |
|
Thanks! This all makes sense. But suppose I omitted your rule that ab=1 -> {b=a^1, a=b^-1}. Will it be the case that the check of “iab = ibia” can be made to succeed by choosing a high enough number with “run” (e.g. > 5, possibly infinity)? In other words, can egglog decide the ground word problem in the free group on two generators using only the three equations as given?
I ask because I am interested in using it as an automated theorem prover for equational logic (as well as a Skolem chase engine), and hope that I’m not conflating EggLog with Egg with EqSat.
… On Feb 11, 2025, at 12:14 AM, Yihong Zhang ***@***.***> wrote:
In this case, (id) has not been populated in the "database", and checking (= (id) (id)) implicitly checks the existence of (id), so it failed. It would work if we manually insert (id) into the database. I also made a slightly more involved example here.
(datatype G
(id)
(inv G)
(plus G G)
)
(relation universe (G))
(rule ((= e (id))) ((universe e)))
(rule ((= e (inv a))) ((universe e)))
(rule ((= e (plus a b))) ((universe e)))
(birewrite (plus (plus a b) c) (plus a (plus b c)))
(birewrite (plus a (id)) a :when ((universe a)))
(birewrite (plus (id) a) a :when ((universe a)))
(birewrite (plus (inv a) a) (id) :when ((universe a)))
(birewrite (plus a (inv a)) (id) :when ((universe a)))
;; ab=1 --> b=a^-1
(rule ((= (id) (plus a b)))
((union b (inv a))
(union a (inv b))))
;; need to populate (id) in the e-graph first
(id)
(check (= (id) (id)))
(constructor a () G)
(constructor b () G)
(let iab (inv (plus (a) (b))))
(let ibia (plus (inv (b)) (inv (a))))
(run 5)
(check (= iab ibia))
—
Reply to this email directly, view it on GitHub <#519 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA2QKN432PQFIXOTCF3RSUD2PGWMRAVCNFSM6AAAAABW35WJYCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMNJQGA4DGMJUGM>.
You are receiving this because you authored the thread.
|
|
Yes! The issue I had in my previous program is that it didn't put a and b into the universe relation. We don't actually need the extra rule |
|
That’s great, this shows how to solve the ground word problem in universal algebra. If you’ll indulge me, I have two hopefully final questions:
1) how does this work with multiple sorts? For example, if I wanted to use a multi-sorted structure such as a category instead of a group, where the constructors depend on two sorts, Ob and Hom, how would the syntax change?
2) can this solution to the ground word problem be lifted to the full word problem? For example, in this scenario, if I take “forall c, c+a = c+b” and skolemize c into a fresh constant will egglog prove "c+a=c+b” if and only if “forall c, c+a = c+b” holds in the free group on two generators? In fact, I'm most curious in if it can handle equational entailment checking via skolemization, proving something like "(forall c, c+a = c+b) -> (forall d, a+d = b+d)" via skolemization and running forever. (I'm guessing Egglog can semi-decide entailment of cartesian theories (skolemized horn theories) but this has to be proven and I'm looking for a proof.)
Question 2 can be more subtle than it looks. Unfailing Knuth-Bendix completion, for example, solves the ground word problem, but simply skolemizing and running forever does *not* turn it into a semi-decision procedure for equational logic. (You have to make use of “refutational completeness” and encode some boolean logic to do so: see theorem 4.34 of https://rg1-teaching.mpi-inf.mpg.de/autrea-ss12/slides/slides21.pdf for example).
… On Feb 11, 2025, at 11:24 AM, Yihong Zhang ***@***.***> wrote:
Yes! The issue I had in my previous program is that it didn't put a and b into the universe relation. We don't actually need the extra rule
(datatype G
(id)
(inv G)
(plus G G)
)
(relation universe (G))
(rule ((= e (id))) ((universe e)))
(rule ((= e (inv a))) ((universe e)))
(rule ((= e (plus a b))) ((universe e)))
(birewrite (plus (plus a b) c) (plus a (plus b c)))
(birewrite (plus a (id)) a :when ((universe a)))
(birewrite (plus (id) a) a :when ((universe a)))
(birewrite (plus (inv a) a) (id) :when ((universe a)))
(birewrite (plus a (inv a)) (id) :when ((universe a)))
(constructor a () G)
(constructor b () G)
(universe (a))
(universe (b))
(push)
(union (id) (plus (a) (b)))
(run 5)
(check (= (a) (inv (b))))
(pop)
(push)
(let iab (inv (plus (a) (b))))
(let ibia (plus (inv (b)) (inv (a))))
(run 5)
(check (= iab ibia))
(pop)
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you authored the thread.Message ID: ***@***.***>
|
This was referenced Feb 12, 2025
Is this something you have in mind? Assuming I understand your question correctly, I think this is hard in current egglog, since egglog does not have real parametric/dependent types. Real parametric/dependent types introduce problems since each function is supposed to be backed by a database table, and it's not clear when to instantiate a parametric function (like
Does it suffice to show EqSat subsumes Skolem chase (which we show in the semantics paper)?
I think egglog can prove |
|
Thanks again for your response!
Dependent sorts are nice, but I really just mean multiple sorts, something like this for the action of a group on a set:
(datatype G A
(id : G)
(inv : G -> G)
(plus : G * G -> G)
(action : G * A -> A)
)
For categories in particular, they can be axiomatized using cartesian logic, so dependent sorts shouldn’t be necessary, just constructors that can use multiple sorts. Encoding multiple sorts into a single sort leads to verbosity that I’d like to avoid.
—
It wouldn’t surprise me if Egglog could decide the full word problem for universal algebra, but it has to be proven (at least, based solely on the Suciu paper). This is because in general, there is no way to turn an arbitrary semi-decision procedure for ground equality in universal algebra into a semi-decision procedure for non-ground equality:
Suppose I have a semi-decision procedure F : (s:Signature) -> (t:EquationalTheory s) -> (t1:GroundTerm t) -> (t2:GroundTerm t)->Bool, which is one way to understand EggLog based on the Suciu Paper. And suppose I want to implement a semi-decision procedure of type (s:Signature) -> (t:EquationalTheory s) -> (t1’:Term t) -> (t2’:Term t)->Bool. I might try to skolemize t1 and t2, resulting in ground terms on a signature s’ that is larger than s. But F only proves equality in the smaller vocabulary s! I can’t even invoke my original ground semi-decider F on the skolemizations of t1 and t2, because the skolemizations live in a different signature than the original terms. Type error!
So, for systems that prove the full world problem from the ground one, they have to show how. Sometimes, this can be trivial; maybe F can be directly used on the skolemized terms regardless of the change in signature. Sometimes, it is not: in unfailing knuth bendix completion, for example, you can’t just apply F directly to the skolemized terms, that results in incompleteness. Instead, you also have to change the theory t to talk about the new Skolem constants, and ensure they are “smaller” than all other constants, and use a refutational completeness property of the knuth bendix algorithm in order to prove completeness of F on s’.
At a practical level, I’m trying to connect egglog to CQL (http://categoricaldata.net), and so I’m trying to understand if I can do so “directly” (pick my own Skolem constants and pass the skolemized terms to egglog), or if something more involved is required (pick my own Skolem constants and then pass the skolemized terms to egglog but where egglog is run on a non-trivially different theory than I started with), to retain completeness (all provable (not necessarily ground) equalities eventually terminate with ’true’).
It's possible the Skolem chase may semi-decide the full word problem; I'll try to find a proof. I had mostly been thinking about how to use EqSat for the full word problem.
… On Feb 12, 2025, at 7:43 PM, Yihong Zhang ***@***.***> wrote:
how does this work with multiple sorts? For example, if I wanted to use a multi-sorted structure such as a category instead of a group, where the constructors depend on two sorts, Ob and Hom, how would the syntax change?
Is this something you have in mind?
(sort Ob)
(sort (Hom a b) for ((a b : Ob)))
(function id () (Hom a b) for ((a b : Ob)))
Assuming I understand your question correctly, I think this is hard in current egglog, since egglog does not have real parametric/dependent types. This also introduces new problems since each function is backed by a database table, and it's not clear when to instantiate a parametric function (like id) with concrete types.
I'm guessing Egglog can semi-decide entailment of cartesian theories (skolemized horn theories)
Does it suffice to show EqSat subsumes Skolem chase (which we show in the semantics paper)?
• can this solution to the ground word problem be lifted to the full word problem?
I think egglog can prove forall c, c+a = c+b by skomizing c to an uninterpreted constant. For entailment, if you have forall c, c+a = c+b an axiom and check if a+d() = b+d() holds (for Skolem constant d()), would that just work?
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you authored the thread.Message ID: ***@***.***>
|
Yeah egglog supports multiple sorts. There are also many examples in the web demo.
I never thought of it! This sounds interesting. Yes EqSat can semi-decide the ground word problem but I kinda just take the full word problem for granted. Let me know if you make any new discoveries about the connection between EqSat and the full word problem. |
|
I was about to write to Dan Suciu and ask if he knew if EqSat generalized to the full word problem, or if SkChase can solve the full word problem, when I realized you know him better than I do :-). With the multi-sorted syntax I have enough to start attaching egglog to CQL, but ultimately the completeness and possibly even soundness of doing so will hinge on the open questions described in this thread.
Here's a concrete example of what might go wrong lifting a ground word problem solver to the full word problem; I'm not quite sure how to test this in Egglog, but maybe you can help?
Let the signature have two sorts, "Void" and "nat" and two constants "one:nat" and "two:nat".
Then "one = two" should not be provable, but "forall x:Void, one = two" should be provable (according to the usual rules of multi-sorted equational logic with empty sorts).
But if you skolemize variable x into a fresh constant x', there's no proof rule to allow concluding one=two in an empty context with Void inhabited by constant x'.
What would egglog do here?
FWIW, empty sorts pop up in CQL a lot, because empty sorts are interpreted as empty database tables. This problem also comes up with entailment checking: the check {Nat,Void,one:Nat,two:Nat} |- {Nat,Void,one:Nat,two:Nat,forall x:Void, one = two} would come up when trying to prove that inclusion functors between algebraic theories are actually functorial.
… On Feb 17, 2025, at 2:24 PM, Yihong Zhang ***@***.***> wrote:
yihozhang
left a comment
(egraphs-good/egglog#519)
something like this for the action of a group on a set
Yeah egglog supports multiple sorts. There are also many examples in the web demo.
(datatype*
(G
(id)
(inv G)
(plus G G))
(A
(action G A)))
in general, there is no way to turn an arbitrary semi-decision procedure for ground equality in universal algebra into a semi-decision procedure for non-ground equality
I never thought of it! This sounds interesting. Yes EqSat can semi-decide the ground word problem but I kinda just take the full word problem for granted. Let me know if you make any new discoveries about the connection between EqSat and the full word problem.
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you authored the thread.
<#519 (comment)> <https://github.com/notifications/unsubscribe-auth/AA2QKN5YVDQUO6SLLGMYVVL2QJORLAVCNFSM6AAAAABW35WJYCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMNRUGE3DGMJWGI>
yihozhang
left a comment
(egraphs-good/egglog#519)
<#519 (comment)>
something like this for the action of a group on a set
Yeah egglog supports multiple sorts. There are also many examples in the web demo.
(datatype*
(G
(id)
(inv G)
(plus G G))
(A
(action G A)))
in general, there is no way to turn an arbitrary semi-decision procedure for ground equality in universal algebra into a semi-decision procedure for non-ground equality
I never thought of it! This sounds interesting. Yes EqSat can semi-decide the ground word problem but I kinda just take the full word problem for granted. Let me know if you make any new discoveries about the connection between EqSat and the full word problem.
—
Reply to this email directly, view it on GitHub <#519 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA2QKN5YVDQUO6SLLGMYVVL2QJORLAVCNFSM6AAAAABW35WJYCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMNRUGE3DGMJWGI>.
You are receiving this because you authored the thread.
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hi all, I've been experimenting with encoding equational theories in the sense of universal algebra into Egglog. For example, group theory. I understand that I could enter a complete set of re-write rules as discovered by Knuth-Bendix completion but I wanted to see what would happen if I just use the usual 3 equation encoding:
I understand why the erroneous rule is flagged - its right hand side refers to the variable a that is not bound on the left, and the crash is on a kind of rule that is usually disallowed (variable -> non-variable). Here is the message:
I'm wondering - can Egglog be used to semi-decide ground equality of arbitrary equational theories, such as group theory? This paper: https://arxiv.org/pdf/2501.02413 makes it seem like the answer is 'yes' and so I'm trying to figure out how to do, and wondering if the above approach is correct or if there are other approaches.
The text was updated successfully, but these errors were encountered: