AngouriMath

Symbolics for .NET


Table of contents

AngouriMath

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

PredicateEntailment

← Back to list of classes

Description

Summary

Whether one predicate being true forces another to be true, decided structurally and
only where it can be proven.

Remarks

Written for Piecewise, which takes its first matching case and can
therefore drop any case whose predicate entails an earlier one: wherever the later
predicate holds the earlier one holds too, so the earlier case is taken and the later is
unreachable. That rule was already applied for predicates that are equal; this is
the same rule with a wider notion of "already covered".
One-directional and deliberately incomplete. Entailment between arbitrary predicates
is not decidable, so the only answers here are "proven" and "not proven", and the second is
answered false. A false negative costs a case that could have been
dropped, which is a longer answer; a false positive would delete a reachable case, which is
a wrong one. Everything below is therefore a sufficient condition, never a heuristic.
Three-valued logic does not complicate it. A case is *taken* only when its predicate
is true, so the only thing that has to hold is that a true antecedent forces a true
consequent. What either predicate does when it is NaN — over a non-real argument, say
— never arises, because a case with a NaN predicate is not taken either way.
 Part of question I.3 of
#1212, where
distributing a binder over a piecewise produces one case per subset of the conditions and
most of them are unreachable.

Members

























Angouri © 2019-2023 · Project's repo · Site's repo · Octicons · Transparency · 4378 pages online