Combinatory Compression of Given Proofs

INTRO.

Explanation of the Table Columns

Each row represents properties of a proof of the indicated problem. The problems are from the TPTPCD2 corpus. The considered proofs were obtained with SGCD and CCS in different configurations. For some problems no proof was available and for others sevaral proofs with the same least size of the CL compression obtained by different configurations.

For each proof we consider:

• Its source proof, a D-term.
• Its compressed grammar, obtained via CDTools with TreeRePair from the source proof. TreeRePair was called with -optimize edges.
• Its CL compression obtained from the compressed grammar with CDTools. Options were lambda_optim=2 and simp=red. The method follows Simon Peyton Jones: The Implementation of Functional Programming Languages, 1987.

The compacted object size (tree object size, object height, resp.) of a D-term is its compacted size (tree size, height, resp.) after replacing all maximal subterms whose leaves are only combinators with decicated constants.

Problem

The proven TPTP problem.

Rating

Problem rating according to latest value of the Rating field in TPTP 7.5.0.

Min C

Minimal compacted size of a proof of the problem. Highlighted numbers indicate absolutely ascertained minimal values, the other values refer to values that are just minimal in the underlying set of considered proofs.

CL: CO

Compacted object size of the CL compression. Values are highlighted as follows: Smaller than the value of Min C. The hyperlink leads to a graph representation of the proof.

CL: CO/HO/TO

Dimensions of the CL compression: compacted object size, tree object size, and object height.

D: C/H/T

Dimensions of the source proof: compacted size, tree size and height.

G: Rank

Rank of the compressed grammar, i.e., the maximal numbers of parameters of a nonterminal.

G: Size

Size of the compressed grammar, i.e., the sum of the number of edges on the right hand sides of its productions.

G: Src

Size of the source grammar before compression. This is twice the compacted size of the source proof.

Combinators

Maximal subterms of the CL compression in which all leaves are combinators. B₄, C₄ are called B*, C' in Peyton Jones: The Implementation of Functional Programming Languages, 1987. B" represents BB.

SGCD-T

The source proof was output by SGCD in configuration SGCD-T, which is based on enumeration by tree size and outputs proofs after the first one only if the object tree size of its CL compression is strictly smaller than that of the previous proofs.

SGCD-H

The source proof was output by SGCD in configuration SGCD-H, which is similar to SGCD-T but based on enumeration by height.

SGCD-P

The source proof was output by SGCD in configuration SGCD-P, which is similar to SGCD-T but based a form of enumeration that combines subproofs of a given proof.

CCS-C

The source proof was output by CCS in configuration CCS-C, which is similar to SGCD-T but based on enumeration by compacted size.

Other

The proof was found in earlier experiments by SGCD or CCS. Such proofs are only considered if they have a strictly smaller CL translation then all proofs by the other configurations or the problem could not be solved at all by the other configurations.