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 -