Phase 4: Substitution Bug Fix - Summary

Problem

The Universal Levenshtein Automaton was rejecting valid words that required substitution operations.

Example: "test" → "text" (1 substitution: s→x) was incorrectly rejected with max_distance=2.

Test Results Before Fix:

• 6/10 acceptance tests passing
• All 4 failing tests involved substitutions

Root Cause

Location: src/transducer/universal/state.rs, line 155 in add_position() method

Bug: The subsumption logic was backwards. When adding a new position to the state:

// WRONG (before fix):
if !self.positions.iter().any(|p| subsumes(&pos, p, self.max_distance)) {
    self.positions.insert(pos);
}

This rejected a new position pos if it subsumed any existing position p. But subsumption means "pos is BETTER than p", so pos should be ADDED (and p should be removed).

Subsumption Rule

From thesis Definition 11 (page 22):

• Position i#e subsumes j#f if f > e AND |j - i| ≤ f - e
• Meaning: i#e is better (fewer errors) and can cover j#f's matches

Why It Failed

At step 4 of processing "test" → "text":

• State before: [I-2#2, I-1#2] (both with 2 errors)
• New position from match: I+0#1 (only 1 error - BETTER!)
• Check: Does I+0#1 subsume I-1#2?
  • e=1, f=2 → f > e? YES ✓
  • |(-1) - 0| ≤ 2-1? → 1 ≤ 1? YES ✓
• Result: I+0#1 subsumes I-1#2, so it was rejected ❌

This left the state with only error positions, causing acceptance to fail.

Solution

Fixed Code:

pub fn add_position(&mut self, pos: UniversalPosition<V>) {
    // Step 1: Remove any existing positions that are subsumed by the new position
    // If pos subsumes p, then p is worse and should be removed
    self.positions.retain(|p| !subsumes(&pos, p, self.max_distance));

    // Step 2: Add the new position only if it's not subsumed by any remaining position
    // If p subsumes pos for some p, then pos is worse and should be rejected
    if !self.positions.iter().any(|p| subsumes(p, &pos, self.max_distance)) {
        self.positions.insert(pos);
    }
}

Key Changes:

1. Line 151 was already correct (remove positions subsumed by new pos)
2. Line 155 logic was flipped:
   • Before: Reject if pos subsumes something (WRONG)
   • After: Reject if something subsumes pos (CORRECT)

Validation

Cross-Validation Test

Created tests/universal_vs_parameterized.rs to compare Universal vs Parameterized automata:

// Test that both implementations agree
let universal = UniversalAutomaton::<UniversalStandard>::new(max_distance);
let universal_result = universal.accepts(word, input);

let transducer = Transducer::standard(dict);
let parameterized_results: Vec<_> = transducer.query(input, max_distance).collect();
let parameterized_result = parameterized_results.iter().any(|w| w == word);

assert_eq!(universal_result, parameterized_result);

Result: All 3 cross-validation tests pass ✓

Acceptance Test Suite

Before Fix: 6/10 passing After Fix: 10/10 passing ✓

All test cases now work:

• ✓ Exact matches
• ✓ Single deletions
• ✓ Single insertions
• ✓ Single substitutions (WAS BROKEN, NOW FIXED)
• ✓ Multiple edit operations
• ✓ Empty strings
• ✓ Longer words

Debugging Process

1. Cross-validation: Compared Universal vs Parameterized implementations

   • Confirmed Universal was rejecting valid matches

2. Detailed tracing: Added debug output to track:

   • State positions after each character
   • Bit vector matches
   • Position successor generation

3. Trace analysis: Discovered:

   • Match was correctly detected: I+0#1
   • But final state didn't include it: [I-2#2, I-1#2]
   • Position was being dropped during state construction

4. Subsumption analysis: Calculated:

   • I+0#1 subsumes I-1#2 (better position)
   • Line 155 rejected I+0#1 for subsuming something
   • This was backwards!

5. Fix applied: Flipped the subsumption logic

6. Validation: All tests pass

Files Modified

1. src/transducer/universal/state.rs (line 148-158)

   • Fixed add_position() subsumption logic

2. src/transducer/universal/automaton.rs (line 526-534)

   • Fixed incorrect test assertion (test→best is distance 1, not 2)

3. tests/universal_vs_parameterized.rs (NEW)

   • Cross-validation test suite

Documentation Created

1. PHASE4_TRACE_ANALYSIS.md - Detailed trace of "test"→"text" execution
2. PHASE4_BUG_FIX_SUMMARY.md - This document
3. DIAGONAL_CROSSING_DEBUG_SUMMARY.md - Previous debugging session notes

Impact

This fix resolves the substitution handling bug and brings the Universal Levenshtein Automaton to full correctness for Standard (insert/delete/substitute) operations with max_distance ≤ 2.

Status: Phase 4 implementation complete ✓