Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.word-break

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/word_break.clj1 definitions, 3 theorems

AHoF Word Break (dynamic programming): decide whether a string can be segmented into a sequence of dictionary words -- the core of tokenizers, CJK word segmentation, and URL/identifier splitting. The DP fills breakable[i] = 'the prefix of length i splits into words'; a split point j works when the prefix up to j is itself breakable AND the remaining piece j..i is a dictionary word, and breakable[i] is the OR of all working split points: split-works? prefix-breakable? suffix-is-word? = prefix-breakable? AND suffix-is-word? over booleans. Proved native and axiom-free: the per-split test as the boolean conjunction of a breakable prefix and a dictionary-word suffix (via logic/if-data over Bool); that a split works when both hold; and that it fails when the prefix is not breakable or the suffix is not a word. The scan over split points and the OR-accumulation are executable; what is proved is the per-split success decision. Requires data/Bool, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.word-break` prints this classification.

word-break/split-works? :
  (x₁ x₂ : data/Bool)
  → data/Bool

word-break/split-works-both-hold :
  → boolean/and data/true data/true = data/true

word-break/split-fails-prefix-unbreakable :
  → boolean/and data/false data/true = data/false

word-break/split-fails-suffix-not-word :
  → boolean/and data/true data/false = data/false