bend-ml-bpe-tokenizer Releases (4): 0.1.3.0 0x559a0abb492a951db15be435191b6d0a indexed https://jend.leeeet.dev/files.txt?path=bend-ml-bpe-tokenizer@0.1.3.0 0.1.2.0 0xa071a92aabcffe6fc04dc3a60f0096ba unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-bpe-tokenizer@0.1.2.0 0.1.1.0 0xbce52aed55d81f3c75dfd6518c9bcbdd unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-bpe-tokenizer@0.1.1.0 0.1.0.0 0x3333bd5274f4ce66fdf8fe0c26c6b532 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-bpe-tokenizer@0.1.0.0 Definitions (72): BendMlBpeTokenizer.Tk (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=Tk) # Token: a raw byte (B) or the result of a merge rule, by rule id (M). type Tk is Data: B{n: Nat} M{k: Nat} BendMlBpeTokenizer.Rule (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=Rule) # Merge rule: joins the pair (a, b) into the token M{id}. type Rule is Data: Rule{id: Nat, a: Tk, b: Tk} BendMlBpeTokenizer.Tk.eq (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=Tk.eq) def Tk.eq(+x: Tk, +y: Tk) -> Bool: BendMlBpeTokenizer.peek (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=peek) # does xs start with exactly the pair (a, b)? def peek(+a: Tk, +b: Tk, xs: List<&2, Tk>) -> Bool: BendMlBpeTokenizer.merge.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=merge.go) # Replaces each occurrence (non-overlapping, left to right) of the pair # (a, b) with the token c. `hit` is always `peek(a, b, xs)`: the caller computes it, # because a match can only open parameters. def merge.go(xs: List<&2, Tk>, hit: Bool, +a: Tk, +b: Tk, +c: Tk) -> List<&2, Tk>: BendMlBpeTokenizer.merge (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=merge) def merge(+a: Tk, +b: Tk, +c: Tk, +xs: List<&2, Tk>) -> List<&2, Tk>: BendMlBpeTokenizer.encode.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=encode.go) # applies the rules from the oldest to the newest; `done` keeps the ones already applied # (newest first), which is exactly the table that decode needs. Only the proofs read it, so it # is erased (`-done`): the checker keeps it and the compiled program never builds it. Building # it cost half of the time to encode (found by Mathews Fernando's bend-lint, dead_accumulator). def encode.go(todo: List<&2, Rule>, -done: List<&2, Rule>, xs: List<&2, Tk>) -> List<&2, Tk>: BendMlBpeTokenizer.encode (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=encode) # The table goes from the oldest rule to the newest (like merges.txt). def encode(+table: List<&2, Rule>, xs: List<&2, Tk>) -> List<&2, Tk>: BendMlBpeTokenizer.hits (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=hits) # is the newest rule in the table the one that creates the token tk? def hits(table: List<&2, Rule>, +tk: Tk) -> Bool: BendMlBpeTokenizer.exp.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=exp.go) # Expansion of a token into bytes. The table has the newest rule first and # a rule only refers to older tokens, so expanding a and b looks only at # the rest of the table. `hit` is always `hits(table, tk)`. def exp.go(table: List<&2, Rule>, hit: Bool, tk: Tk) -> List<&2, Nat>: BendMlBpeTokenizer.exp (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=exp) def exp(+table: List<&2, Rule>, +tk: Tk) -> List<&2, Nat>: BendMlBpeTokenizer.dec (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=dec) # decodes with the already reversed table (newest first) def dec(+table: List<&2, Rule>, ids: List<&2, Tk>) -> List<&2, Nat>: BendMlBpeTokenizer.decode (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=decode) def decode(+table: List<&2, Rule>, ids: List<&2, Tk>) -> List<&2, Nat>: BendMlBpeTokenizer.lift (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=lift) # bytes -> initial tokens def lift(bs: List<&2, Nat>) -> List<&2, Tk>: BendMlBpeTokenizer.has (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=has) # does some rule in the table have the id i? def has(+D: List<&2, Rule>, +i: Nat) -> Bool: BendMlBpeTokenizer.kn (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=kn) # is the token a byte, or was it created by a rule in the table? def kn(+D: List<&2, Rule>, tk: Tk) -> Bool: BendMlBpeTokenizer.knl (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=knl) def knl(+D: List<&2, Rule>, xs: List<&2, Tk>) -> Bool: BendMlBpeTokenizer.wf.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=wf.go) # well-formed table: no id repeats def wf.go(todo: List<&2, Rule>, +done: List<&2, Rule>) -> Bool: BendMlBpeTokenizer.wf (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=wf) def wf(table: List<&2, Rule>) -> Bool: BendMlBpeTokenizer.Cnt (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=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) # --------------------------------------------------------------- type Cnt is Data: Cnt{a: Tk, b: Tk, n: Nat} BendMlBpeTokenizer.same_head (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=same_head) # is the first Cnt of cs the pair (a, b)? def same_head(cs: List<&2, Cnt>, +a: Tk, +b: Tk) -> Bool: BendMlBpeTokenizer.bump.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=bump.go) # adds 1 to the counter of the pair (a, b), or creates it at the end of the list def bump.go(cs: List<&2, Cnt>, hit: Bool, +a: Tk, +b: Tk) -> List<&2, Cnt>: BendMlBpeTokenizer.bump (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=bump) def bump(+cs: List<&2, Cnt>, +a: Tk, +b: Tk) -> List<&2, Cnt>: BendMlBpeTokenizer.count.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=count.go) def count.go(xs: List<&2, Tk>, cs: List<&2, Cnt>) -> List<&2, Cnt>: BendMlBpeTokenizer.pick2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=pick2) def pick2(better: Bool, c: Cnt, cur: Cnt) -> Cnt: BendMlBpeTokenizer.pick (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=pick) def pick(c: Cnt, cur: Cnt) -> Cnt: BendMlBpeTokenizer.best.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=best.go) def best.go(cs: List<&2, Cnt>, cur: Cnt) -> Cnt: BendMlBpeTokenizer.best (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=best) def best(cs: List<&2, Cnt>) -> Maybe<&1, Cnt>: BendMlBpeTokenizer.train.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=train.go) # up to n merges, ids from `next` on; m is the current best pair (best(count(xs))) def train.go(n: Nat, +next: Nat, +xs: List<&2, Tk>, m: Maybe<&1, Cnt>) -> List<&2, Rule>: BendMlBpeTokenizer.train (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=train) # the table from the oldest rule to the newest def train(n: Nat, +next: Nat, +xs: List<&2, Tk>) -> List<&2, Rule>: BendMlBpeTokenizer.BD (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=BD) # a type chosen by a Bool: rewriting through it refutes True == False def BD(b: Bool, t: Type, f: Type) -> Type: BendMlBpeTokenizer.nat_eq_sound (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=nat_eq_sound) def nat_eq_sound(a: Nat, b: Nat, e: {True{} == Nat.is_eq(a, b) : Bool}) -> {a == b : Nat}: BendMlBpeTokenizer.nat_eq_refl (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=nat_eq_refl) def nat_eq_refl(a: Nat) -> {True{} == Nat.is_eq(a, a) : Bool}: BendMlBpeTokenizer.and_true (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=and_true) def and_true(p: Bool, q: Bool, e: {True{} == Bool.and(p, q) : Bool}) -> {True{} == p : Bool} & {True{} == q : Bool}: BendMlBpeTokenizer.and_intro (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=and_intro) def and_intro(p: Bool, q: Bool, ep: {True{} == p : Bool}, eq: {True{} == q : Bool}) -> {True{} == Bool.and(p, q) : Bool}: BendMlBpeTokenizer.or_left (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=or_left) def or_left(p: Bool, q: Bool, ep: {True{} == p : Bool}) -> {True{} == Bool.or(p, q) : Bool}: BendMlBpeTokenizer.or_right (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=or_right) def or_right(p: Bool, q: Bool, eq: {True{} == q : Bool}) -> {True{} == Bool.or(p, q) : Bool}: BendMlBpeTokenizer.not_true (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=not_true) # not p is true -> p is false def not_true(p: Bool, e: {True{} == Bool.not(p) : Bool}) -> {False{} == p : Bool}: BendMlBpeTokenizer.tk_eq_sound (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=tk_eq_sound) def tk_eq_sound(+x: Tk, +y: Tk, e: {True{} == Tk.eq(x, y) : Bool}) -> {x == y : Tk}: BendMlBpeTokenizer.ext_m (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=ext_m) # Adding 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 ext_m(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, +j: Nat, h: Bool, eh: {h == Nat.is_eq(i, j) : Bool}, nf: {True{} == Bool.not(has(D, i)) : Bool}, kt: {True{} == has(D, j) : Bool}) -> {exp(Rule{i, a, b} <> D, M{j}) == exp(D, M{j}) : List<&2, Nat>}: BendMlBpeTokenizer.and_true_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=and_true_l) def and_true_l(p: Bool, q: Bool, e: {True{} == Bool.and(p, q) : Bool}) -> {True{} == p : Bool}: BendMlBpeTokenizer.and_true_r (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=and_true_r) def and_true_r(p: Bool, q: Bool, e: {True{} == Bool.and(p, q) : Bool}) -> {True{} == q : Bool}: BendMlBpeTokenizer.ext_tok (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=ext_tok) # the same for any known token (a byte never depends on the table) def ext_tok(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, t: Tk, kt: {True{} == kn(D, t) : Bool}, nf: {True{} == Bool.not(has(D, i)) : Bool}) -> {exp(Rule{i, a, b} <> D, t) == exp(D, t) : List<&2, Nat>}: BendMlBpeTokenizer.ext_dec.step (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=ext_dec.step) def ext_dec.step(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, +x: Tk, +t: List<&2, Tk>, k1: {True{} == kn(D, x) : Bool}, nf: {True{} == Bool.not(has(D, i)) : Bool}, ih: {dec(Rule{i, a, b} <> D, t) == dec(D, t) : List<&2, Nat>}) -> {dec(Rule{i, a, b} <> D, x <> t) == dec(D, x <> t) : List<&2, Nat>}: BendMlBpeTokenizer.ext_dec (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=ext_dec) # decoding a list of known tokens does not change when the new rule is added def ext_dec(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, xs: List<&2, Tk>, +kx: {True{} == knl(D, xs) : Bool}, +nf: {True{} == Bool.not(has(D, i)) : Bool}) -> {dec(Rule{i, a, b} <> D, xs) == dec(D, xs) : List<&2, Nat>}: BendMlBpeTokenizer.exp_new (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=exp_new) # The new token M{i} expands to the expansion of a followed by that of b # (looking only at the old table D). def exp_new(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, h: Bool, eh: {h == Nat.is_eq(i, i) : Bool}) -> {exp(Rule{i, a, b} <> D, M{i}) == List.append(&2, Nat, exp(D, a), exp(D, b)) : List<&2, Nat>}: BendMlBpeTokenizer.mp_core (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=mp_core) # Central step: in place of a b t we get M{i} followed by m, where m decodes # like t. Both sides decode the same because M{i} expands to exp(a) ++ exp(b). def mp_core(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, +t: List<&2, Tk>, +m: List<&2, Tk>, ka: {True{} == kn(D, a) : Bool}, kb: {True{} == kn(D, b) : Bool}, +nf: {True{} == Bool.not(has(D, i)) : Bool}, ihm: {dec(Rule{i, a, b} <> D, m) == dec(Rule{i, a, b} <> D, t) : List<&2, Nat>}) -> {dec(Rule{i, a, b} <> D, M{i} <> m) == dec(Rule{i, a, b} <> D, a <> b <> t) : List<&2, Nat>}: BendMlBpeTokenizer.kn_sub (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=kn_sub) # if x == a and x is known, a is known too def kn_sub(+D: List<&2, Rule>, +x: Tk, +a: Tk, ex: {x == a : Tk}, kx: {True{} == kn(D, x) : Bool}) -> {True{} == kn(D, a) : Bool}: BendMlBpeTokenizer.mp_false (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=mp_false) # x stays out of the rewrite: if the rest decodes the same, x <> rest does too def mp_false(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, +x: Tk, +t: List<&2, Tk>, +mg: List<&2, Tk>, ih: {dec(Rule{i, a, b} <> D, mg) == dec(Rule{i, a, b} <> D, t) : List<&2, Nat>}) -> {dec(Rule{i, a, b} <> D, x <> mg) == dec(Rule{i, a, b} <> D, x <> t) : List<&2, Nat>}: BendMlBpeTokenizer.mp_hit (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=mp_hit) # the pair is x y: the tokens were equal to a and b def mp_hit(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, +x: Tk, +y: Tk, +t: List<&2, Tk>, +m: List<&2, Tk>, +ex: {x == a : Tk}, +ey: {y == b : Tk}, +kxx: {True{} == kn(D, x) : Bool}, +kyy: {True{} == kn(D, y) : Bool}, +nf: {True{} == Bool.not(has(D, i)) : Bool}, ihm: {dec(Rule{i, a, b} <> D, m) == dec(Rule{i, a, b} <> D, t) : List<&2, Nat>}) -> {dec(Rule{i, a, b} <> D, M{i} <> m) == dec(Rule{i, a, b} <> D, x <> y <> t) : List<&2, Nat>}: BendMlBpeTokenizer.mp (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=mp) # merge.go does not change what decode returns (with the new rule on top of the table) def mp(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, xs: List<&2, Tk>, hit: Bool, +eh: {hit == peek(a, b, xs) : Bool}, +kx: {True{} == knl(D, xs) : Bool}, +nf: {True{} == Bool.not(has(D, i)) : Bool}) -> {dec(Rule{i, a, b} <> D, merge.go(xs, hit, a, b, M{i})) == dec(Rule{i, a, b} <> D, xs) : List<&2, Nat>}: BendMlBpeTokenizer.kn_mono (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=kn_mono) # adding a rule to the table only increases what is known def kn_mono(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, t: Tk, kt: {True{} == kn(D, t) : Bool}) -> {True{} == kn(Rule{i, a, b} <> D, t) : Bool}: BendMlBpeTokenizer.kn_new (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=kn_new) # the token created by the new rule is known def kn_new(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk) -> {True{} == kn(Rule{i, a, b} <> D, M{i}) : Bool}: BendMlBpeTokenizer.kp (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=kp) def kp(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, xs: List<&2, Tk>, hit: Bool, +eh: {hit == peek(a, b, xs) : Bool}, +kx: {True{} == knl(D, xs) : Bool}) -> {True{} == knl(Rule{i, a, b} <> D, merge.go(xs, hit, a, b, M{i})) : Bool}: BendMlBpeTokenizer.enc_known (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=enc_known) # every emitted token is known to the complete (reversed) table def enc_known(todo: List<&2, Rule>, +done: List<&2, Rule>, +xs: List<&2, Tk>, +wfe: {True{} == wf.go(todo, done) : Bool}, +kx: {True{} == knl(done, xs) : Bool}) -> {True{} == knl(List.reverse.go(&2, Rule, todo, done), encode.go(todo, done, xs)) : Bool}: BendMlBpeTokenizer.enc_dec (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=enc_dec) # applying all the rules does not change what decode returns def enc_dec(todo: List<&2, Rule>, +done: List<&2, Rule>, +xs: List<&2, Tk>, +wfe: {True{} == wf.go(todo, done) : Bool}, +kx: {True{} == knl(done, xs) : Bool}) -> {dec(List.reverse.go(&2, Rule, todo, done), encode.go(todo, done, xs)) == dec(done, xs) : List<&2, Nat>}: BendMlBpeTokenizer.lift_dec (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=lift_dec) # with no rules, the bytes decode to themselves def lift_dec(bs: List<&2, Nat>) -> {dec(Nil{}, lift(bs)) == bs : List<&2, Nat>}: BendMlBpeTokenizer.lift_known (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=lift_known) def lift_known(bs: List<&2, Nat>) -> {True{} == knl(Nil{}, lift(bs)) : Bool}: BendMlBpeTokenizer.roundtrip (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=roundtrip) # LAW 1 (roundtrip): with a well-formed table (all rule ids # distinct), decoding what was encoded returns the original bytes. law roundtrip: for +table: List<&2, Rule> for +bs: List<&2, Nat> for +w: {True{} == wf(table) : Bool} {decode(table, encode(table, lift(bs))) == bs : List<&2, Nat>} BendMlBpeTokenizer.vocab_bound (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=vocab_bound) # LAW 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 vocab_bound: for +table: List<&2, Rule> for +bs: List<&2, Nat> for +w: {True{} == wf(table) : Bool} {True{} == knl(List.reverse(&2, Rule, table), encode(table, lift(bs))) : Bool} BendMlBpeTokenizer.dec_append (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=dec_append) # LAW 3 (concatenation): decoding two token lists together is decoding # each one and joining the bytes. law dec_append: for +D: List<&2, Rule> for xs: List<&2, Tk> for +ys: List<&2, Tk> {dec(D, List.append(&2, Tk, xs, ys)) == List.append(&2, Nat, dec(D, xs), dec(D, ys)) : List<&2, Nat>} BendMlBpeTokenizer.lt_succ (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=lt_succ) # n < 1 + n def lt_succ(n: Nat) -> {True{} == Nat.is_lt(n, 1n+n) : Bool}: BendMlBpeTokenizer.lt_ne (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=lt_ne) # j < i -> i != j def lt_ne(j: Nat, i: Nat, e: {True{} == Nat.is_lt(j, i) : Bool}) -> {False{} == Nat.is_eq(i, j) : Bool}: BendMlBpeTokenizer.lt_up (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=lt_up) # j < i -> j < 1 + i def lt_up(j: Nat, i: Nat, e: {True{} == Nat.is_lt(j, i) : Bool}) -> {True{} == Nat.is_lt(j, 1n+i) : Bool}: BendMlBpeTokenizer.below (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=below) # all ids in the rule list are smaller than i def below(D: List<&2, Rule>, +i: Nat) -> Bool: BendMlBpeTokenizer.below_has (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=below_has) def below_has(D: List<&2, Rule>, +i: Nat, +e: {True{} == below(D, i) : Bool}) -> {False{} == has(D, i) : Bool}: BendMlBpeTokenizer.below_up (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=below_up) def below_up(D: List<&2, Rule>, +i: Nat, +e: {True{} == below(D, i) : Bool}) -> {True{} == below(D, 1n+i) : Bool}: BendMlBpeTokenizer.below_cons (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=below_cons) # adding the rule with id `next` (greater than all those in `done`) keeps the table "below 1+next" def below_cons(+a: Tk, +b: Tk, +D: List<&2, Rule>, +i: Nat, +e: {True{} == below(D, i) : Bool}) -> {True{} == below(Rule{i, a, b} <> D, 1n+i) : Bool}: BendMlBpeTokenizer.below_fresh (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=below_fresh) # not (has D i) when all the ids in D are smaller than i def below_fresh(+D: List<&2, Rule>, +i: Nat, +e: {True{} == below(D, i) : Bool}) -> {True{} == Bool.not(has(D, i)) : Bool}: BendMlBpeTokenizer.tw (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=tw) # train.go generates rules with ids next, next+1, ...: none repeats, whatever the corpus def tw(n: Nat, +next: Nat, +xs: List<&2, Tk>, m: Maybe<&1, Cnt>, +done: List<&2, Rule>, +bl: {True{} == below(done, next) : Bool}) -> {True{} == wf.go(train.go(n, next, xs, m), done) : Bool}: BendMlBpeTokenizer.train_wf (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=train_wf) # LAW (train_wf): the table that train returns is always well formed, so the roundtrip holds for it law train_wf: for n: Nat for +next: Nat for +xs: List<&2, Tk> {True{} == wf(train(n, next, xs)) : Bool} BendMlBpeTokenizer.roundtrip_trained (https://jend.leeeet.dev/definition.txt?path=bend-ml-bpe-tokenizer@0.1.3.0/main.bend&name=roundtrip_trained) # LAW 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. No hypothesis at all. law roundtrip_trained: for +n: Nat for +corpus: List<&2, Nat> for +bs: List<&2, Nat> {decode(train(n, 0n, lift(corpus)), encode(train(n, 0n, lift(corpus)), lift(bs))) == bs : List<&2, Nat>}