Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.cyk

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

AHoF CYK Algorithm (Cocke-Younger-Kasami): decide whether a string is generated by a context-free grammar in Chomsky Normal Form, in O(n^3 * |G|), by dynamic programming over substrings. A cell for a span holds the nonterminals that derive it; a rule A -> B C lets A derive a span when it splits into a left part derived by B and a right part derived by C: rule-applies? left-has-B? right-has-C? = left-has-B? AND right-has-C? over booleans. Proved native and axiom-free: the rule-application test as the boolean conjunction of the two subspan memberships (via logic/if-data over Bool); that a rule applies when both parts are derivable; that it does NOT apply when the left part lacks B; and that it does not apply when the right part lacks C. The span iteration and cell union over all split points and rules are executable; what is proved is the per-split rule-application decision (a full parse accepts when the start symbol reaches the whole-string cell). 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.cyk` prints this classification.

cyk/rule-applies? :
  (x₁ x₂ : data/Bool)
  → data/Bool

cyk/rule-applies-both-derivable :
  → cyk/rule-applies? data/true data/true = data/true

cyk/rule-fails-left-missing :
  → cyk/rule-applies? data/false data/true = data/false

cyk/rule-fails-right-missing :
  → cyk/rule-applies? data/true data/false = data/false