Compact bit encoding schemes for simply-typed lambda-terms
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016),
, pp.146-157
(2016), [peer-reviewed]
Event Date:
September 18-22, 2016
Abstract / 概要
We consider the problem of how to compactly encode simply-typed $\lambda$-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, $\lambda$-terms) that generate them. To exploit its good compression power, the compression scheme has to come with a method for compactly encoding the $\lambda$-terms into bit strings. To this end, we propose two type-based bit-encoding schemes; the first one encodes a $\lambda$-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 $\lambda$-terms.