fix: Make unification logic less strict

[croyzor]

The Plus constraint has up till now been too strict in extension unification. So far we have been deriving things like the following:

a := Plus("C", b)
a := {"A", "B", "C"}
implies
b := {"A", "B"}

(as in minus_test, which this PR removes)
However, plus should be meant as the union of the the singleton set that it specifies with the extension set of another metavariable. Hence in the above example the solution for b could be either {"A", "B"} or {"A", "B", "C"}.

This means that if we have chains of circuit operations which all add the "quantum" resource, they can all be represented as Plus constraints

[croyzor]

Potential improvement: we could assert that if the node is a Lift node, then it generates a "greater than" Plus constraint and otherwise generates a "greater than or equal" Plus constraint. What do you think, @acl-cqc ?

[acl-cqc]

As it stands, this PR isn't doing anything - you are removing a test OK, but what about adding one of something that you couldn't verify before?? I see #539 but is that test passing already??

Potential improvement: we could assert that if the node is a Lift node, then it generates a "greater than" Plus constraint and otherwise generates a "greater than or equal" Plus constraint. What do you think, @acl-cqc ?

Good question. ISTR this relates to the issues Alex Rice had with resource inference in Tierkreis too. I can see a few possibilities.

• As you suggest, keep lift nodes generating an input-does-not-contain constraint. I think this might be a useful thing to do - if nothing need be added, we don't need a lift node. Where else do we generate "greater than" Plus constraints atm, and should those be "strictly equal"?

  • This may lead to problems with substitution of variables - i.e. lift nodes disappear when graphs are moved into new contexts (perhaps this will only happen during Tierkreis execution and we won't see it yet?). If so, it might help to specify that every Input node has empty extensions; the containing DFG node then takes a (non-disjoint, greater-than-or-equal) union of its inputs with the delta of the containing graph. (This might be a good idea anyway).

• Drop Lift nodes. What if we just say, the input extensions of every node must be exactly equal to the union of the output extensions of every predecessor.

[croyzor]

As it stands, this PR isn't doing anything - you are removing a test OK, but what about adding one of something that you couldn't verify before?? I see #539 but is that test passing already??

#539 was passing on main by mistake - the PR now shows that the test is failing on main, and that same commit has been added to this branch (and the test now passes.)

As you suggest, keep lift nodes generating an input-does-not-contain constraint. I think this might be a useful thing to do - if nothing need be added, we don't need a lift node. Where else do we generate "greater than" Plus constraints atm, and should those be "strictly equal"?

Before this PR we only generated "strictly greater than" constraints, and following this PR we never generate such constraints.

This may lead to problems with substitution of variables - i.e. lift nodes disappear when graphs are moved into new contexts (perhaps this will only happen during Tierkreis execution and we won't see it yet?). If so, it might help to specify that every Input node has empty extensions; the containing DFG node then takes a (non-disjoint, greater-than-or-equal) union of its inputs with the delta of the containing graph. (This might be a good idea anyway).

Hmm, good point about recontextualising graphs, but i think we can just ignore lift nodes in that context and run inference to re-add them where necessary (once we're adding lift nodes automatically)

Drop Lift nodes. What if we just say, the input extensions of every node must be exactly equal to the union of the output extensions of every predecessor.

This is an option, but definitely one for another PR...

[acl-cqc]

Either just add So, do nothing. to make it clear this if here is just to scope the comment; Or, comment out the else if as well. Of course that'll then become noncompiling and soon break, so if you go that way, might be better to translate it from rust to english ;)

[acl-cqc]

It might be nicer still to use meta and other_meta instead of m0 and m1 (whichever way around it is)

[acl-cqc]

Right - so without the fix, this line would break, yes?

[acl-cqc]

In which case LGTM ;-)

[croyzor]

Exactly!

[acl-cqc]

Ok, makes sense now, ta. I'm leaning towards not keeping a "disjoint union" constraint for lift because if we use that, then substitution of context could mean requiring removal of lift nodes, whereas with only the one kind of union, removal of lift nodes is always an optimization, never required. (And removal of nodes during infer_and_validate feels like a rather big thing to be sneaking in behind the user's back. Inserting them might be even bigger, I suppose....)

That said, I'm still holding out hope that this moves us towards eventual removal of the lift node type altogether, but indeed, not for this PR!

[acl-cqc]

How about something like

let mid_nodes = [A,A,B,B,A,B].map(|ext| mknode(&mut hugr, root, df_sig.clone(), ext)).collect::<Result<Vec<Node>,_>>()?;
let nodes = [[input], mid_nodes, [output]].concat()

(there is a collect that turns iterator of Result<T,...> into Result<Vec,...>)

[acl-cqc]

You could even define mknode as a closure |ext| {...} after you've done let hugr = and let df_sig= and then it'd be just .map(mknode).collect....