Compact bit encoding schemes for simply-typed lambda-terms

Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
EditorsEijiro Sumii, Jacques Garrigue, Gabriele Keller
PublisherAssociation for Computing Machinery, Inc
Pages146-157
Number of pages12
ISBN (Print)9781450342193
DOIs
Publication statusPublished - 2016 Aug 4
Event21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016 - Nara, Japan
Duration: 2016 Sep 182016 Sep 24

Publication series

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

Other

Other21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016
CountryJapan
CityNara
Period16/9/1816/9/24

Keywords

  • Bit encoding
  • Data compression
  • Simply-typed λ-calculus

ASJC Scopus subject areas

  • Software
  • Computer Science Applications
  • Computational Theory and Mathematics

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

Cite this