Eager Term Rewriting For The Fracterm Calculus Of Common Meadows

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 tha...

Full description

Saved in:
Bibliographic Details
Published in:Computer journal 2024-06, Vol.67 (5), p.1866-1871
Main Authors: Bergstra, Jan A, Tucker, John V
Format: Article
Language:English
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0010-4620
1460-2067
DOI:10.1093/comjnl/bxad106