law vocab_bound

bend-ml-bpe-tokenizer@0.1.3.0 · main.bend:525

import Base

525# LAW 2 (vocabulary): every token emitted by encode is a raw byte or was
526# created by one of the table's rules; an unknown id never appears.
527law vocab_bound:
528  for +table: List<&2, Rule>
529  for +bs: List<&2, Nat>
530  for +w: {True{} == wf(table) : Bool}
531  {True{} == knl(List.reverse(&2, Rule, table), encode(table, lift(bs))) : Bool}