src/tree.bend

bend-lawful-stdlib@0.1.0.0 · 70 lines · 6 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/class.bend as C
3
4# tree.bend: binary trees reduced with parallel calls.
5#
6#   import ./tree.bend as Tree
7#   Tree.reduce(~Nat, ~Nat.add_sg(), t)
8#
9# reduce evaluates the two halves of each Fork with a parallel call. The
10# law reduce_foldr says that for any C.Semigroup, reduce gives the same
11# result as Base's List.foldr over the leaves in order. It needs no
12# identity element, because a tree always has a leaf.
13#
14# Not yet measured: the speedup of reduce on the CPU, and any run on the
15# GPU.
16
17type Tree<-A: Data> is Data:
18  Tip{x: A}
19  Fork{l: Tree<A>, r: Tree<A>}
20
21def reduce(~A: Data, ~m: C.Semigroup<A>, t: Tree<A>) -> A:
22  match t:
23    case Tip{x}:
24      x
25    case Fork{l, r}:
26      a b = reduce(~A, ~m, l) reduce(~A, ~m, r)
27      C.Semigroup.op(A, m, a, b)
28
29# the leaves, left to right, in front of acc
30def to_list.go(-A: Data, t: Tree<A>, acc: List<&2, A>) -> List<&2, A>:
31  match t:
32    case Tip{x}:
33      x <> acc
34    case Fork{l, r}:
35      to_list.go(A, l, to_list.go(A, r, acc))
36
37def to_list(-A: Data, t: Tree<A>) -> List<&2, A>:
38  to_list.go(A, t, Nil{})
39
40# a balanced tree with 2^d leaves f(lo), f(lo+1), ..., so both halves of
41# each parallel call do the same amount of work
42def build(~A: Data, ~f: Nat -> A, +d: Nat, +lo: Nat) -> Tree<A>:
43  match d:
44    case 0n:
45      Tip{f(lo)}
46    case 1n+p:
47      l r = build(~A, ~f, p, lo) build(~A, ~f, p, Nat.add(lo, Nat.pow(2n, p)))
48      Fork{l, r}
49
50# reduce agrees with foldr. With acc = Nil{}:
51# {op(reduce(t), z) == foldr(to_list(t), z)}.
52law reduce_foldr:
53  for ~A: Data
54  for ~m: C.Semigroup<A>
55  for t: Tree<A>
56  for +acc: List<&2, A>
57  for +z: A
58  {C.Semigroup.op(A, m, reduce(~A, ~m, t), List.foldr(~&2, ~A, ~A, ~C.Semigroup.fn(~A, ~m), acc, z)) == List.foldr(~&2, ~A, ~A, ~C.Semigroup.fn(~A, ~m), to_list.go(A, t, acc), z) : A}
59
60def reduce_foldr(A, m, t, acc, z):
61  match t:
62    case Tip{x}:
63      {==}
64    case Fork{+l, +r}:
65      -fz = List.foldr(~&2, ~A, ~A, ~C.Semigroup.fn(~A, ~m), acc, z)
66      -g = C.Semigroup.op(A, m, C.Semigroup.op(A, m, reduce(~A, ~m, l), reduce(~A, ~m, r)), fz)
67      %reduce_foldr(~A, ~m, l, to_list.go(A, r, acc), z) : {g == _ : A}
68      %reduce_foldr(~A, ~m, r, acc, z) : {g == C.Semigroup.op(A, m, reduce(~A, ~m, l), _) : A}
69      Equal.sym(A, C.Semigroup.op(A, m, reduce(~A, ~m, l), C.Semigroup.op(A, m, reduce(~A, ~m, r), fz)), g,
70        C.Semigroup.assoc(A, m, reduce(~A, ~m, l), reduce(~A, ~m, r), List.foldr(~&2, ~A, ~A, ~C.Semigroup.fn(~A, ~m), acc, z)))