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

ProvesEqual(AngouriMath.Entity,AngouriMath.Entity,System.Collections.Generic.IReadOnlyList{AngouriMath.Core.Transformations.Matching.MatchedRule},AngouriMath.Core.Budgets.WorkBudget)

Method (no overloads)

Summary

Whether rules prove left and
right equal, within budget. A
false means not proved, never unequal.

Remarks

This is the reliable half, and canonicalising is not. Bringing two expressions
separately to a canonical form and comparing the results only decides equality where
the rules are confluent: otherwise one side can reach a form the other cannot,
and two equal expressions end in different forms having each been canonicalised
correctly. Measured, on (x + y) * (x - y) against x ^ 2 - y ^ 2: the
product's graph reaches the difference of squares, the difference of squares' graph
does not reach the product, and the two forms are the same size — so each canonicalises
to itself.
Asking in one graph has no such gap. Both expressions are inserted, every equality the
rules reach from either is merged, and the question is whether they ended in one
class — which does not depend on the rules being confluent, only on their reaching far
enough within the budget.

AngouriMath

Table of contents

AngouriMath

ProvesEqual​(AngouriMath.​Entity,​AngouriMath.​Entity,​System.​Collections.​Generic.​IReadOnlyList{AngouriMath.​Core.​Transformations.​Matching.​MatchedRule},​AngouriMath.​Core.​Budgets.​WorkBudget)

ProvesEqual(AngouriMath.Entity,AngouriMath.Entity,System.Collections.Generic.IReadOnlyList{AngouriMath.Core.Transformations.Matching.MatchedRule},AngouriMath.Core.Budgets.WorkBudget)