One final round of small cleanups for Monoids benchmark

Author: slavapestov

benchmark/multi-source/Monoids/Automaton.swift

@@ -82,85 +82,69 @@ extension Automaton {
   }
 }
 
-/// Constructs an automaton to recognize the complement of this regular set:
-///
-///   .*(x1|x2|...).*
-///
-/// where 'words' is [x1, x2, ...].
-///
-/// This is Lemma 2.1.3 in:
-///
-/// String Rewriting Systems, R.V. Book, F. Otto 1993. Springer New York.
-func buildAutomaton(_ words: [Word], _ alphabet: Int) -> Automaton {
-  // Proper prefixes of each word.
-  var prefixes = Set<Word>()
-
-  var result = Automaton()
-
-  func isIrreducible(_ word: Word) -> Bool {
-    for i in 0 ..< word.count {
-      for other in words {
-        if i + other.count <= word.count {
-          if Word(word[i ..< (i + other.count)]) == other {
-            return false
-          }
-        }
-      }
-    }
+extension RewritingSystem {
+  /// Constructs an automaton to recognize the complement of this regular set:
+  ///
+  ///   .*(x1|x2|...).*
+  ///
+  /// where 'words' is [x1, x2, ...].
+  ///
+  /// This is Lemma 2.1.3 in:
+  ///
+  /// String Rewriting Systems, R.V. Book, F. Otto 1993. Springer New York.
+  func buildAutomaton() -> Automaton {
+    // Proper prefixes of each word.
+    var prefixes = Set<Word>()
 
-    return true
-  }
+    var result = Automaton()
 
-  prefixes.insert([])
-  for word in words {
-    for i in 0 ..< word.count {
-      let prefix = Word(word[0 ..< i])
-      prefixes.insert(prefix)
+    func isIrreducible(_ word: Word) -> Bool {
+      return reduceOne(word) == nil
     }
-  }
 
-  result.states = prefixes.sorted { compare($0, $1, order: .shortlex) == .lessThan }
+    prefixes.insert([])
+    for rule in presentation.rules {
+      let word = rule.lhs
+      for i in 0 ..< word.count {
+        let prefix = Word(word[0 ..< i])
+        prefixes.insert(prefix)
+      }
+    }
 
-  for prefix in prefixes {
-    for x in 0 ..< UInt8(alphabet) {
-      let word = prefix + [x]
+    result.states = prefixes.sorted { compare($0, $1, order: .shortlex) == .lessThan }
 
-      if prefixes.contains(word) {
-        result.transitions.append((prefix, x, word))
-        continue
-      }
+    for prefix in prefixes {
+      for x in 0 ..< UInt8(alphabet) {
+        let word = prefix + [x]
 
-      if !isIrreducible(word) {
-        continue
-      }
+        if prefixes.contains(word) {
+          result.transitions.append((prefix, x, word))
+          continue
+        }
 
-      for i in 1 ... word.count {
-        let suffix = Word(word[i...])
+        if !isIrreducible(word) {
+          continue
+        }
+
+        for i in 1 ... word.count {
+          let suffix = Word(word[i...])
 
-        if prefixes.contains(suffix) {
-          result.transitions.append((prefix, x, suffix))
-          break
+          if prefixes.contains(suffix) {
+            result.transitions.append((prefix, x, suffix))
+            break
+          }
         }
       }
     }
-  }
-
-  return result
-}
 
-extension Presentation {
-  /// The Irr(R) automaton.
-  func automaton(alphabet: Int) -> Automaton {
-    return buildAutomaton(rules.map { $0.lhs }, alphabet)
+    return result
   }
 
   /// Returns the number of irreducible words in this monoid presentation, or
   /// nil if this set is infinite.
-  ///
-  /// If the presentation is complete, this is the cardinality of the
-  /// presented monoid. Otherwise, it is an upper bound.
-  func cardinality(alphabet: Int) -> Int? {
-    let automaton = automaton(alphabet: alphabet)
+  var cardinality: Int? {
+    precondition(state == .complete)
+    let automaton = buildAutomaton()
     if automaton.hasStar {
       return nil
     }

benchmark/multi-source/Monoids/Enumeration.swift

@@ -54,8 +54,9 @@ struct RuleShape {
 struct PresentationShape {
   var rules: [RuleShape]
 
-  var presentation: Presentation {
-    return Presentation(rules: rules.map { $0.rule })
+  func presentation(alphabet: Int) -> Presentation {
+    return Presentation(alphabet: alphabet,
+                        rules: rules.map { $0.rule })
   }
 }
 
@@ -72,7 +73,7 @@ func enumerateAll(alphabet: Int, shapes: [PresentationShape], output: Bool)
   let perms = allPermutations(alphabet)
 
   for shape in shapes {
-    var p = shape.presentation
+    var p = shape.presentation(alphabet: alphabet)
     var done = false
 
 loop: while !done {
@@ -90,13 +91,14 @@ loop: while !done {
       }
 
       for rule in p.rules {
+        precondition(rule.rhs.count <= rule.lhs.count)
         if compare(rule.rhs, rule.lhs, order: .shortlex) != .lessThan {
           filteredRHS += 1
           continue loop
         }
       }
 
-      if unique.contains(p.sorted(order: .shortlex)) {
+      if unique.contains(p) {
         filteredSymmetry += 1
         continue
       }
@@ -106,7 +108,6 @@ loop: while !done {
         unique.insert(permuted.sorted(order: .shortlex))
       }
 
-      precondition(p == p.sorted(order: .shortlex))
       instances.append(p)
     }
   }
@@ -126,9 +127,12 @@ func ruleShapes(_ n: Int) -> [RuleShape] {
   for i in 0 ..< n {
     let j = n - i
 
-    // Don't generate rules with shorter left-hand side.
+    // Don't consider rules with a shorter left-hand side.
     if j < i { continue }
 
+    // Don't consider rules of the form x=1 or x=y where x, y are generators.
+    if j == 1 && i <= 1 { continue }
+
     result.append(RuleShape(lhs: j, rhs: i))
   }
   return result

benchmark/multi-source/Monoids/Monoids.swift

@@ -16,11 +16,18 @@ func run(output: Bool) async {
   await solver.solve()
 
   // These we know we can't solve.
-  let expect: [Presentation] = ["bab=aaa,bbbb=1", "aaaa=1,abbba=b", "aaa=a,abba=bb"]
+  let expectUnsolved: [Presentation] = ["bab=aaa,bbbb=1", "aaaa=1,abbba=b", "aaa=a,abba=bb"]
 
   // Make sure everything else was solved.
   let unsolved = solver.subset.map { instances[$0] }
-  if unsolved != expect {
-    fatalError("Expected \(expect), but got \(unsolved)")
+  if unsolved != expectUnsolved {
+    fatalError("Expected \(expectUnsolved), but got \(unsolved)")
+  }
+
+  // Also check finite monoid results.
+  let expectFinite = [1: 1188, 2: 2059, 3: 1233, 4: 1644, 5: 1019, 6: 1630, 7: 686, 8: 884, 9: 493, 10: 615, 11: 191, 12: 317, 13: 79, 14: 134, 15: 62, 16: 158, 17: 16, 18: 60, 19: 2, 20: 52, 21: 38, 22: 12, 24: 31, 25: 5, 26: 11, 27: 42, 28: 10, 30: 52, 32: 5, 34: 8, 36: 17, 39: 4, 42: 4, 44: 8, 48: 12, 50: 12, 52: 4, 55: 4, 56: 8, 60: 18, 64: 14, 81: 6, 84: 22, 96: 1, 100: 4, 105: 2, 120: 7, 129: 2, 147: 6, 160: 2, 165: 2, 192: 2, 195: 2, 320: 2, 324: 2, 339: 4, 605: 2, 1083: 2]
+  let finite = solver.finite
+  if finite != expectFinite {
+    fatalError("Expected \(expectFinite), but got \(finite)")
   }
 }

benchmark/multi-source/Monoids/Presentation.swift

@@ -49,17 +49,9 @@ extension Rule: ExpressibleByStringLiteral, CustomStringConvertible {
 }
 
 struct Presentation: Hashable {
+  var alphabet: Int
   var rules: [Rule]
 
-  var alphabet: Int {
-    var result: Int = 0
-    for rule in rules {
-      for s in rule.lhs { result = max(result, Int(s)) }
-      for s in rule.rhs { result = max(result, Int(s)) }
-    }
-    return result + 1
-  }
-
   var longestRule: Int {
     var result = 0
     for rule in rules {
@@ -70,8 +62,13 @@ struct Presentation: Hashable {
   }
 }
 
+func printRules(_ rules: [Rule]) -> String {
+  return rules.map { $0.description }.joined(separator: ",")
+}
+
 extension Presentation: ExpressibleByStringLiteral, CustomStringConvertible {
   init(_ str: String) {
+    self.alphabet = 2
     self.rules = str.split(separator: ",").map { Rule(String($0)) }
   }
 
@@ -80,8 +77,7 @@ extension Presentation: ExpressibleByStringLiteral, CustomStringConvertible {
   }
 
   var description: String {
-    if rules.isEmpty { return "," }
-    return rules.map { $0.description }.joined(separator: ",")
+    return printRules(rules)
   }
 }
 
@@ -145,7 +141,8 @@ extension Rule {
 
 extension Presentation {
   func permuted(_ perm: Permutation) -> Presentation {
-    return Presentation(rules: rules.map { $0.permuted(perm) })
+    return Presentation(alphabet: alphabet,
+                        rules: rules.map { $0.permuted(perm) })
   }
 }
 
@@ -367,6 +364,6 @@ extension Presentation {
     let sortedRules =
       rules.map { $0.oriented(order: order)! }
            .sorted { compare($0, $1, order: order) == .lessThan }
-    return Presentation(rules: sortedRules)
+    return Presentation(alphabet: alphabet, rules: sortedRules)
   }
 }

benchmark/multi-source/Monoids/README.md

@@ -22,3 +22,5 @@ In addition to Knuth-Bendix completion, there are some other interesting algorit
 The Knuth-Bendix implementation is pretty fast. It uses a trie to speed up reduction and finding overlaps.
 
 The main "entry point" is `func run()` in Monoids.swift.
+
+A formal write-up is here: https://factorcode.org/slava/aaaaabbabb.pdf

benchmark/multi-source/Monoids/RewritingSystem.swift

@@ -33,13 +33,13 @@ struct RewritingSystem {
   // Limits for completion
   struct Limits: Hashable {
     var maxRounds = 100
-    var maxRules = 180
+    var maxRules = 200
     var maxLength = 100
     var maxReductionLength = 100
     var maxReductionSteps = 1 << 24
   }
 
-  var limits: Limits
+  var limits = Limits()
 
   var checkedRulesUpTo = 0  // Completion progress
   var reducedRules: [UInt32] = []  // Bitmap of reduced rules
@@ -55,10 +55,9 @@ struct RewritingSystem {
     var numReductionSteps = 0
   }
 
-  init(alphabet: Int, limits: Limits) {
+  init(alphabet: Int) {
     self.alphabet = alphabet
     self.trie = Trie(alphabet: self.alphabet)
-    self.limits = limits
 
     criticalPairs.reserveCapacity(128)
   }
@@ -288,6 +287,6 @@ struct RewritingSystem {
         result.append(rule)
       }
     }
-    return Presentation(rules: result)
+    return Presentation(alphabet: alphabet, rules: result)
   }
 }

benchmark/multi-source/Monoids/Solver.swift

@@ -30,6 +30,9 @@ struct Solver {
   // This is a list of indices of all remaining unsolved instances.
   var subset: [Int]
 
+  // Histogram of finite monoid cardinality.
+  var finite: [Int: Int] = [:]
+
   var factors: [Order: [Int: [Word]]] = [:]
   var maxFactors: [Int] = []
 
@@ -86,8 +89,8 @@ struct Solver {
 
       var strategies: [Strategy] = []
 
-      for frequency in [0, 1] {
-        for factorLength in 2 ..< maxFactors.count {
+      for factorLength in 2 ..< maxFactors.count {
+        for frequency in [0, 1] {
           let strategy = Strategy(factorLength: factorLength,
                                   frequency: frequency)
           for order in orderMix[alphabet + 1]! {
@@ -104,8 +107,13 @@ struct Solver {
 
       for n in subset {
         let instance = instances[n]
-        print("\(n)\t\(instance)\thard")
+        print("\(n + 1)\t\(instance)\thard")
       }
+
+      print("# Finite monoids: ", terminator: "")
+      print(finite.sorted { $0.0 < $1.0 }
+                  .map { "\($0): \($1)" }
+                  .joined(separator: ", "))
     }
   }
 
@@ -119,8 +127,8 @@ struct Solver {
   }
 
   mutating func collectFactors(_ n: Int, _ p: Presentation, order: Order) -> [Word] {
-    // FIXME: The 2 is a magic number
-    let words = p.collectFactors(order: order, upToLength: p.longestRule + 2)
+    // FIXME: The 6 is a magic number.
+    let words = p.collectFactors(order: order, upToLength: 6)
     if !words.isEmpty {
       let longestFactor = words.map { $0.count }.max()!
       for i in 2 ... longestFactor {
@@ -243,18 +251,19 @@ struct Solver {
               retired[strategyIndex]!.append(n)
 
               // Print the instance and solution.
-              var str = "\(n)\t\(instances[n])\t"
+              var str = "\(n + 1)\t\(instances[n])\t"
 
               if let cardinality = solution.cardinality {
                 str += "finite:\(cardinality)"
+                finite[cardinality, default: 0] += 1
               } else {
                 str += "infinite"
               }
               str += "\tfcrs:\(solution.presentation)"
 
               // Print the extra generators that were added, if any.
               if !solution.extra.isEmpty {
-                str += "\t\(Presentation(rules: solution.extra))"
+                str += "\t\(printRules(solution.extra))"
               }
 
               if output {