4 ms·
> we have consensus It's decidable whether a TRS is confluent, i.e. if a fixpoint exists, exactly one fixpoint exists. Or what do you mean?
by maweki 2y ago
> we have consensus
It's decidable whether a TRS is confluent, i.e. if a fixpoint exists, exactly one fixpoint exists. Or what do you mean?
- almostgotcaught 2y agoi don't know what you're trying to say. i'm saying that "all" the rewrite rules don't matter, only the "interesting" ones matter but interesting is related to opinion/taste/cost.
- maweki 2y agorewriting rules are more like function/predicate definitions in FP or LP and not like axioms. Term rewriting does have its own axioms, like ZFC does. What you're saying is akin to "not all functions are interesting". Well, yes... But that's true for any model of computation.