TY - GEN

T1 - Functional programs as compressed data

AU - Kobayashi, Naoki

AU - Matsuda, Kazutaka

AU - Shinohara, Ayumi

PY - 2012

Y1 - 2012

N2 - 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 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 the paper, 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.

AB - 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 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 the paper, 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.

KW - Algorithms

KW - Theory

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

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

U2 - 10.1145/2103746.2103770

DO - 10.1145/2103746.2103770

M3 - Conference contribution

AN - SCOPUS:84857859953

SN - 9781450311182

T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

SP - 121

EP - 130

BT - POPL

PB - Association for Computing Machinery

T2 - ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, PEPM'12, Co-located with POPL 2012

Y2 - 23 January 2012 through 24 January 2012

ER -