Eager Term Rewriting For The Fracterm Calculus Of Common Meadows
Jan Aldert Bergstra, John Vivian Tucker · The Computer Journal · 2023
Abstract Eager equality is a novel semantics for equality in the presence of partial operations. We consider term rewriting for eager equality for arithmetic in which division is a partial operator. We use common meadows which are essentially fields that contain an absorptive element $\bot $. The idea is that term rewriting is supposed to be semantics preserving for non-$\bot $ terms only. We show soundness and adequacy results for eager term rewriting w.r.t. the class of all common meadows. However, we show that an eager term rewrite system which is complete for common meadows of rational numbers is not easy to obtain, if it exists at all.