Discussion: Definedness analysis in rewrite rules and equations

[jberthold]

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.

[ana-pantilie]

syntax Int ::= f(Int) [function] | g(Int) [function]

rule f(g(X)) => X +Int X

Error: illegal function symbol g on the LHS; consider it a simplification rule if that's what you wanted

---

syntax A ::= f(Map) [function] | blabla

rule f(K |-> V M:Map) => blabla

Question: is (K |-> V M) defined? if it's undefined, then the rule above is unsound (writing Bottom to something non-Bottom)

    rule f(K |-> V K |-> V) => blabla

<=> rule #Bottom => blabla