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

← Back to list of members

Binder​(System.​String,​AngouriMath.​Core.​Transformations.​Matching.​MatchPattern)

 Method (no overloads)

Summary

Matches a binder — a node that declares a name and puts a body under it — binding the
declared name to varName and matching the body against
body. Repeating varName inside
body is how a rule says the same variable.

Remarks

{ x : x in S } is S, and the switch said so by deconstructing
ConditionalSet(var v, Inf(var v, var s)) — reading the node's stored parts. A pattern could not: the matcher walked DirectChildren, and a set builder
publishes one child there, its predicate, with the bound name already replaced by a
placeholder invented per traversal. So a two-child pattern over it never matched, and
no pattern could name the bound variable at all.
#1074One node type needs this, not six. The issue expected every binder to be in the
same position; measuring them says otherwise. A summation, a product, an integral, a
derivative, a limit and a lambda each publish the name they bind as an ordinary child,
un-renamed, so an ordinary Node``1(AngouriMath.Core.Transformations.Matching.MatchPattern[]) already reaches it —
Summationf offers four children and the second is the index. Only
ConditionalSet hides and renames, and only it has an
MatchableChildren override.
The name position is a hole, and cannot be anything else. Matching a bound name
against a written one would make the pattern read { x : … } and
{ y : … } as different expressions, which they are not, so this refuses
anything but Any(System.String) there. Alpha-invariance then holds for the same
reason it holds of the switch arm: what is asserted is that two occurrences are
the same name, never which name.
What a rule owes in return. Reading inside a binder means the body arrives with
its bound name written, so a replacement that lifts part of that body out of the
binder frees an occurrence that was bound — capture, in reverse. Nothing here can check
that, because the replacement is arbitrary. { x : x in S } is safe because
S is a sibling of the bound occurrence rather than under it; a rule taking out
something that mentions varName would not be.

























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