Support and testing for equality-atom and if-then-else based RDDL-style boolean interoperability

[mejrpete]

Note that this PR is submitted as a draft, since the true PR should probably be opened against a separate feature branch, rather than devel.

Boolean interop for RDDL requires the ability to move from Term -> Formula and from Formula -> Term within the AST built in Tarski as discussed in #91. In general, we need the ability to construct nested formulae which include both logical operations on expressions with atoms based on the numerically-derived Boolean sort, and direct mathematical operations on these items.

To accomplish this in practice, two patterns can be used.

1) Term -> Formula:

Given a Term with sort Boolean, we can use the typical equality predicate and a constant True/1 value to wrap to a Formula (for a language which has both the Boolean and Equality theories attached)

a = lang.function('a', lang.Boolean)
b = lang.function('b', lang.Boolean)
bool_t = lang.constant(1, lang.Boolean)
logical_formula = (a == bool_t) | (b == bool_t)

2) Formula -> Term:

Given a Formula, we can wrap out to a Term with sort Boolean using the IfThenElse term, and corresponding boolean constants.

a = lang.function('a', lang.Boolean)
b = lang.function('b', lang.Boolean)
bool_t = lang.constant(1, lang.Boolean)
logical_formula = (a == bool_t) | (b == bool_t)
math_included = ite(logical_formula, bool_t, lang.constant(0, lang.Boolean)) + 1 

With these two patterns, we can arbitrarily move back and forth between Formula and Term objects depending on the operations needed when building the AST in Tarski. Additionally, because these patterns are easily identifiable with simple pattern matching, when performing write-side IO for an RDDL domain which includes these wrappers within the Tarski representation, we can remove the wrappers accordingly, and generate legal RDDL which does not include the additional representational overhead involved with the wrapper patterns discussed above.

The Tarski modeling approach for RDDL using these patterns involves representing Boolean RDDL values as Boolean (sort) codomain functions, with equality-based atoms as the basic logical type (e.g. (a == lang.constant(1, lang.Boolean)). This is in contrast to the approach explored in the rddl-support branch (#96), which assumed the use of Predicate for representation of Boolean RDDL values. One additional advantage of this change is that while the closed-world assumption prohibits the declaration of false-valued non-fluents and initial-state state-fluents (necessary in RDDL, since Boolean valued fluents can be declared with default values of true) in an implementation based on Predicate representations for these fluents (as in #96), the use of Boolean codomain functions in this alternate approach trivially avoids this issue.

Included changes/additions:

1. Incorporating a Boolean sort descended from Natural when the Boolean theory is attached to a FirstOrderLanguage
2. Addition of Bernoulli as a builtin for the Random theory
3. Implementation additions in RDDL write IO in order to "unwrap" the two major patterns used to translate back and forth between Formula and Term items when using the Boolean sort as described.
4. Minor changes to write true and false literals rather than 0/1 when writing RDDL from our representation (needed as far as I know for appropriate behavior with both the PROST and rddlsim RDDL parsers)
5. Test additions & modifications to test RDDL write-side IO support, along with tests for the Boolean theory changes

Omissions/Necessary future discussion

1. Current tests are focused on write-side RDDL IO. Neither the read-side tests, nor the read-side RDDL IO code has been modified to automatically wrap back and forth using the two patterns above.
2. From a user perspective (when using Tarski as a tool to directly construct the AST and domain/instance models for RDDL-specified problems) requiring the explicit use of these wrappers puts significant onus on the user to understand the distinction between Formula and Term within Tarski in order to appropriately use these wrappers and correctly construct their domain/instance. While this is potentially workable, it would be preferable from the user's perspective to have some level of "automatic" injection of wrappers in instances where there is a mismatch between input to an operator and the expected object type (e.g. when dispatching a lor called from a Formula where the argument is a Term with sort Boolean). This would involve building recovery logic with knowledge of the Boolean sort into Tarski's operator dispatching implementation, which may or may not be acceptable from a design standpoint. This may be a worthwhile point of discussion!

[miquelramirez]

Hi @mejrpete,

1. Current tests are focused on write-side RDDL IO. Neither the read-side tests, nor the read-side RDDL IO code has been modified to automatically wrap back and forth using the two patterns above.

That is okay, will check, but the problem is that I don't really have very strong "constraints" on this. Basically because I haven't any planners using the RDDL -> AST features.

2. From a user perspective (when using Tarski as a tool to directly construct the AST and domain/instance models for RDDL-specified problems) requiring the explicit use of these wrappers puts significant onus on the user to understand the distinction between Formula and Term within Tarski in order to appropriately use these wrappers and correctly construct their domain/instance. While this is potentially workable, it would be preferable from the user's perspective to have some level of "automatic" injection of wrappers in instances where there is a mismatch between input to an operator and the expected object type (e.g. when dispatching a lor called from a Formula where the argument is a Term with sort Boolean). This would involve building recovery logic with knowledge of the Boolean sort into Tarski's operator dispatching implementation, which may or may not be acceptable from a design standpoint. This may be a worthwhile point of discussion!

The "significant onus on the user" is a bit fuzzy for me, I need to see specific examples where this becomes an issue.

Python being Python (and not C++) it is not clear to me what degree of "automation" is possible, analogous to what would be the approach in C++ (e.g. generic programming, traits, concepts, etc.) to essentially implement what is code generation. Overloading operators in Python was a massive pain in the bum and the best we could come up with were the frankly, quite bothersome, concept of TermReference to wrap terms so we could use them in standard containers.

If you could come with a concrete example that illustrates this issue - on a gist perhaps - I would appreciate it.

Regards,

Miquel.

[miquelramirez]

I have been thinking a bit about the issues regarding modelling support @mejrpete you mentioned earlier.

Thinking a bit about it I see the following as possible "helpers":

1. Add literal or lt global function

This would be a global function much like symref is, and with a similar purpose. The function would be something along the lines of:

def lt(t: CompoundTerm, v: Constant) -> Atom:
    if t.symbol.builtin: 
        raise SyntaxError("Cannot define literals for built-in symbol: {}".format(str(t.symbol)))
    return t == v

So one could write:

condition = land( lt(f(a), 1), lt(g(b), 1)) # f(a) = 1 /\ g(b) = 1
condition2  = lor( lt(f(a), 0), lt(g(c), 1)) # f(a) = 0 -> g(c) = 1

2. Overload operators of CompoundTerm

This would require to overwrite a binary operator like @ for CompoundTerm, encapsulating the same as the proposed function lt above. Then we would end up with something like:

condition = land( f(a)@1, g(b)@1) # for  f(a) = 1 /\ g(b) = 1
condition2  = lor( f(a)@0, g(c)@1) # for f(a) = 0 -> g(c) = 1

What do you think? any other ideas?