Tire Table 函数式数组的一种表示法

作为一个刚接触函数式编程的新人，说实话在数据结构这个问题上确实给我带来了非常多的困扰。这两天借着假期正好在读software foundation. 其中第三卷正好提到了这种数据结构，感觉挺有意思的

才学疏浅，只是在这里转记一下书上的东西。这里所有的东西都来自于s f中的vfa卷!

xH : 问题引入

思考如下程序

collisions=0;
  for (i=0; i<2N; I++)
     a[i]=0;
  for (j=0; j<N; j++) {
     i = input[j];
     if (a[i] != 0)
       collisions++;
     a[i]=1;
  }
  return collisions;

这里如果使用常见的命令式编程语言，时间复杂度很明显是 O(n), 两个一层的循环。但是这种程序复杂度的分析太粗了。。。。在大多数的函数式的编程语言中， 我们通常是没有数组这个数据结构的，大多数时候我们只能使用类似链表的map结构（key是index）来表示这里面查询这一步也会引入一个O(n)的开销，这显然是严重拖慢了程序的执行

针对这样的情况，常见函数式语言可以做出如下的常见调整

• 在函数式编程语言语法级别上去引入一些可变的数据结构， 其代表做法是SML, OCaml之类的语言中在语法级别上支持类c数组。是的，这种做法非常的不清真！更加糟糕的是如果我们希望用一些 被严格证明安全的数据结构（Verified functional datastructure） 就会遇到比较大的困难。这时候需要引入霍尔逻辑（Hoare Logic ）。
• 熟悉 Haskell的同学肯定会想到使用IO Monad, 这个完全OK, 抽时间我也记一下吧～～～
• 接受这种速度的损失，当然O(n)的损失确实过大， 考虑使用红黑树代替链表可以把这种带查询的结构优化到O(log(n))

但是上述的讨论过程中我们只考虑了结构本身的问题， 实际上Int之类的东西操作的时候还是会有常数级别的开销的， 在一些函数式编程语言，特别 是我们做形式化验证的过程中这个可能会变得不可忽略。

xO xH: 极端情况

考虑如下的函数式程序

Fixpoint loop (input: list nat) (c: nat) (table: total_map bool) : nat :=
  match input with
  | nil ⇒ c
  | a::al ⇒ if table a
                  then loop al (c+1) table
                  else loop al c (t_update table a true)
 end.
Definition collisions (input: list nat) : nat :=
       loop input 0 (t_empty false).

首先和之前分析的一样，没有任何优化，直接使用list (这里的total map是一个类似放着kv映射关系的list)，其本身的时间复杂度退化到O(n^2)。
是吗？
不，情况远比你想的糟糕， 首先因为Nat 这个类型使用的是 Peano表示的方式，之前我有记过这个表示法。这意味着map查找中比较数组下标的这个操作只有平均O(N)速度！整体的时间复杂度甚至到达了 O(n^3).

xI xH： 尝试使用更加高效的数字表示法

学算法的时候一种很常见对比较的优化方式是二分，这里显然是很容易用上的，既然原来用list一样的Peano表示法

0:    o
1:    S o
2:    S S 0

那么转为二叉树类似的表示复杂度就会立刻下降

o:  
leaf
1: 
        A
    /       \
Leaf.       Leaf 

2:
                A
            /       \
           A         Leaf
        /     \
      Leaf    Leaf

3:
                A
            /       \
           A           A
        /     \     /    \
      Leaf    Leaf Leaf  Leaf

......

本来对于两个数字线性的比较一旦把数字用一颗完全二叉树来表示那么时间复杂度立马就下降到 O(log(N)) 了。
很好有了想法，接下来只要给出规则，定义这种表示就可以了，更何况自然数有奇偶性，它天生就是二分的！

定义语法

Inductive positive : Set :=
  | xI : positive → positive
  | xO : positive → positive
  | xH : positive.

定义语义

Fixpoint positive2nat (p: positive) : nat :=
  match p with
  | xI q ⇒ 1 + 2 * positive2nat q
  | xO q ⇒ 0 + 2 * positive2nat q
  | xH ⇒ 1
 end.

我们先不考虑0的表示吧， 先表达正数好了，毕竟对于数组下标这样的场景来说是完全ok的。xH代表了 1 ，xO n表达了所有的非0偶数(2 * n), oI n表达了非1奇数(2 * n + 1)

其实这个表达初看确实是挺费脑子的，简单的写几个吧，二叉树的图我就不画了

1
xH

2 = 2 * 1
xO xH

3 = 2 * 1 + 1
xI xH

4 = 2 * 2
xO (xO xH)

5 = 2 * 2 + 1
xI (xO xH)

10 = 2 * 5 
xO (xI (xO xH))

嘛如果是一个一个写下去还是挺好写的吧～～

xO xO xH: 改进时间复杂度到 N * N * LogN

ok,有了上述的这种全新的正整数的表示方法，只要替换一下就可以啦 easy

Definition total_mapz (A: Type) := Z → A.
Definition empty {A:Type} (default: A) : total_mapz A := fun _ ⇒ default.
Definition update {A:Type} (m : total_mapz A)
                    (x : Z) (v : A) :=
  fun x' ⇒ if Z.eqb x x' then v else m x'.

Fixpoint loop (input: list Z) (c: Z) (table: total_mapz bool) : Z :=
  match input with
  | nil ⇒ c
  | a::al ⇒ if table a
                  then loop al (c+1) table
                  else loop al c (update table a true)
 end.

这里直接使用了Coq标准库内置的类似正整数的数据结构，不过这里面已经扩展到整数了，基本的原理是没有差的

xI xO xH: 更快！ N * LogN * LogN

其实看到logN很明显接下来的优化还是和二分的想法有关。之前说了红黑树这样的平衡树是可以带来查询性能优化的。现在这种类似链表的结构显然是不能满足的，但是用Key 加上 Value的形式做成的函数式 Tree Map还是复杂了， 有没有一种简洁的数据结构？

学习字符串算法的时候，大家肯定是已经接触过Trie这个数据结构了，这种对字符串公共前缀进行优化的方法也可以被放到我们index的表达中，我们的index说白了就3个基本符号， 如果写成字符串的形式不同的字符串可以拥有大量的公共串！先看看Trie的图吧

image.png

图片是百度来的百度百科

简单的说，Trie这个数据结构是一种用符号来标记边（或者节点）查找时，在后继节点中寻找下一个字符的公共结构，本质非常类似一个自动机，或者说一棵AST。
我们之前提到的二分的index显然是可以转化成这样的一颗二叉Trie的因为我们这里的字符的可能性就三种。一种比较直接的想法就是，用向左子树中搜索下一个字符来表示 xO, 用向右子树中搜索下一个（二分表示的数字中）字符来表示xI.

很好，这样我们只需要在生成的数字index构成的trie的节点上放开一个用来存放值的结构（一个函数就可以啦，类似map）

code如下

Inductive trie (A : Type) :=
    | Leaf : trie A
    | Node : trie A → A → trie A → trie A.
Arguments Leaf {A}.
Arguments Node {A} _ _ _.
Definition trie_table (A: Type) : Type := (A * trie A)%type.
Definition empty {A: Type} (default: A) : trie_table A :=
      (default, Leaf).
Fixpoint look {A: Type} (default: A) (i: positive) (m: trie A): A :=
    match m with
    | Leaf ⇒ default
    | Node l x r ⇒
        match I with
        | xH ⇒ x
        | xO i' ⇒ look default i' l
        | xI i' ⇒ look default i' r
        end
    end.
Definition lookup {A: Type} (i: positive) (t: trie_table A) : A :=
   look (fst t) i (snd t).
Fixpoint ins {A: Type} default (i: positive) (a: A) (m: trie A): trie A :=
    match m with
    | Leaf ⇒
        match I with
        | xH ⇒ Node Leaf a Leaf
        | xO i' ⇒ Node (ins default i' a Leaf) default Leaf
        | xI i' ⇒ Node Leaf default (ins default i' a Leaf)
        end
    | Node l o r ⇒
        match I with
        | xH ⇒ Node l a r
        | xO i' ⇒ Node (ins default i' a l) o r
        | xI i' ⇒ Node l o (ins default i' a r)
        end
    end.
Definition insert {A: Type} (i: positive) (a: A) (t: trie_table A)
                 : trie_table A :=
  (fst t, ins (fst t) i a (snd t)).

嘛可以试试画画一颗插入了3号和10号元素的树

image.png

ok!!!!
不过其实关于这种Trie Table的性质特别是不变量窝还没搞明白。。。。。所以最重要的验证和证明暂且不写了s a d.......