egraphs-good / egglog

egraphs + datalog!
https://egraphs-good.github.io/egglog/
MIT License
458 stars 54 forks source link

Subsumption confusing semantics #462

Open oflatt opened 2 weeks ago

oflatt commented 2 weeks ago

Subsumption currently works kind of like a query and kind of like an action. For example, this code:

(Subsume (Add (Add 2 3) 4))

Adds (Add 2 3) to the database. However, if (Add (Add 2 3) 4) isn't present, it errors out because it couldn't find an existing entry.

Is this the behavior we want? Perhaps we wanted subsumption to first add the tuple, then subsume it?

saulshanabrook commented 1 week ago

I don't have a strong opinion on which semantics is preferable. I do agree maybe it would make sense to add it.

I am curious, is this from just experimenting, or in your use case do you often try to subsume things that don't yet exist?

oflatt commented 1 week ago

I ran into a bug in eggcc that was a result of me misusing subsumption. I actually thought the semantics was to add it

yihozhang commented 1 week ago

I'm actually surprised about this behavior, because delete works fine even if the tuple does not exist, and we rely on this behavior at some places.

(datatype E (A))
(delete (A)) ;; works fine
(subsume (A)) ;; panics

I believe subsume should follow the behavior of delete. As another example, switching the order of the two rules below will cause egglog to panic

(datatype E (A))

(rule () ((A)))
(rule () ((subsume (A))))

(run 1) ;; works fine, but switching causes panic.
saulshanabrook commented 1 week ago

Sounds good to fix it. I would assume it works like delete/set as well.