AngouriMath

Navigation

Home Quick start Wiki Almanac Research What's new Try Use Angouri.org GitHub Report a bug ~~Donate~~ Contacts

← Back to list of members

Reversed

Property

Summary

This rule read the other way, or null where it has no such reading.

Remarks

The two sides swap and nothing else does. The side condition is carried over
unchanged, because it is a predicate on the bindings and both directions produce the
same bindings; and Soundness is carried over unchanged, because what a
rewrite rule claims is an equality and an equality is symmetric.
What does not carry over is termination. A rule that collects becomes one that
expands, so a reversed rule composed with the rule it came from does not reach a fixed
point — k*p + k*q and k*(p + q) rewrite to each other forever. A reversed
set is a thing to ask questions of, not one to run to stability.

AngouriMath

Table of contents

AngouriMath

Reversed