Multi-Layer WFST Architecture for Programming Language Error Correction
This directory contains comprehensive documentation for a multi-layer error correction system that addresses lexical, grammatical, semantic, and behavioral errors in programming languages, with specific focus on Rholang (a process calculus language).
grammar-correction/
├── README.md (this file) # Overview and navigation
├── MAIN_DESIGN.md # Comprehensive design document
└── theoretical-analysis/ # Formal analysis of properties
├── README.md # Navigation for theoretical docs
├── index.md # Quick reference index
├── complete-analysis.md # Full formal analysis (52 KB)
├── quick-reference.md # Property matrix & theorems (11 KB)
├── visual-guide.md # ASCII diagrams (33 KB)
├── executive-summary.md # For stakeholders (19 KB)
└── completion-report.md # Analysis deliverables
../guides/grammar-correction/
└── implementing-guarantees.md # Implementation guide with code
../research/grammar-correction/
└── analysis-log.md # Scientific methodology & experiments
⏱️ Quick Overview (5 minutes)
theoretical-analysis/index.md👔 Management/Stakeholder (30 minutes)
theoretical-analysis/executive-summary.md💻 Developer/Implementer (1-2 hours)
MAIN_DESIGN.md../guides/grammar-correction/implementing-guarantees.md🔬 Researcher/Deep Dive (3-4 hours)
MAIN_DESIGN.mdtheoretical-analysis/complete-analysis.md../../research/grammar-correction/analysis-log.mdInput: Raw Text with Errors
↓
┌─────────────────────────────────────┐
│ Layer 1: Lexical Correction │ ← liblevenshtein (existing)
│ • Levenshtein automata │
│ • Character-level edit distance │
└────────────┬────────────────────────┘
│ corrected tokens
┌────────────▼────────────────────────┐
│ Layer 2: Grammar Correction │ ← THIS DESIGN
│ • Tree-sitter GLR parsing │
│ • BFS over parse states │
│ • LookaheadIterator API │
└────────────┬────────────────────────┘
│ valid parse trees
┌────────────▼────────────────────────┐
│ Layer 3: Semantic Validation │ ← THIS DESIGN
│ • Type checking (Hindley-Milner) │
│ • Scope analysis │
└────────────┬────────────────────────┘
│ type-correct programs
┌────────────▼────────────────────────┐
│ Layer 4: Semantic Repair │ ← THIS DESIGN
│ • Error localization (SHErrLoc) │
│ • Constraint solving (SMT) │
│ • Template-based fixes │
└────────────┬────────────────────────┘
│ repaired programs
┌────────────▼────────────────────────┐
│ Layer 5: Process Verification │ ← THIS DESIGN (Rholang-specific)
│ • Session type checking │
│ • Deadlock detection │
│ • Race condition analysis │
└────────────┬────────────────────────┘
│
Output: Corrected, Verified Program
| Layer | Determinism | Correctness | Optimality |
|---|---|---|---|
| 1. Lexical | ✓ (with tie-breaking) | ✓ | ✓ (per-token) |
| 2. Grammar | ~ (conditional) | ✓ | ~ (BFS: uniform cost only) |
| 3. Semantic Val | ✓ (with det vars) | ✓ | ✓ (perfect filter) |
| 4. Semantic Rep | ~ (conditional) | ~ (syntactic ✓) | ✗ (undecidable) |
| 5. Process Ver | ✓ | ✓ | N/A |
| Pipeline | ~ (achievable) | ✓ (syntactic) | ✗ (approximation) |
Key Findings:
For details, see theoretical-analysis/quick-reference.md.
Layer 1: Lexical - Fixes character-level typos
prnt → print\mathcal{O}(n)$ recognition)Layer 2: Grammar - Fixes syntax errors
if x { print(x) → if x { print(x) }Layer 3: Semantic Validation - Filters type-incorrect programs
"hello" + 5 (type mismatch)Layer 4: Semantic Repair - Fixes type/scope errors
x + 1 where x undefined → suggest similar namesLayer 5: Process Verification - Ensures protocol correctness (Rholang)
MAIN_DESIGN.md (✅ COMPLETE, 5,143 lines)
Status: ✅ Complete (Sections 1-17 fully written)
theoretical-analysis/complete-analysis.md (52 KB, complete)
theoretical-analysis/quick-reference.md (11 KB, complete)
theoretical-analysis/visual-guide.md (33 KB, complete)
theoretical-analysis/executive-summary.md (19 KB, complete)
../../guides/grammar-correction/implementing-guarantees.md (33 KB, complete)
../../research/grammar-correction/analysis-log.md (23 KB, complete)
Immediate (1-2 weeks):
Short-term (2-3 weeks): 4. Implement Hindley-Milner type inference (~1 week) 5. Add SHErrLoc error localization (~3-5 days) 6. Implement template-based semantic repair (~1 week)
Medium-term (4-8 weeks): 7. Session type checking for Rholang (~2-3 weeks) 8. Deadlock and race detection (~1 week) 9. Complete LSP integration (~1 week) 10. Performance benchmarks and optimization (~1-2 weeks)
Total: 12-16 weeks for production-ready implementation
For detailed roadmap, see MAIN_DESIGN.md Sections 14-15.
This design extends the existing liblevenshtein hierarchical correction framework:
docs/design/hierarchical-correction.md (lexical layer)This programming language grammar correction design shares the same three-tier hybrid architecture with the WFST-based text normalization design (../../wfst/ (planned)), but targets different domains:
Both designs follow the Chomsky hierarchy (Regular → Context-Free → Unrestricted):
┌────────────────────────────────────────────────────────────┐
│ Tier 1: Regular (FST/NFA) - O(n) deterministic │
│ • Programming Language: Levenshtein (Layer 1) │
│ • Text Normalization: FST + NFA phonetic │
└────────────────────────────────────────────────────────────┘
↓
┌────────────────────────────────────────────────────────────┐
│ Tier 2: Context-Free (CFG) - O(n²-n³) deterministic │
│ • Programming Language: Tree-sitter (Layer 2) │
│ • Text Normalization: Earley parser + lattice parsing │
└────────────────────────────────────────────────────────────┘
↓
┌────────────────────────────────────────────────────────────┐
│ Tier 3: Unrestricted (Neural/CSG) - O(n²+) probabilistic │
│ • Programming Language: SMT + Type inference (Layers 3-5) │
│ • Text Normalization: LLM integration │
└────────────────────────────────────────────────────────────┘
Shared Principle: Use the simplest formalism that can solve the problem (deterministic symbolic layers before neural fallback).
1. Lattice Parsing (../../wfst/lattice_parsing.md (planned))
2. LLM Integration Patterns (../../wfst/architecture.md#integration-with-large-language-models (planned))
3. Deployment Modes (../../wfst/architecture.md#deployment-modes (planned))
1. Process Calculus Verification (Layer 5)
2. SMT-Based Semantic Repair (Layer 4)
3. Incremental Parsing (Tree-sitter)
For detailed comparisons and integration strategies, see:
../../wfst/README.md (planned) - WFST architecture overview../../wfst/architecture.md (planned) - Complete system design../../wfst/lattice_parsing.md (planned) - Lattice parsing technique../../wfst/cfg_grammar_correction.md (planned) - CFG-based grammar correction for codeThis 5-layer code correction design is extended by the MeTTaIL architecture for conversational AI and LLM agent support:
| Layer | Component | Documentation |
|---|---|---|
| Dialogue Context | Turn tracking, entity registry, topic graph | Dialogue README |
| Simplification | Post-correction source-to-source optimization | Simplification Transpiler |
| Pragmatic Reasoning | Speech act classification, implicature resolution | Correction WFST Overview |
| LLM Integration | Prompt preprocessing, response validation | LLM Integration |
| Agent Learning | Feedback collection, pattern adaptation | Agent Learning |
For integrating grammar correction with MeTTa pattern matching:
Formal correctness proofs for the grammar correction layers:
All references in this documentation are open-access (arXiv, ACL Anthology, author websites).
Key Papers:
Full bibliography: MAIN_DESIGN.md Section 16.
MAIN_DESIGN.mdtheoretical-analysis/complete-analysis.md../../guides/grammar-correction/implementing-guarantees.md../../research/grammar-correction/analysis-log.mdIf you find broken links, unclear sections, or errors:
theoretical-analysis/README.md for cross-referencestheoretical-analysis/index.md for quick navigationThis design documentation is part of the liblevenshtein-rust project.
License: Apache-2.0 (same as main project)
Attribution: Design by Claude (Anthropic) based on extensive research of open-access academic literature.
Date: January 2025
v1.0 (2025-01-04): Initial comprehensive design and theoretical analysis
v1.1 (2025-11-21): Cross-pollination with WFST design
v2.0 (2025-11-21): MAIN_DESIGN.md completion
Last Updated: 2025-11-21 Status: ✅ Design Complete (All 17 sections), Implementation Pending Maintainer: liblevenshtein-rust project
Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |