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.
Mon 19 Sep
|17:00 - 17:25|
Kotaro TakedaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan, Kazuya YaguchiTohoku University, Japan, Ayumi ShinoharaTohoku University, JapanDOI
|17:25 - 17:50|
Shin-Cheng MuAcademia Sinica, Taiwan, Yu-Hsi ChiangNational Taiwan University, Taiwan, Yu-Han LyuDartmouth College, USADOI
|17:50 - 18:15|
Jan ChristiansenFlensburg University of Applied Sciences, Germany, Nikita DanilenkoUniversity of Kiel, Germany, Sandra DylusUniversity of Kiel, GermanyDOI