RewritingSystem

struct RewritingSystem<Term> : Sendable where Term : RewritingTerm

A set of rewriting rules describing some equational equivalences.

Show on GitHub

  • The identifier of a rule in a rewriting system.

    Declaration

    Swift

    typealias RuleID = Int
    Show on GitHub

  • The rules in the system, including those that may have been simplified.

    Declaration

    Swift

    private(set) var rules: [RewritingRule<Term>] { get }
    Show on GitHub

  • A map from terms to the rule of which they are the left-hand side.

    Declaration

    Swift

    private var termToRule: Trie<Term, RuleID>
    Show on GitHub

  • Creates an empty system.

    Declaration

    Swift

    init()
    Show on GitHub

  • Rewrites u with the rules in self until a normal form is reached.

    The rewriting process is notionally nondeterministic unless self is confluent.

    Declaration

    Swift

    func reduce(_ u: Term) -> Term
    Show on GitHub

  • Inserts the given rule using compareOrder to order pairs of terms.

    A rule u => v is notionally contained in a rewriting system if that system contains a set of rules capable of rewriting u to v. This set may not contain u => v itself.

    The return value is (true, new) if r is not already notionally contained in the system, where new is the identifier of a newly inserted rule that is encoding r. Otherwise, the return value is (false, old) where old is the identifier of a rule encoding r.

    Precondition

    The source of the rule is ordered after its target.

    Declaration

    Swift

    @discardableResult
mutating func insert(
  _ r: RewritingRule<Term>,
  orderingTermsWith compareOrder: (Term, Term) -> StrictOrdering
) -> (inserted: Bool, ruleAfterInsertion: RuleID)
    Show on GitHub

  • Turns self into a terminating and confluent rewriting system, using compareOrder to order pairs of terms.

    This method uses Knuth-Bendix completion algorithm to transform self into a terminating confluent system. The completion procedure is semi-decidable: it returns true if it succeeds or false if it suspects that it won’t terminate.

    Declaration

    Swift

    mutating func complete(orderingTermsWith compareOrder: (Term, Term) -> StrictOrdering) -> Bool
    Show on GitHub

  • Calls action on each overlap between two rules of the system.

    Declaration

    Swift

    private func forEachOverlap(do action: (RuleID, RuleID, Term.Index) -> Void)
    Show on GitHub

  • Calls action on each overlap involving i.

    Declaration

    Swift

    private func forEachOverlap(involving i: RuleID, do action: (RuleID, Term.Index) -> Void)
    Show on GitHub

  • Calls action on each identifier in terms denoting a rule having an overlap between its left-hand side and suffix.

    If the key/value pair (t, i) is contained in terms, then t is the suffix of some term l and i identifies a rewriting rule l => r.

    Declaration

    Swift

    private func forEachOverlap(
  of suffix: Term.SubSequence, in terms: SubTrie<Term, RuleID>,
  do action: (RuleID) -> Void
)
    Show on GitHub

  • Returns the critical pair formed by the rules lhs and rhs, which overlap at the i-th position of lhs‘s source.

    Declaration

    Swift

    private func formCriticalPair(
  _ lhs: RuleID, _ rhs: RuleID, overlappingAt i: Int
) -> CriticalPair
    Show on GitHub

  • Adds a rule rewritng p‘s first element to its second, or vice versa, using compareOrder to order pairs of terms.

    Declaration

    Swift

    private func resolveCriticalPair(
  _ p: CriticalPair,
  orderingTermsWith compareOrder: (Term, Term) -> StrictOrdering
) -> RewritingRule<Term>?
    Show on GitHub

  • Removes the rules in self whose left hand side can be reduced by a simpler rule.

    Declaration

    Swift

    private mutating func leftSimplify()
    Show on GitHub

  • Removes i from self if the suffix of its left-hand side starting from p contains a subterm that can be reduced by another rule.

    Declaration

    Swift

    private mutating func simplify(_ i: RuleID, lookingForTermsInSuffixFrom p: Term.Index) -> Bool
    Show on GitHub

  • The rewritings of a term by two different rules or the same rule at two different positions.

    See more

    Declaration

    Swift

    private struct CriticalPair : Sendable
    Show on GitHub

  • The identifier of an overlap between rewriting rules.

    See more

    Declaration

    Swift

    private struct OverlapIdentifier : Hashable, Sendable
    Show on GitHub