main.bend checks

raw source on the hub · import bend-ml-bpe-tokenizer@0.1.0.0/main.bend as Main

bend-ml-bpe-tokenizer: BPE byte-level com roundtrip provado.

import bend-ml-bpe-tokenizer@0.1.0.0/main.bend as BPE

Um token é um byte cru (B{n}) ou o resultado de uma regra de merge (M{id}). A tabela é uma lista de regras da mais antiga para a mais nova, como o merges.txt do GPT-2: a regra de id k junta o par (a, b) no token M{k}. encode aplica as regras em ordem; decode expande cada token de volta para bytes. As leis estão no fim do arquivo, cada uma com sua prova.

Como ler as provas: uma prova em Bend é uma função cujo TIPO é a afirmação. match faz análise de casos, a chamada recursiva é a hipótese de indução, %e : P reescreve o objetivo com a igualdade e, {==} fecha quando os dois lados já são o mesmo termo. +x marca uma variável que pode ser usada mais de uma vez.

2 imports

import Base
import bend-ml-nat-lemmas@0.1.0.0/main.bend as NL

Laws

law roundtrip provedsource · line 514 · raw

@+table:List<&2, Rule> -> @+bs:List<&2, Nat> -> @+w:{True{} == wf(table) : Bool} -> {decode(table, encode(table, lift(bs))) == bs : List<&2, Nat>}

LEI 1 (roundtrip): com uma tabela bem formada (ids de regra todos diferentes), decodificar o que foi codificado devolve os bytes originais.

law vocab_bound provedsource · line 525 · raw

@+table:List<&2, Rule> -> @+bs:List<&2, Nat> -> @+w:{True{} == wf(table) : Bool} -> {True{} == knl(List.reverse(&2, Rule, table), encode(table, lift(bs))) : Bool}

LEI 2 (vocabulário): todo token emitido por encode é um byte cru ou foi criado por uma das regras da tabela; nunca aparece um id desconhecido.

law dec_append provedsource · line 536 · raw

@+D:List<&2, Rule> -> @xs:List<&2, Tk> -> @+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>}

LEI 3 (concatenação): decodificar duas listas de tokens juntas é decodificar cada uma e juntar os bytes.

Types

type Tk source · line 21 · raw

Data

Token: um byte cru (B) ou o resultado de uma regra de merge, pelo id da regra (M).

B
```
@n:Nat -> Tk
```
M
```
@k:Nat -> Tk
```

type Rule source · line 26 · raw

Data

Regra de merge: junta o par (a, b) no token M{id}.

Rule
```
@id:Nat -> @a:Tk -> @b:Tk -> Rule
```

type Cnt source · line 177 · raw

Data

===================================================================== Treino (não precisa de prova: gera tabelas; a tabela vale se wf(table)) ===================================================================== --------------------------------------------------------------- treino: conta pares adjacentes, funde o mais frequente, repete (desempate: o primeiro par que apareceu, como no minbpe) ---------------------------------------------------------------

Cnt
```
@a:Tk -> @b:Tk -> @n:Nat -> Cnt
```

Definitions

def Tk.eq source · line 29 · raw

@+x:Tk -> @+y:Tk -> Bool

def peek source · line 41 · raw

@+a:Tk -> @+b:Tk -> @xs:List<&2, Tk> -> Bool

o início de xs é exatamente o par (a, b)?

def merge.go source · line 55 · raw

@xs:List<&2, Tk> -> @hit:Bool -> @+a:Tk -> @+b:Tk -> @+c:Tk -> List<&2, Tk>

Troca cada ocorrência (não sobreposta, da esquerda para a direita) do par (a, b) pelo token c. hit é sempre peek(a, b, xs): o chamador calcula, porque um match só abre parâmetros.

def merge source · line 66 · raw

@+a:Tk -> @+b:Tk -> @+c:Tk -> @+xs:List<&2, Tk> -> List<&2, Tk>

def encode.go source · line 71 · raw

@todo:List<&2, Rule> -> @done:List<&2, Rule> -> @xs:List<&2, Tk> -> List<&2, Tk>

aplica as regras da mais antiga para a mais nova; done guarda as já aplicadas (a mais nova primeiro), que é exatamente a tabela que o decode precisa.

def encode source · line 81 · raw

@+table:List<&2, Rule> -> @xs:List<&2, Tk> -> List<&2, Tk>

A tabela vem da regra mais antiga para a mais nova (como o merges.txt).

def hits source · line 85 · raw

@table:List<&2, Rule> -> @+tk:Tk -> Bool

a regra mais nova da tabela é a que cria o token tk?

def exp.go source · line 99 · raw

@table:List<&2, Rule> -> @hit:Bool -> @tk:Tk -> List<&2, Nat>

Expansão de um token em bytes. A tabela tem a regra mais nova primeiro e uma regra só se refere a tokens mais antigos, então expandir a e b olha apenas o resto da tabela. hit é sempre hits(table, tk).

def exp source · line 112 · raw

@+table:List<&2, Rule> -> @+tk:Tk -> List<&2, Nat>

def dec source · line 116 · raw

@+table:List<&2, Rule> -> @ids:List<&2, Tk> -> List<&2, Nat>

decodifica com a tabela já invertida (mais nova primeiro)

def decode source · line 123 · raw

@+table:List<&2, Rule> -> @ids:List<&2, Tk> -> List<&2, Nat>

def lift source · line 127 · raw

@bs:List<&2, Nat> -> List<&2, Tk>

bytes -> tokens iniciais

def has source · line 137 · raw

@+D:List<&2, Rule> -> @+i:Nat -> Bool

alguma regra da tabela tem o id i?

def kn source · line 145 · raw

@+D:List<&2, Rule> -> @tk:Tk -> Bool

o token é um byte, ou foi criado por uma regra da tabela?

def knl source · line 152 · raw

@+D:List<&2, Rule> -> @xs:List<&2, Tk> -> Bool

def wf.go source · line 160 · raw

@todo:List<&2, Rule> -> @+done:List<&2, Rule> -> Bool

tabela bem formada: nenhum id se repete

def wf source · line 167 · raw

@table:List<&2, Rule> -> Bool

def same_head source · line 181 · raw

@cs:List<&2, Cnt> -> @+a:Tk -> @+b:Tk -> Bool

o primeiro Cnt de cs é o par (a, b)?

def bump.go source · line 189 · raw

@cs:List<&2, Cnt> -> @hit:Bool -> @+a:Tk -> @+b:Tk -> List<&2, Cnt>

soma 1 ao contador do par (a, b), ou o cria no fim da lista

def bump source · line 198 · raw

@+cs:List<&2, Cnt> -> @+a:Tk -> @+b:Tk -> List<&2, Cnt>

def count.go source · line 201 · raw

@xs:List<&2, Tk> -> @cs:List<&2, Cnt> -> List<&2, Cnt>

def pick2 source · line 212 · raw

@better:Bool -> @c:Cnt -> @cur:Cnt -> Cnt

def pick source · line 219 · raw

@c:Cnt -> @cur:Cnt -> Cnt

def best.go source · line 224 · raw

@cs:List<&2, Cnt> -> @cur:Cnt -> Cnt

def best source · line 231 · raw

@cs:List<&2, Cnt> -> Maybe<&1, Cnt>

def train.go source · line 239 · raw

@n:Nat -> @+next:Nat -> @+xs:List<&2, Tk> -> @m:Maybe<&1, Cnt> -> List<&2, Rule>

até n fusões, ids a partir de next; m é o melhor par atual (best(count(xs)))

def train source · line 250 · raw

@n:Nat -> @+next:Nat -> @+xs:List<&2, Tk> -> List<&2, Rule>

a tabela da regra mais antiga para a mais nova

def BD source · line 258 · raw

@b:Bool -> @t:Type -> @f:Type -> Type

um tipo escolhido por um Bool: reescrever através dele refuta True == False

def nat_eq_sound source · line 265 · raw

@a:Nat -> @b:Nat -> @e:{True{} == Nat.is_eq(a, b) : Bool} -> {a == b : Nat}

def nat_eq_refl source · line 279 · raw

@a:Nat -> {True{} == Nat.is_eq(a, a) : Bool}

def and_true source · line 286 · raw

@p:Bool -> @q:Bool -> @e:{True{} == Bool.and(p, q) : Bool} -> Pair({True{} == p : Bool}, {True{} == q : Bool})

def and_intro source · line 294 · raw

@p:Bool -> @q:Bool -> @ep:{True{} == p : Bool} -> @eq:{True{} == q : Bool} -> {True{} == Bool.and(p, q) : Bool}

def or_left source · line 302 · raw

@p:Bool -> @q:Bool -> @ep:{True{} == p : Bool} -> {True{} == Bool.or(p, q) : Bool}

def or_right source · line 310 · raw

@p:Bool -> @q:Bool -> @eq:{True{} == q : Bool} -> {True{} == Bool.or(p, q) : Bool}

def not_true source · line 318 · raw

@p:Bool -> @e:{True{} == Bool.not(p) : Bool} -> {False{} == p : Bool}

not p é verdadeiro -> p é falso

def tk_eq_sound source · line 326 · raw

@+x:Tk -> @+y:Tk -> @e:{True{} == Tk.eq(x, y) : Bool} -> {x == y : Tk}

def ext_m source · line 343 · raw

@+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>}

Acrescentar a regra i (nova) ao topo da tabela não muda a expansão de um token M{j} que a tabela antiga já conhece (j != i, porque i é novo).

def and_true_l source · line 357 · raw

@p:Bool -> @q:Bool -> @e:{True{} == Bool.and(p, q) : Bool} -> {True{} == p : Bool}

def and_true_r source · line 365 · raw

@p:Bool -> @q:Bool -> @e:{True{} == Bool.and(p, q) : Bool} -> {True{} == q : Bool}

def ext_tok source · line 374 · raw

@+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>}

o mesmo para qualquer token conhecido (um byte nunca depende da tabela)

def ext_dec.step source · line 383 · raw

@+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>}

def ext_dec source · line 389 · raw

@+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>}

decodificar uma lista de tokens conhecidos não muda ao acrescentar a regra nova

def exp_new source · line 398 · raw

@+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>}

O token novo M{i} expande para a expansão de a seguida da de b (olhando só a tabela antiga D).

def mp_core source · line 410 · raw

@+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>}

Passo central: no lugar de a b t aparece M{i} seguido de m, onde m decodifica como t. Os dois lados decodificam igual porque M{i} expande para exp(a) ++ exp(b).

def kn_sub source · line 418 · raw

@+D:List<&2, Rule> -> @+x:Tk -> @+a:Tk -> @ex:{x == a : Tk} -> @kx:{True{} == kn(D, x) : Bool} -> {True{} == kn(D, a) : Bool}

se x == a e x é conhecido, a também é

def mp_false source · line 423 · raw

@+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>}

x fica de fora do rewrite: se o resto decodifica igual, x <> resto também

def mp_hit source · line 428 · raw

@+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>}

o par é x y: os tokens eram iguais a a e b

def mp source · line 434 · raw

@+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>}

merge.go não muda o que o decode devolve (com a regra nova no topo da tabela)

def kn_mono source · line 449 · raw

@+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}

acrescentar uma regra à tabela só aumenta o que é conhecido

def kn_new source · line 457 · raw

@+D:List<&2, Rule> -> @+i:Nat -> @+a:Tk -> @+b:Tk -> {True{} == kn(Rule{i, a, b} <> D, M{i}) : Bool}

o token criado pela regra nova é conhecido

def kp source · line 460 · raw

@+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}

def enc_known source · line 475 · raw

@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}

todo token emitido é conhecido pela tabela completa (invertida)

def enc_dec source · line 483 · raw

@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>}

aplicar todas as regras não muda o que o decode devolve

def lift_dec source · line 493 · raw

@bs:List<&2, Nat> -> {dec([], lift(bs)) == bs : List<&2, Nat>}

sem regras, os bytes decodificam para eles mesmos

def lift_known source · line 501 · raw

@bs:List<&2, Nat> -> {True{} == knl([], lift(bs)) : Bool}