io.vinarytree/liblevenshtein-clojure
4.0.0-rc.4
cljdoc
vinary-tree/liblevenshtein-rust
Liking cljdoc? Tell your friends :D
Articles
Readme
Changelog
mathlint-include
liblevenshtein-rust Technical Glossary
Documentation Index
Security & Threat Model
Dictionary Layer
Dictionary Layer — Implementations
DoubleArrayTrieChar Implementation
DoubleArrayTrie Implementation
DynamicDawgChar Implementation
DynamicDawg Implementation
PathMapDictionary Implementation
SuffixAutomaton Implementation
Levenshtein Automata Layer
Intersection and Traversal Layer
Layer 4: Distance Calculation
Distance Calculation — Algorithms
Iterative Dynamic Programming Algorithm
Distance Calculation Optimizations
Recursive Memoization Algorithm
SIMD Optimization Layer
Zipper Navigation Pattern
Layer 7: Contextual Completion Engine
Formal Verification Requirements for Contextual Completion (Phase 9)
Contextual Completion — Implementation
Checkpoint System Implementation
Completion Engine Implementation
Context Tree Implementation
Draft Buffer Implementation
Contextual Completion Patterns
Parallel Workspace Indexing for Contextual Code Completion
Contextual Completion — Use Cases
Code Completion Use Case
Incremental Editing Use Case
Layer 8: Caching Layer
Caching Layer — Eviction Policies
Age (FIFO) Eviction Policy
CostAware Eviction Policy
LFU (Least Frequently Used) Eviction Policy
LRU (Least Recently Used) Eviction Policy
MemoryPressure Eviction Policy
TTL (Time-to-Live) Eviction Policy
Layer 9: Value Storage Architecture
Affine-gap dictionary automata
Unrestricted Damerau–Levenshtein automata
Elastic measures over a prefix-shared quantized trie
Language products: fuzzy distance to a regular language
Exact generalized-operation grid
Literate Class-A preset algorithms
Literate downstream-query algorithms
Documentation Index
liblevenshtein Algorithm Documentation
Fuzzy Maps Optimization Analysis
Fuzzy Map Baseline Performance Analysis
Phase 1.5 Optimization Summary
Fuzzy Map Benchmark Results - Phase 2
Fuzzy Map Profiling Analysis - Phase 3
Phase 4 Optimization Results
Phase 5: Serialization Support Assessment
Fuzzy Maps Implementation - Final Report
Fuzzy Maps — Optimization Analysis Records
FuzzyMultiMap Performance Analysis
FuzzyMultiMap Optimization Results
Hierarchical Lexical Scope Completion - Design Document
Hierarchical Scope Completion Analysis
Hierarchical Scope Completion - Benchmark Results
Architecture
Architecture Overview — the three concern-areas
Archive
Org-Mode Documentation
bench_results_arc_str
bench_results_balanced
bench_results_baseline
bench_results_concurrent
bench_results_dashmap
bench_results_parking_lot
benchmark_baseline
benchmark_no_pgo
benchmark_with_pgo
build_baseline_no_pgo
dawg_benchmark_adaptive
dawg_benchmark_baseline
dawg_benchmark_optimized
dawg_contains_arc_optimized
dawg_contains_threshold16
dawg_edge_iteration_optimized
dawg_query_comparison_results
eviction_wrapper_bench_baseline
fuzzy_multimap_baseline
ordered_query_benchmark_results
pgo_build_log
pgo_build_log_v2
profiling_benchmark_arc_optimized
profiling_benchmark_pathnode
rayon_eval_parallel
rayon_eval_sequential
real_world_benchmark_results
serialization_benchmark_baseline
serialization_benchmark_optimized
threshold_analysis_results
threshold_tuning_results
Debug Findings: "kat"→"chath" Double Split Failure
Development Session Summary - 2025-11-12
Phase 4: Debugging Session Summary
CI Benchmark Integration
CompressedSuffixAutomaton Status
Double-Array Trie Implementation - Status Report
DoubleArrayTrie Integration Status Report
Implementation Status: Optimized DAWG and DAT Comparison
Archived Implementation Records
Refactoring Plan: Shared Commands and Module Splitting
In-Place State Mutation API - Detailed Analysis
Optimization Summary
Phase 4: SmallVec for State Positions Investigation
Phase 5 Profiling Verification
Phase 5: StatePool Optimization Results
Phase 6: Arc Path Optimization Results
Phase 6 Profiling Verification
Profiling Comparison: Before vs After Optimization
Performance Optimization Documentation
benchmark_results_phase5
benchmark_results_phase6
profiling_phase5
profiling_phase6
Arc Reference Counting Optimization Results
Code Completion Performance Guide
Contextual Filtering Optimization Guide
DAWG Implementation Comparison
DAWG Optimizations Applied - Phase 1
DAWG Optimization Opportunities
DAWG Optimization Results - Phase 1
Index-Based Query Iterator Results
liblevenshtein-java vs liblevenshtein-rust Feature Comparison
Optimization Results: Phase 1
Filtering & Prefix Matching: Complete Optimization Summary
PathNode Optimization Results
Performance Analysis: Filtering & Prefix Matching
Profile-Guided Optimization (PGO) Impact Analysis
Phase 2 Optimization Results
Phase 3 Optimization Results
Profiling and Profile-Guided Optimization Results
Query Iterator Arc Usage Analysis
Archived Performance Documentation
Real-World Dictionary Validation Results
Serialization Benchmarks - Baseline (Before Optimizations)
Serialization Optimizations Applied - Phase 1
Serialization Optimization Plan
Serialization Optimization Results - Phase 1
Adaptive Threshold Tuning Results
Research Initiatives
Research Initiatives Tracking
Archived theory deep-dives (superseded by libdictenstein)
Foundations: Tries and Disk I/O
B-trie: Disk-Based Burst Trie
The Adaptive Radix Tree (ART)
Persistent ART: Disk Storage Techniques
Buffer Management
Persistent ARTrie Design
PersistentARTrie Benchmark Results
Archived: disk-trie deep-dive chapters (superseded by libdictenstein)
Introduction: The Substring Search Problem
Suffix Automaton (DAWG) Theory
Compact DAWG (CDAWG) Theory
Symmetric Compact DAWG (SCDAWG) Theory
On-line SCDAWG Construction
SCDAWG Operations
Annotated Bibliography
Archived: SCDAWG deep-dive chapters (superseded by libdictenstein)
BTreeSet vs SmallVec Comparison for Universal Transducers
Diagonal Crossing Bug Analysis and Resolution Notes
Diagonal Crossing Debug Session - Summary
Phase 4: Bit Vector Position Bug Analysis
Phase 4: Automaton Acceptance Bug Analysis
Phase 4: Substitution Problem - Deep Analysis
Phase 4: Trace Analysis - "test" → "text" Substitution Bug
BTreeSet Subsumption Optimization - Test Fixes
Universal Levenshtein Automaton: BTreeSet vs SmallVec Performance Analysis
Archived: BTreeSet Implementation for Universal Levenshtein Transducers
Session 1: trace_composition_cost_bound - Technical Findings
Verification Session Notes
Debugging Session Summary - PatternOverlap.v Compilation
PatternHelpers.v Split Implementation Log
Backend Comparison Results
Backend Performance Comparison (Post-DAT Optimization)
Double-Array Trie Optimization Results
Double-Array Trie Performance Analysis
DAWG Optimization Analysis: Cache Locality & Memory-Mapped Loading
Double-Array Trie Analysis for liblevenshtein-rust
Final Backend Comparison Results - All 6 Backends
Optimization Results: Prefix and Substring Matching
Optimization Summary - Complete Session
Performance Analysis: Prefix and Substring Matching
Benchmarks and Performance Analysis
Academic Benchmark Reproduction
All-backend optimization-propagation evidence
backend_comparison_6backends
backend_comparison_optimized
backend_comparison_results
Cross-Language Benchmark Results — run `phase0`
C++ vs C++: liblevenshtein-cpp against the Rust-backed C++ facade
Java vs Java: liblevenshtein-java 3.0.0 against the Rust-backed JVM binding
Root causes and closure of the liblevenshtein-java performance gap
Cross-Language Benchmark Methodology
dat_benchmark_results
dat_fuzzy_matching_results
dat_levenshtein_benchmark
dat_optimized_benchmark
Benchmark Results: January 2026 Improvements
Optimization and profiling methodology
Optimization propagation across automata and dictionary backends
Benchmark Ledger — PathMap TrieRef Rework
Bounded query-cache policy matrix
Language-Binding Findings Ledger — liblevenshtein-rust
Binding / ABI Performance Experiments — liblevenshtein-rust
Language-binding documentation hub
The `llev_*` C ABI, function by function
Collection-protocol parity and native Rust idioms
The resource consumer — `src/bindings.rs` from the inside
WASM and JavaScript topology — one umbrella runtime, three paths
Bug Reports and Analysis
Cross-Validation Bug Report
Cross-Validation Test Coverage Summary
Cross-Validation Testing: Status and Next Steps
Empty String Bug Fix - Complete
MergeAndSplit Algorithm Bug Analysis
Transposition Bug Analysis
Transposition Bug Fix Summary
Completion Reports
Phase 2 Complete - Next Steps
Levenshtein Distance Optimization - Complete
Phase 2 Optimization: COMPLETE ✅
Levenshtein Distance Functions: Project Completion Summary
Lazy vs Eager Levenshtein Automata
Concepts
Design Documents
Exact affine-gap automaton design
The `PositionKind` and `AutomatonVariant` seam
Class-A alignment presets
Contextual Completion API Design
Contextual Completion Implementation Progress
Contextual Completion Implementation Roadmap
Hierarchical Zipper Architecture for Contextual Code Completion
Ordered cost-monoid design
Crate boundary and pruning duality
Downstream query surfaces
Dynamic DAWG Implementation
Elastic kernels and the generic exact trie walker
Generalized-automaton repair
GeneralizedAutomaton Design Document
Generalized operation sets
Multi-Layer Grammar and Semantic Error Correction
Grammar and Semantic Error Correction
Grammar Correction Project: Complete Work Summary
Grammar Correction Pipeline: Benchmark Specification
Exact multi-kind Dyck correction and its projection bound
Theoretical Analysis of Multi-Layer Error Correction Pipeline
Theoretical Guarantees of Multi-Layer Error Correction Pipeline
Theoretical Analysis: Completion Report
Executive Summary: Theoretical Analysis of Multi-Layer Error Correction
Theoretical Analysis: Complete Index
Theoretical Guarantees - Quick Reference
Theoretical Properties - Visual Guide
WFST Architecture Extensions for Programming Language Error Correction
Hierarchical Error Correction via Automata Composition
Language-product design
Numeric, Weighted-Cost, and Correctness Hardening
PathMap Integration Rework — TrieRef Nodes + Zero-Plumbing Entry Points
Prefix Matching with Levenshtein Automata
PrefixZipper Design Documentation
Protocol Buffers Dictionary and Operation-Set Persistence
Suffix Automaton Design Document
True-Damerau streaming design
Zipper-Based vs Node-Based Query Performance Analysis
Developer Guide
liblevenshtein-rust Architecture
Building the library
Contributing to liblevenshtein-rust
Performance Optimizations
Publishing
Cargo workspace layout
API Design Decision: Substitution Policy Integration
Final Cleanup Log - Restricted Substitutions
Restricted Substitutions - Implementation Complete ✅
Option 1 Analysis: Generic Transducer<D, P = Unrestricted>
Option 1 Implementation: Generic Transducer<D, P = Unrestricted>
Phase 3 Complete: Lazy Automaton Policy Integration
Phase 3 Progress: Lazy Automaton Integration (Day 4-7)
Phase 4 Complete: Eager Automaton Policy Integration
Substitution Policy Implementation Status
Restricted Substitutions Implementation: Progress Summary
Development Records
Restricted Substitutions Feature - Implementation Complete
Implementation Plan: Restricted Substitutions with Lazy/Eager Cross-Validation
Diagram Style Guide & Tooling
01 · Getting Started: Your First Spell Checker
02 · Dictionaries: Static, Dynamic, and on Disk
03 · Algorithms & Result Ordering
04 · Queries, Unicode & Custom Substitutions
05 · Values & Fuzzy Maps
06 · Contextual Completion Engine
07 · Performance & Concurrency
08 · Real-World Project: Phonetic Spellcheck
Examples & Tutorials
Phase 3: Standard Operations Verification
Phase 4: Phonetic Operations - Formal Specification
Formal Verification Findings
Phase 4: Formal Verification and Bug Fix
Phase 4: Phonetic Operations - Implementation Summary
Formal Verification of Levenshtein Automata
Formal Verification Status Report
Formal Verification Validation Matrix
Subsumption Properties - Formal Proof Documentation
Position Invariants - Formal Proof Documentation
Context Tree Visibility - Formal Proof Documentation
Draft Buffer Consistency - Formal Proof Documentation
Checkpoint Stack Correctness - Formal Proof Documentation
Query Fusion Completeness - Formal Proof Documentation
Levenshtein Distance Correctness - Formal Proof Documentation
Hierarchical Visibility Soundness - Formal Proof Documentation
Finalization Atomicity - Formal Proof Documentation
Contextual Completion - Formal Verification Documentation
Formal-Verification Proofs — Records
Generalized Operations — Records
Phase 2 Implementation Plan: Runtime-Configurable Operations
Phase 2 Next Steps: Successor Generation Refactoring
Phase 2 Progress Report: Runtime-Configurable Operations
Phase 2d Analysis: Multi-Character Operations
Phase 2d Implementation - Completion Report
Phase 2d Implementation Plan: Multi-Character Operations
Phase 2d Planning Session Summary
Phase 3 Implementation - Session Handoff Document
Phase 3a Completion Report - Phonetic Merge Operations
Phonetic split and two-for-two operation requirements
DSL Grammar Reference
Hierarchical Lexical Scope Completion
Guides
Restricted Substitutions Guide
Articulatory Distance: Phonetically-Informed Substitution Costs
Compositional Spelling Correction: Phonetic NFAs + Levenshtein Automata
Grammar-Correction Guides
Implementing Theoretical Guarantees
Phonetic Rules Developer Guide
Implementation Status
Phase 6: Dictionary Layer Completeness - Status Report
UTF-8 Character-Level Support Implementation
UTF-8 Character-Level Implementation - Status Report
MORK FuzzySource Adapter for Approximate String Matching
Phase A: FuzzySource Implementation Guide
Phase D: Grammar Correction via MORK Pattern Matching
Phase B: Lattice Integration Guide
Structural Repair for Programming Languages
Phase C: WFST Composition Guide
PathMap Integration Infrastructure
Language bindings architecture
LLRE File Format
MeTTaIL: Semantic Type Checking for MeTTa
Feedback Collection
Pattern Learning
User Preferences
Online Learning
Agent Learning and Feedback Integration
Unified Correction WFST Architecture
Tier 1: Lexical Correction
Tier 2: Syntactic Validation
Tier 3: Semantic Type Checking
Data Flow Through the Correction Stack
Integration Possibilities
MeTTaIL — Correction WFST
Discourse Semantics
Coreference Resolution
Topic Management
Pragmatic Reasoning
Dialogue Context Management
MeTTaIL Scala Prototype
MeTTaIL Rust Prototype
Rholang Integration
Implementation Roadmap
MeTTaIL — Implementation
Prompt Preprocessing
Output Postprocessing
Hallucination Detection
Context Injection
LLM Agent Integration
OpenCog Hyperon Architecture
Hyperon-Experimental: MeTTa Reference Implementation
MeTTaTron: F1R3FLY.io's MeTTa Compiler
MORK and PathMap Integration
MeTTaIL — MeTTa Ecosystem
MeTTaIL — Reference
Bibliography
Gap Analysis: Current State to Full OSLF
Semantic Type Checking Use Cases
Simplification Transpiler Architecture
Layer 1: Analysis Layer
Layer 2: Rule Application Layer
Layer 3: Strategy Selection Layer
Layer 4: Verification Layer
Rholang Structural Congruence Rules
Termination Proof
Performance Targets
RPO-Based Congruence Proofs
Transparency Guarantees for Simplification
Bisimulation-Based Optimization Strategies
Up-To Techniques for Efficient Bisimulation Verification
Source-to-Source Simplification Transpiler
MeTTa Operational Semantics
Native Type Theory (OSLF)
Gph-enriched Lawvere Theories and GSLTs
The RHO Calculus
Type Lifting: Deriving Types from Operational Semantics
Inference Rules: A Practical Guide for Implementers
MeTTaIL — Theoretical Foundations
Migrating to the split CLI in 0.10
Migration Guide: Lazy/Eager Terminology
Migration Guides
Flame Graph Analysis - Query Iterator Optimization
H1 Optimization Implementation Plan
H1 Optimization Results - FINAL
H1_partial
H1_phase2
Phase 3 H2 Optimization - Complete Comparison Analysis
Phase 3 H2 Optimization Results - FINAL
H2_baseline
H2_conditional
Phase 1: Baseline Establishment & Hypothesis Formation
Phase 1.3: Flamegraph Analysis Results
Phase 3: H2 Optimization Implementation Plan
Pool and Intersection Optimization Analysis
Pool and Intersection Optimization Report
Optimization Progress Summary
Query Iterator Optimization - COMPLETE
Query Iterator Performance Analysis
Query Iterator Review, Testing, and Profiling - Summary
Optimization Documentation Index
H2 Optimization Session Summary - 2025-11-18
State Operations Analysis
State Operations Optimization Report
Subsumption Logic Analysis
Subsumption Benchmark Results
Subsumption Optimization Analysis - Final Report
Position Transition Function Analysis
Position Transition Function Optimization Report
UTF-8 Dictionary & Fuzzy Query Optimization Status
flamegraph_analysis
flamegraph_hotspots
LLev and Fuzzy Regex Optimization Journal
Lazy vs Eager Levenshtein Automata: Performance Comparison
Parameterized vs Universal Automata — Records (2025-11-11)
Scientific Optimization Journal: PhoneticNormalizedDictionary
Phonetic Rules Performance Investigation Log
Phase 1: Baseline Investigation
Phase 2: Code Analysis - Allocation Patterns
Phase 3: Optimization Results - can_apply_at() Helper
Phase 4: Iteration Count Analysis
Phase 5: H3 Cache Inefficiency Analysis
Phase 6: H4 Slice Copying Overhead Analysis
Phase 7: Algorithmic Optimization Analysis (Position Skipping)
Phonetic Rules Optimization — Records
post_H2_analysis
PrefixZipper Baseline Performance Analysis
PrefixZipper Optimization Log
SubstitutionSet Optimization - Experiment Log
SubstitutionSet Baseline Performance Results
Hypothesis 1: Const Array Optimization - Results
Hypothesis 2: Bitmap for ASCII Operations
H1 Profiling Results: Integration Impact Analysis
Small-Set Crossover Analysis: Hash vs Linear Scan
Hypothesis 3: Hybrid Small/Large Strategy
SubstitutionSet Optimization - Final Summary
H4-H6 Optimization Evaluation
SubstitutionSet Optimization — Records
Universal Levenshtein Automata Optimization Report
Universal Levenshtein Automata — Optimization Reports (2025-11-11)
Universal State Performance Analysis - Post Cleanup
Universal State (Post-Cleanup) — Records (2025-11-12)
Optimizations — Records
DynamicDawg Complete Optimization Report
DynamicDawg Performance Optimization Results
DynamicDawg Optimization Results - Session 2025-11-03
RCU/Atomic Swapping Assessment for DynamicDawg
Beider-Morse Phonetic Matching Algorithm Extraction
Caverphone Algorithm Extraction
Cologne Phonetic (Kölner Phonetik) Algorithm Extraction
Daitch-Mokotoff Soundex Algorithm Extraction
Metaphone and DoubleMetaphone Algorithm Extraction
NYSIIS Algorithm Extraction
Phonetic Algorithm Extraction for LLev Rules
Soundex Algorithm Extraction
Vinary Tree `4.0.0-rc.1` release ledger
Vinary Tree `4.0.0-rc.2` release ledger
Vinary Tree `4.0.0-rc.3` release ledger
Vinary Tree `4.0.0-rc.4` release ledger
Release evidence ledgers
Releasing the Vinary Tree language bindings
Research and Analysis
ARTrie — Research Record
baseline-u32-raw
baseline-u8-raw
baseline-u32-stats
baseline-u8-stats
ARTrie Optimization Scientific Ledger
Batch Processing — Research Record
Batch Query Processing Experiment Log
Bimachines and liblevenshtein-rust: Applicability Analysis
Bimachines — Research Record
Branch Archive: Retired Experiment Branches
Comparative Analysis — Research Record
Distance Functions: Initial Benchmark Analysis
Formal Verification Tools for Rust: Research Summary
GPU Acceleration for Levenshtein Distance: Feasibility Analysis
Java vs Rust Implementation Comparison: Empty String Bug Analysis
Rayon Integration Evaluation Results
Distance Optimization Research
Levenshtein Distance Functions: Implementation Summary
Phase 2 Optimization Results
Phase 2 Optimization - Executive Summary
Distance Functions: Optimization Roadmap
Banded dynamic time warping and LB_Keogh: source and implementation analysis
Edit distance with Real Penalty: paper summary and implementation analysis
Norvig Corpus Integration - Implementation Summary
MP DAT Implementation Plan
Norvig Corpus Integration - Implementation Plan
Evaluation Methodology for Levenshtein Automata
Eviction Wrapper — Research Record
Eviction Wrapper Optimization Plan
Eiter–Mannila discrete Fréchet: paper and implementation analysis
Research roadmap
Gotoh 1982: engineering summary
Grammar Correction — Research Record
Theoretical Analysis Research Log
Fast String Correction with Levenshtein-Automata - Complete Paper Summary
Fast String Correction with Levenshtein-Automata
Levenshtein Automata - Glossary
Implementation Mapping: Paper to Code
Lowrance–Wagner 1975: engineering summary
English Phonetic Corrections Feasibility Analysis
English Phonetic Corrections: Practical Implementation Guide
Generalized Operations Framework: Implementation Status
Phonetic Corrections — Research Record
SIMD Optimization Research
Phase 4 Batch 2A: Transducer Core SIMD - Complete ✅
Batch 2A: Position Subsumption SIMD - Complete ✅
Batch 2B: Dictionary Edge Lookup SIMD - Performance Analysis
SIMD Optimization Opportunities Analysis
Phase 3 SIMD Reassessment
Phase 3: SIMD Vectorization Research
Phase 3: SIMD Vectorization Results
Phase 4 Batch 1: Foundation & Quick Wins - Complete ✅
Phase 4: SIMD Optimization - Completion Status
Time Warp Edit Distance: source analysis and implementation contract
Universal Levenshtein Automata - Algorithms
Universal Levenshtein Automata - Glossary
Universal Levenshtein Automata - Implementation Mapping
Universal Levenshtein Automata - Paper Summary
Parameterized Transducer Subsumption Optimization Decision
Phase 1 Completion Report
Phase 2 Week 5: State Transitions - Completion Report
Phase 3: Diagonal Crossing Functions - Completion Report
Phase 4: Substitution Bug Fix - Summary
Phase 4: Automaton Construction - Progress Report
Phase 4: Universal Automaton - Current Status
Universal Levenshtein Automata - Complete Documentation
Subsumption in liblevenshtein-java and liblevenshtein-rust
Subsumption Optimization - Pre-Sorting for Early Termination
Subsumption Optimization - Complete Analysis
TCS 2011 Paper Implementation Mapping
TCS 2011 Paper Applicability to Lazy Automata
Universal Neighborhood Automata (TCS 2011) - Comprehensive Analysis
Universal Levenshtein Automata - Theoretical Foundations
Universal Levenshtein Automata - Architectural Sketches
Universal Levenshtein Automata - Decision Matrix
Universal Levenshtein Automata - Implementation Plan
Universal Levenshtein Automata - Progress Tracker
Universal Levenshtein Automata - Technical Analysis
Universal Levenshtein Automata - Use Cases & Applications
WallBreaker Algorithm - Implementation Complete
WallBreaker Architectural Sketches
WallBreaker Benchmarking Plan
WallBreaker Implementation Decision Matrix
WallBreaker Implementation Plan
WallBreaker Implementation Progress Tracker
WallBreaker Optimization Scientific Ledger
WallBreaker Technical Analysis - Current Codebase
Weighted Levenshtein Automata - Research & Analysis
Learning Optimal Weights from Confusion Matrices
Scientific Ledger
Affine-gap correctness, pruning, and resource gate
Automata WFST Completion Audit
Automata and WFST Scientific Evaluation Ledger
Class-A preset correctness and specialization gate
Degenerate Hamming and indel dictionary walkers
Downstream query surfaces correctness and performance ledger
Banded DTW, LB_Keogh, and prefix-first pruning gate
ElasticKernel extraction and MSM compatibility gate
Shared elastic-kernel UCR classification and pruning-economics protocol
ERP kernel correctness and pruning gate
Phase 11: weighted-position collapse gate
Discrete Fréchet kernel correctness and bottleneck-monoid gate
Generalized Automaton Exact-Repair Correctness Cost
Generalized Automaton Fractional-Cost Boundary Performance
LanguageProduct cost-indexed frontier versus legacy cost-distinct frontier
MSM Automata Scientific Evaluation
OperationSet Binary Persistence and Gzip Gate
Parallel batch fuzzy-query evaluation over a shared transducer
Phase 12: prefix-shared fzf scoring
`PositionKind` seam zero-cost and compatibility gate
True Damerau–Levenshtein correctness and resource gate
TWED kernel correctness, metric contract, and pruning gate
Version-tied cross-query result cache for the Levenshtein transducer
Automaton-variant security
Binding trust model — liblevenshtein as a resource consumer
Resource-exhaustion controls for automata and dynamic programs
Disk-based tries (PersistentARTrie) — integration with liblevenshtein
Classifying edit distances before implementing them
SCDAWG — integration with liblevenshtein
Snapshot semantics — the cursor laws and their persistence-theory basis
Time Series — Records
MSM Time Series Benchmark Analysis
Universal Levenshtein Automaton Documentation
Session Completion Summary - Universal Transposition Implementation
Hypothesis H4: Understanding Bit Vector Semantics
Hypothesis H5: Offset Calculation Defect in Transposition Completion
Hypothesis H6: Test Assertions May Be Incorrect
Lazy to Universal Automaton Mapping for Transposition
Merge/Split Operations Analysis - Phase 3
Universal merge/split variant: Phase 3 completion record
Transposition Fix - Cross-Validation with Lazy Automaton
Transposition Logic - Hypothesis 2
Transposition Logic - Hypothesis 3: Invert the Condition
Universal Automaton: Transposition and Merge/Split Implementation Plan
Transposition Manual Trace - "ab" → "ba"
Universal Automaton Transposition Implementation - Phase 1 Complete
Universal Automaton Transposition Implementation - Phase 1 Update
Universal Automaton Transposition Implementation - Phase 2 Complete
Transposition Implementation - Debugging Required
Transposition Implementation Summary - Phase 2
User Guide
Levenshtein Algorithm Guide
Dictionary Backend Guide
Code Completion Guide
Feature Documentation
Getting Started with liblevenshtein-rust
PrefixZipper Usage Guide
Binary Persistence Guide
Dictionary Thread Safety
Formal Verification Architecture
OCaml Extraction Status
Family ABI Invariant Traceability
Formal Verification Findings Ledger
Verification Index
Verification Progress Report
Proof Completion Plan
Levenshtein Verification Proof Index
Formal Verification with Rocq
Formal Verification Gates
Rust Implementation Status
Verification Summary
Formal Verification Improvements
Admitted Lemmas Status Report
Core Verification Library - Completion Summary
Fundamental Discovery: is_valid_trace Allows Duplicate Pairs
Phase 1: change_cost_compose_bound Proof Plan
Phase 1: Witness Uniqueness & Proof Structure - COMPLETE ✅
Phase 4 Completion Summary
Phase 4 Session 1: Witness Lemma Axiomatization & change_cost_compose_bound - COMPLETE ✅
Phase 4 Sessions 1-2: Axiomatization & Trace Composition Cost Bound - COMPLETE ✅
Phase 5: Attempt to Complete All Admitted Lemmas
Phases 2-3: NoDup Lemmas - COMPLETE ✅
Proof Session Logs - Levenshtein Distance Verification
Liblevenshtein Core Verification Library
Automaton Proofs Status
Verification — Core Theories: Automaton
Modular Decomposition Summary
Verification — Core Theories
Formal Verification of Grammar Correction Pipeline
Grammar Correction Verification - Summary
CV Encoding Correctness Proof - COMPLETED
Proof Maintenance Guide for NFA/Phonetic Verification
NFA/Phonetic Regex Layer - Formal Verification
NFA/Phonetic Regex Layer - Formal Specification Summary
Interval-Relaxed MSM Trie Search — Design & Verification
Verification — MSM
Position Skipping Optimization - Formal Verification Summary
Phonetic Position Skipping Proof - Admitted Lemmas Status Report
Axiom 1 Completion Guide: Step-by-Step Instructions
Axiom 1 Critical Analysis: Fundamental Issue Identified
Axiom 1 Proof Strategy: Algorithm Execution Semantics
Axiom 2 Completion Guide: Step-by-Step Instructions
Axiom 2 Final Analysis: Production Readiness with Documented Gap
Axiom 2 Proof Progress Report
Complete Verification Roadmap: From 98.7% to 100%
Coq Verification Completion Status
Coq/Rocq Modular Proof Compilation: Memory Analysis
Current Status: Modular Decomposition
Modular Decomposition Status
Module Renaming & Modularization Cleanup Summary
Position Skipping Optimization: Benchmark Results
Production Rules Analysis for Axiom 2 Completion
Verification — Phonetic
Resource Limiting for Coq/Rocq Compilation
Rule Pair Interaction Matrix (13×13 = 169 pairs)
Verification Session Summary - November 20, 2025
Modular Decomposition - Completion Report
Modular Decomposition - Position Skipping Proof
Position Skipping Proof - Modular Organization
Phonetic Rewrite Rules - Performance Baseline
TLA+ Specifications for liblevenshtein
tlc-results-2026-05-26
tlc-results-2026-05-27
Namespaces
vinary-tree
liblevenshtein
cljdoc
builds & hosts documentation for Clojure/Script libraries
Keyboard shortcuts
Ctrl
+
k
Jump to recent docs
←
Move to previous article
→
Move to next article
Ctrl
+
/
Jump to the search field
Raise an issue
Browse cljdoc source
Chat on Slack
× close