反向比特串编码

在学习Programming Language Foundations in Agda第一章Naturals时, 最后有个比特串的反向编码, 觉得也挺有意思的.

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

编码方式, nil是高位方向
1011   => x1 x1 x0 x1 nil
001011 => x1 x1 x0 x1 x0 x0 nil

这种编码方式用来实现inc(加1)比较简单:

inc : Bin → Bin
inc nil = x1 nil
inc (x0 m) = x1 m
inc (x1 m) = x0 (inc m)

思路很简单, 开始遇到的1都变成0, 最后一个0变为1(在这里面就是第一个0).

©著作权归作者所有,转载或内容合作请联系作者
平台声明：文章内容（如有图片或视频亦包括在内）由作者上传并发布，文章内容仅代表作者本人观点，简书系信息发布平台，仅提供信息存储服务。

推荐阅读更多精彩内容