bend-ml-bpe-tokenizer

Releases (4)

• 0.1.3.0 indexed
• 0.1.2.0 unindexed
• 0.1.1.0 unindexed
• 0.1.0.0 unindexed

Definitions (72)

main.bend

• type TkToken: a raw byte (B) or the result of a merge rule, by rule id (M).
• type RuleMerge rule: joins the pair (a, b) into the token M{id}.
• def Tk.eq
• def peekdoes xs start with exactly the pair (a, b)?
• def merge.goReplaces each occurrence (non-overlapping, left to right) of the pair (a, b) with the token c.
• def merge
• def encode.goapplies the rules from the oldest to the newest; `done` keeps the ones already applied (newest first), which is exactly the table that decode needs.
• def encodeThe table goes from the oldest rule to the newest (like merges.txt).
• def hitsis the newest rule in the table the one that creates the token tk?
• def exp.goExpansion of a token into bytes.
• def exp
• def decdecodes with the already reversed table (newest first)
• def decode
• def liftbytes -> initial tokens
• def hasdoes some rule in the table have the id i?
• def knis the token a byte, or was it created by a rule in the table?
• def knl
• def wf.gowell-formed table: no id repeats
• def wf
• type Cnt===================================================================== Training (needs no proof: it generates tables; a table is valid if wf(table)) ===================================================================== --------------------------------------------------------------- training: count adjacent pairs, merge the most frequent one, repeat (tie-break: the first pair that appeared, as in minbpe) ---------------------------------------------------------------
• def same_headis the first Cnt of cs the pair (a, b)?
• def bump.goadds 1 to the counter of the pair (a, b), or creates it at the end of the list
• def bump
• def count.go
• def pick2
• def pick
• def best.go
• def best
• def train.goup to n merges, ids from `next` on; m is the current best pair (best(count(xs)))
• def trainthe table from the oldest rule to the newest
• def BDa type chosen by a Bool: rewriting through it refutes True == False
• def nat_eq_sound
• def nat_eq_refl
• def and_true
• def and_intro
• def or_left
• def or_right
• def not_truenot p is true -> p is false
• def tk_eq_sound
• def ext_mAdding the (new) rule i on top of the table does not change the expansion of a token M{j} that the old table already knows (j != i, because i is new).
• def and_true_l
• def and_true_r
• def ext_tokthe same for any known token (a byte never depends on the table)
• def ext_dec.step
• def ext_decdecoding a list of known tokens does not change when the new rule is added
• def exp_newThe new token M{i} expands to the expansion of a followed by that of b (looking only at the old table D).
• def mp_coreCentral step: in place of a b t we get M{i} followed by m, where m decodes like t.
• def kn_subif x == a and x is known, a is known too
• def mp_falsex stays out of the rewrite: if the rest decodes the same, x <> rest does too
• def mp_hitthe pair is x y: the tokens were equal to a and b
• def mpmerge.go does not change what decode returns (with the new rule on top of the table)
• def kn_monoadding a rule to the table only increases what is known
• def kn_newthe token created by the new rule is known
• def kp
• def enc_knownevery emitted token is known to the complete (reversed) table
• def enc_decapplying all the rules does not change what decode returns
• def lift_decwith no rules, the bytes decode to themselves
• def lift_known
• law roundtripLAW 1 (roundtrip): with a well-formed table (all rule ids distinct), decoding what was encoded returns the original bytes.
• law vocab_boundLAW 2 (vocabulary): every token emitted by encode is a raw byte or was created by one of the table's rules; an unknown id never appears.
• law dec_appendLAW 3 (concatenation): decoding two token lists together is decoding each one and joining the bytes.
• def lt_succn < 1 + n
• def lt_nej < i -> i != j
• def lt_upj < i -> j < 1 + i
• def belowall ids in the rule list are smaller than i
• def below_has
• def below_up
• def below_consadding the rule with id `next` (greater than all those in `done`) keeps the table "below 1+next"
• def below_freshnot (has D i) when all the ids in D are smaller than i
• def twtrain.go generates rules with ids next, next+1, ...: none repeats, whatever the corpus
• law train_wfLAW (train_wf): the table that train returns is always well formed, so the roundtrip holds for it
• law roundtrip_trainedLAW 5 (roundtrip_trained): train a table on any corpus, with as many merges as you like: decoding what it encodes always returns the original bytes.