TY - GEN

T1 - Compact bit encoding schemes for simply-typed lambda-terms

AU - Takeda, Kotaro

AU - Kobayashi, Naoki

AU - Yaguchi, Kazuya

AU - Shinohara, Ayumi

N1 - Publisher Copyright:
© 2016 ACM.

PY - 2016/8/4

Y1 - 2016/8/4

N2 - 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 bitencoding 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.

AB - 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 bitencoding 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.

KW - Bit encoding

KW - Data compression

KW - Simply-typed λ-calculus

UR - http://www.scopus.com/inward/record.url?scp=85054963797&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85054963797&partnerID=8YFLogxK

U2 - 10.1145/2951913.2951918

DO - 10.1145/2951913.2951918

M3 - Conference contribution

AN - SCOPUS:85054963797

SN - 9781450342193

T3 - ICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

SP - 146

EP - 157

BT - ICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

A2 - Sumii, Eijiro

A2 - Garrigue, Jacques

A2 - Keller, Gabriele

PB - Association for Computing Machinery, Inc

T2 - 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016

Y2 - 18 September 2016 through 24 September 2016

ER -