Predicates and Formulas as Boolean functions

[JoD]

In many ways, Predicates, Formulas and Connectives behave as Boolean functions, mapping variables to the Boolean type {True, False}. By allowing predicates and functions to be used as terms, we support this notion, and provide a richer language to the programmer.

In a first step, we implement this functionality as syntactic sugar. E.g.: Q(!x:(P(x)) <=> ?y:(y=True<=>!x:P(x))&Q(y). A function toInt(Boolean):int mapping False to 0 and True to 1 should be provided. This way, Boolean typed terms can be used in arithmetic.

In a later stage, predicates can be implemented as a subclass of function, possibly allowing some optimization. Some questions are still open, e.g. how to handle "partial predicates".