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

QuantifierFacts

← Back to list of classes

Description

Summary

What the quantifiers around a statement establish while they decide it: each bound name
is a member of the set it ranges over, and a claim made under a hypothesis is made where
the hypothesis holds. A rule that needs one of those facts, such as that p is prime
or that 0 < k < p, asks here.

Remarks

A node has no parent, so a rule inside a body cannot walk up to the quantifier that binds
its names. The quantifier hands the facts down instead, for as long as it takes to decide:
the set its name ranges over, and for forall x in S : H implies C -- or
C or not H, which says the same -- the conjuncts of H while C is
simplified. They are never in scope while H itself is simplified, or
H implies C would lose its hypothesis. For exists and
exists! each conjunct of the body is simplified with the ones before it in scope.
Scopes nest, so the inner quantifier of forall p in PP : forall k in ZZ : ... knows
that p is prime. Nothing leaves a scope: a verdict reached with the facts is the
verdict on the quantified statement, which states them, and it carries no condition.
 The bound name is renamed first, to a name no other expression has, and every fact is
about a renamed name. That is what keeps a verdict from escaping through a cache. A node
that caches its simplification can only have read a fact if it mentions a renamed name,
and every such node is built during this decision and is reachable from nothing else. A
cache keyed on the structure of an expression cannot serve it elsewhere either, since no
other expression has the name. For the same reason a conjunct of the hypothesis about the
free names alone is not recorded: a rule reading it could simplify a node that is shared.
A substitution stops at a binder, so an inner quantifier that binds the same name again
is not renamed through, and the outer facts about the name do not reach it.
 Only a body in which a rule reads the facts is renamed and decided this way. Every other
statement is decided as it was, under its own names.
 https://github.com/asc-community/AngouriMath/issues/1409

Members

























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