Outsource Properties to a new package

[mforets]

Idea: outsource Reachability/src/Properties to an independent package MathematicalPredicates.jl.

Pros and ideas for extension:

• add "syntactic sugar": convenience macros to express conjunctions or disjunctions with sets
• add methods for simplification of predicates
• redefine the methods using the abstract MathematicalSets.jl interface
• definition of safety problems independently of Reachability.jl
• MathematicalPredicates.jl are interesting on its own

Cons:

• it is currently a rather small module
• the code needs to be generalized, eg. not depend on LazySets

[schillic]

Could it be just Predicates.jl? This already sounds quite mathematical.

After thinking about this a bit, it is generally good to keep packages small.

Here are some more arguments in the other direction:

• The proposed methods could also be added now, so they are not really advantages.
• If we want to make use of changes in MathematicalPredicates.jl, we need to wait until a new version is released (the same issue we have with LazySets already). In this case that is not a show-stopper because I expect the package to be rather robust with only occasional changes.

[mforets]

Could it be just Predicates.jl? This already sounds quite mathematical.

It is just in line with our MathematicalXYZ series :smile: And it sounds more specific to our application than "Predicates".

[schillic]

It is just in line with our MathematicalXYZ series

Indeed, so typing using Math<TAB> in the REPL is not enough :frowning_face:

And it sounds more specific to our application than "Predicates".

I think in a programming context a predicate is well understood. I prefer a 13-character name over a 25-character name if possible.

[mforets]

Specificity has its drawbacks, i agree, and a reason that there's plenty of discussion over Discourse about naming conventions in Julia.. IMO MathematicalPredicates goes in line with the specificity criterion in the same sense to prefer MathematicalSets over just Sets or MathematicalSystems over Systems. About the name completion for quick REPL usage, you can always define a new alias in the startup.jl file, if that is an option.

[mforets]

I had a look at packages with related keywords and this is what came up:

• https://github.com/roberthoenig/FirstOrderLogic.jl
• https://github.com/JuliaGeometry/GeometricalPredicates.jl
• https://github.com/lairez/ExactPredicates.jl
• https://pkg.julialang.org/docs/ImplicitEquations/TUSCW/0.6.0/autodocs/#ImplicitEquations.Preds

[schillic]

The main problem I see with the current architecture is that a predicate has exactly one argument, and moreover in a conjunction/disjunction all conjuncts/disjuncts share this argument. In general you want to be able to specify a property such as:

@predicate x, y -> pred1(y, x) ∧ (pred2() ∨ ¬pred3(y) ∨ pred2()))

My suggestion is to make a predicate parametric in the number of arguments. In particular, a conjunction (and analogously a disjunction) P would be defined as a list of pairs (c, indices) where c is a predicate (a conjunct) that expects k arguments and indices is a list of k indices to know which arguments of P should be passed to c (and in which order). In the example above, we would have:

P: Conjunction{2}([(c1, [2, 1]), (c2, [2])])
c1: Atom{2}
c2: Disjunction{1}([(c3, []), (c4, [1]), (c5, [])])
c3: Atom{0}
c4: Negation{1}(c6)
c5: Atom{0}
c6: Atom{1}

Then check(P, [x, y]) (or however we want to call the evaluation method) would be doing check(c1, [y, x]) && check(c2, [y]) and check(c2, [y]) itself would be doing check(c3, []) || check(c4, [y, x]) || check(c5, [y]), and so on. (The && would of course be replaced by a loop because there can be an arbitrary number of conjuncts.) An Atom{k} would have a Function that takes k arguments.

This is all relatively simple apart from the @predicate, which is however only for convenience and not required for this to work.

Things become tricky if we want to support check(P, x, y) instead of check(P, [x, y]). I do not see how to interpret the indices lists in this case. We would also have to create these check methods with the correct number of arguments programmatically.

---

Note that pred2 occurs twice in my example, but I did not make use of this. In principle I suggest that we require that the predicates have no side effects or that there is an option to specify this. This allows the library to do optimizations (such as ignoring the second call to pred2 or changing the order of conjunctions for evaluation). I do not plan to make use of that, but maybe this is useful for somebody else.