Compact bit encoding schemes for simply-Typed lambda-Terms

Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish
Pages (from-to)146-157
Number of pages12
JournalACM SIGPLAN Notices
Issue number9
Publication statusPublished - 2016 Sep 4


  • Bit encoding
  • Data compression
  • Simply-Typed lambda-calculus

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'Compact bit encoding schemes for simply-Typed lambda-Terms'. Together they form a unique fingerprint.

Cite this