Timeline for natural metrics for proof length
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 14, 2020 at 15:08 | comment | added | Jacques Carette | @user One problem with using a coding of the lambda calculus is that 'coding' arithmetic is usually very inefficient, even from the point of view program length. Adding binary-coded naturals makes some programs exponentially shorter. So Kolmogorov-short programs will inevitably end up re-inventing such things for brevity. | |
| Aug 13, 2020 at 19:34 | comment | added | user76284 | I think the binary lambda calculus could play that role. Indeed it was invented for that reason (concrete AIT). | |
| Aug 13, 2020 at 13:16 | comment | added | Jacques Carette | @user76284 That would be because when analysing DFAs, etc, there is a fixed and adequate meta-language in which length is measured. There is a kind of shift that happens as the computing power gets larger, and some things become undecidable. Size becomes an unstable measure. | |
| Aug 12, 2020 at 19:41 | comment | added | user76284 | “Without it, length becomes a rather whimsical notion.” I don’t think that’s true. Take the problems of minimizing DFAs, NFAs, and regular expressions, which are certainly valid problems that are studied in the literature. | |
| Aug 12, 2020 at 13:00 | history | answered | Jacques Carette | CC BY-SA 4.0 |