Discussion: Definedness analysis in rewrite rules and equations

While discussing "argument predicates" for function rules, some questions about definedness in rule/equation side conditions came up.
This issue persists aspects of this discussion for posterity and further development.

• Possibly one should check, in this order:
  • assuming the LHS term is defined, are the requires guaranteed to be defined?
  • assuming LHS term and requires are defined, is the RHS guaranteed to be defined?
• if only total functions and constructors (total) are used in a term, it is safe to assume that the term is defined (safe approximation).
  • If, for example, a requires clause ends up containing a division by zero: division is not total. We should analyse requires clauses for the functions used.
• Currently, hs-backend-booster tries to perform a safe approximation of whether a rule preserves definedness.
  • The RHS term is checked to not contain partial functions.
  • But what about RHS predicates and LHS predicates?
    • This is not a problem for rewriting in booster at the moment, as no rule gets applied unless they are all true anyway (NB that the RHS predicates are checked, too, to prune invalid states).
    • once terms are simplified inside side conditions, definedness of side conditions needs to be ensured.
      • i.e., side conditions have to be checked like the RHS term is (symbols can occur inside \equals and \in predicates)
      • Simplifications whose predicates do not preserve definedness have to be discarded.
      • If a function rule has predicates which do not ensure definedness, no rules of the same and lower priorities can be safely applied.

Start with hs-backend-booster's current safe approximation of definedness for rewrite rules, then trace how RHS terms, LHS predicates, RHS predicates, and requires clauses are checked. The issue does not name files or tests; done would require a settled design for definedness analysis across side conditions and simplifications.