Compact bit encoding schemes for simply-typed lambda-terms
Compact bit encoding schemes for simply-typed lambda-terms
复制标题
简单类型 lambda 项的紧凑位编码方案
DOI：
10.1145/2951913.2951918
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Shinohara Ayumi
中科院分区：
文献类型：
--
作者：
Takeda Kotaro;Kobayashi Naoki;Yaguchi Kazuya;Shinohara Ayumi
我们考虑如何将简单类型的λ项紧凑地编码成位串的问题。这项工作的动机是Kobayashi等人最近在高阶数据压缩方面的工作，其中数据被编码为生成它们的函数程序（或λ项）。为了利用其良好的压缩能力，压缩方案必须提供一种将λ项紧凑地编码为位串的方法。为此，我们提出了两种基于类型的位编码方案；第一种是使用类型信息将λ项编码为符号序列，然后应用算术编码将该序列转换为位字符串。第二个更复杂；我们准备了一个上下文无关语法（CFG），它只描述类型良好的术语，然后使用专门用于CFG的算术编码的变体。我们已经实现了这两种方案，并证实它们通常比以前的λ项位编码方案输出更紧凑的代码。
We consider the problem of how to compactly encode simply-typed λ-terms into bit strings. The work has been motivated by Kobayashi et al.’s recent work on higher-order data compression, where data are encoded as functional programs (or, λ-terms) that generate them. To exploit its good compression power, the compression scheme has to come with a method for compactly encoding the λ-terms into bit strings. To this end, we propose two type-based bit-encoding schemes; the first one encodes a λ-term into a sequence of symbols by using type information, and then applies arithmetic coding to convert the sequence to a bit string. The second one is more sophisticated; we prepare a context-free grammar (CFG) that describes only well-typed terms, and then use a variation of arithmetic coding specialized for the CFG. We have implemented both schemes and confirmed that they often output more compact codes than previous bit encoding schemes for λ-terms.