Functional programs as compressed data

Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi

Research output: Contribution to journalArticlepeer-review

10 Citations (Scopus)


We propose an application of programming language techniques to lossless data compression, where tree data are compressed as functional programs that generate them. This “functional programs as compressed data” approach has several advantages. First, it follows from the standard argument of Kolmogorov complexity that the size of compressed data can be optimal up to an additive constant. Secondly, a compression algorithm is clean: it is just a sequence of β-expansions (i.e., the inverse of β-reductions) for λ-terms. Thirdly, one can use program verification and transformation techniques (higher-order model checking, in particular) to apply certain operations on data without decompression. In this article, we present algorithms for data compression and manipulation based on the approach, and prove their correctness. We also report preliminary experiments on prototype data compression/transformation systems.

Original languageEnglish
Pages (from-to)39-84
Number of pages46
JournalHigher-Order and Symbolic Computation
Issue number1
Publication statusPublished - 2012 Mar


  • Data compression
  • Functional programs
  • Higher-order Model Checking
  • Program transformation
  • Semantics based program manipulation

ASJC Scopus subject areas

  • Software
  • Computer Science Applications


Dive into the research topics of 'Functional programs as compressed data'. Together they form a unique fingerprint.

Cite this