Support unary predicates in cat

[xeren]

This PR affects the intermediate representation for memory models, such that Relation can model sets as well. This relates to issues #535 and #371.

Features:

• The cat parser accepts domain(r) and range(r) without brackets.
• The builtin New constructs a free set.
• The empty r axiom allows a set as operand.

API changes:

• Add Relation.isUnaryRelation() and Relation.isBinaryRelation().
• Add unary and binary type checks to constructors of Constraint.
• Add Wmm.newRelation(boolean) and Wmm.newRelation(String,boolean).
• Replace DomainIdentity and RangeIdentity with Domain and Range.
• Remodel SetIdentity as non-static.
• Add TagSet as its bottom-level replacement for static SetIdentity.
• RelationAnalysis also learns Knowledge for unary relations, stored as identity graphs.

CAAT changes:

• Replace ProjectionIdentityGraph with ProjectionSet.
• Add n-ary IntersectionSet and UnionSet.
• Remove guarantee that SetPredicate only depends on SetPredicate.
• Add AbstractWMMSet, DynamicDefaultWMMSet and MaterializedWMMSet.
• Build instances of SetPredicate for unary relations in ExecutionGraph.

Additional:

• Fix a bug in caat where Element.derivLength was not updated.

[hernanponcedeleon]

I haven't checked the code in detail, but something I am not a big fan of is the "abuse" of the term relation even for unary predicates. I know that in some domains (e.g., mathematics) relations can be also unary, but I think the terms "relation" and "set" are much more common in the domain of WMMs.

One possibility would be to use set/relation/predicate for the unary/binary/general cases, but this will probably require changes all over the place.

[ThomasHaas]

I haven't checked the code in detail, but something I am not a big fan of is the "abuse" of the term relation even for unary predicates. I know that in some domains (e.g., mathematics) relations can be also unary, but I think the terms "relation" and "set" are much more common in the domain of WMMs.

One possibility would be to use set/relation/predicate for the unary/binary/general cases, but this will probably require changes all over the place.

The problem is that you would need two classes, one to represent sets, and one to represent relations.
The easiest (and probably best) solution is to use a single class with an arity parameter like René does.

[hernanponcedeleon]

The problem is that you would need two classes, one to represent sets, and one to represent relations. The easiest (and probably best) solution is to use a single class with an arity parameter like René does.

I do not see why that would contradict my proposal. That class could be called Predicate and then methods like isUnaryRelation() and isBinaryRelation() could be renamed to isSet() and isRelation() to match the common terms used in WMMs

[ThomasHaas]

If you mean it like that, then sure.

[ThomasHaas]

Why is this change necessary?

[xeren]

I encountered Already bound name W, and others like ext and figured that I probably should check the global namespace as well when computing unique names. A better way would be to add relations to the local namespace on every occasion.

[ThomasHaas]

I think the only case where relations are "secretely" generated (i.e. outside of the parser) is when invoking wmm.getPredefinedRelation (or whatever it is called). This one is a little annoying. I think for binary relations, we just opted to never generate named subrelations (except for the hidden one's like idd) so that there was never a name conflict.
I guess if you do the same with tag sets generated there, it would should work correctly. At least I don't see why the code that worked for binary relations shouldn't just work out-of-the-box for unary relations anymore.

[xeren]

Another Already bound name F occurred, because in opencl.cat, dynamic_tag(X) is defined before F is declared, which is used in that function. dynamic_tag is called twice, so the namespace lookup misses twice, leading to a redefinition of F.
Maybe createUniqueName should always check wmm, rather than namespace, to not be sensitive to local scopes and to guarantee uniqueness in wmm.

[ThomasHaas]

I cannot really follow. You removed the update of the namespace in visitExprBasic and that is why you create relations without registering their names in the namespace. If you do this correctly, and assuming that wmm.getOrCreatePredefinedRelation(k) does not create named subrelations for tag set, I think it should work just fine.
What breaks if you use the original 1-line code but replace the Filter.byTag(k) with addDefinition(new TagSet(wmm.newSet(k), k))?

[xeren]

What breaks if you use the original 1-line code but replace the Filter.byTag(k) with addDefinition(new TagSet(wmm.newSet(k), k))?

There are two loosely-dependent namespace systems at work here: Wmm.getRelation(String) and VisitorCat.namespace. During parsing, I get collisions in Wmm.addAlias(String,Relation), because the previous call to VisitorCat.createUniqueName(String) only checks the other namespace system.

Previously we used Wmm.addFilter(Filter) to bind a name to a set. That is a third namespace system and it does not check for name collisions. Now that sets and relations have merged, these collisions are detected. This also happens with the oneliner.

You removed the update of the namespace in visitExprBasic and that is why you create relations without registering their names in the namespace.

I removed the update in visitExprBasic, because I added an additional lookup with wmm.getRelation(name). With this, binding the name in the local namespace became obsolete. let instructions still modify that namespace.

[ThomasHaas]

I want to understand how collisions even happen. I understand that there are two namespaces (the parser and the wmm), but from my understanding every name in the Wmm should also appear in the parser's namespace if visitExprBasic and visitLetExpr register all names they encounter, no? The only exception I can think of is if wmm.getOrCreatePredefinedRelation(k) creates named subrelations which then appear in the wmm's namespace but not in the parser's.

Either way, my main concern was that something might go wrong if the parser's namespace is not aligned with the wmm's namespace, especially when functions that capture only the parser's namespace are involved. But after thinking about it for a little bit, I don't think anything breaks there.

[ThomasHaas]

I do not see why that would contradict my proposal. That class could be called Predicate and then methods like isUnaryRelation() and isBinaryRelation() could be renamed to isSet() and isRelation() to match the common terms used in WMMs

A quite annoying problem is that the Predicate<T> class exists in the java standard namespace.
That is why I used the name CAATPredicate in CAAT to avoid name clashes.
That being said, we also use Thread and Function although they clash with existing java classes (which is annoying sometimes).

[xeren]

I know that in some domains (e.g., mathematics) relations can be also unary, but I think the terms "relation" and "set" are much more common in the domain of WMMs.

I do not see why that would contradict my proposal. That class could be called Predicate and then methods like isUnaryRelation() and isBinaryRelation() could be renamed to isSet() and isRelation() to match the common terms used in WMMs

With currently 569 usages of Relation in development, that will cause a lot of conflicts. I'd rather do the renaming in another PR. I can rename isSet() and isRelation() immediately, though.

A quite annoying problem is that the Predicate<T> class exists in the java standard namespace.
That is why I used the name CAATPredicate in CAAT to avoid name clashes.

Then I throw WmmPredicate and EventPredicate into the ring. The first would be a double naming, as the package already says wmm.

[ThomasHaas]

Then I throw WmmPredicate and EventPredicate into the ring. The first would be a double naming, as the package already says wmm.

I prefer the first. Such "double naming" is never an issue IMO.

EDIT: Also, I agree about delaying the renaming to another PR.

[hernanponcedeleon]

Sorry it took me forever to come back to this PR.

I left a few more comments

[hernanponcedeleon]

LGTM.

Unless @ThomasHaas has further comments, we can merge

[ThomasHaas]

LGTM