AngouriMath
SubsumesCore(AngouriMath.Core.Transformations.Matching.MatchPattern,System.Collections.Generic.Dictionary{System.String,AngouriMath.Core.Transformations.Matching.MatchPattern})
Method (no overloads)
Summary
A node pattern pins the node type and the arity, so it subsumes only another node
pattern of that type and arity whose children it subsumes in turn — under one
assignment, so that a hole repeated across children has to be assigned the same
subpattern in each.
pattern of that type and arity whose children it subsumes in turn — under one
assignment, so that a hole repeated across children has to be assigned the same
subpattern in each.
Remarks
Commutativity is a claim about this side. A commutative pattern matches a
node in either order, so subsuming needs only one of the two pairings to
work; a non-commutative one gets the written pairing and nothing else. When the
pattern being subsumed is the commutative one, it matches both orders, so this must
cover both — and a non-commutative pattern covers both only when its two children
are interchangeable, which the written pairing already decides. The assignment is
copied before each attempt, because a pairing that fails half way must not leave
its bindings behind for the other one.
node in either order, so subsuming needs only one of the two pairings to
work; a non-commutative one gets the written pairing and nothing else. When the
pattern being subsumed is the commutative one, it matches both orders, so this must
cover both — and a non-commutative pattern covers both only when its two children
are interchangeable, which the written pairing already decides. The assignment is
copied before each attempt, because a pairing that fails half way must not leave
its bindings behind for the other one.
Angouri © 2019-2023 · Project's repo · Site's repo · Octicons · Transparency · 4378 pages online