Timeline for Is there a formal notion of what we do when we 'Let X be ...'?
Current License: CC BY-SA 2.5
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 6, 2010 at 8:41 | comment | added | Neel Krishnaswami | @Noam: yes, you're totally right. On reflection there's obviously a tower of exponentials on the order of the cut formula. I don't know what I was thinking. | |
| Apr 6, 2010 at 6:37 | vote | accept | Zavosh | ||
| Apr 5, 2010 at 20:44 | comment | added | Noam Zeilberger | @Neel, side remark: isn't it much worse than doubly-exponential? I thought Statman proved normalization for simply-typed lambda calculus is not elementary recursive. | |
| Apr 5, 2010 at 19:14 | answer | added | Charles Stewart | timeline score: 9 | |
| Apr 5, 2010 at 14:48 | comment | added | François G. Dorais | @Neel: I also think it's a good idea to post the lambda-calculus observation as a partial answer. | |
| Apr 5, 2010 at 14:39 | comment | added | François G. Dorais | @Neel: I'm thinking the gain with definitions is exactly the same as the gain with allowing cuts, both would give the same amount of "compression." Your observation seems to support this. Does this sound right to you or do you see something else happening here? | |
| Apr 5, 2010 at 13:03 | comment | added | Neel Krishnaswami | @FGD: even for just intuitionistic propositional logic there's a doubly-exponential blowup in cut elimination. It seems to me that you need something more subtle than simple cut-elimination to answer this question. This is why I haven't responded to this question, despite the fact that "let x be foo in bar" is exactly the proof term for cut in lambda-calculi. | |
| Apr 5, 2010 at 12:50 | comment | added | François G. Dorais | I changed the tags a bit so that this good question attracts more attention from experts in complexity theory. (I don't think [formal-languages] really applies, but I left it as is.) | |
| Apr 5, 2010 at 12:48 | history | edited | François G. Dorais |
edited tags
|
|
| Apr 5, 2010 at 4:58 | comment | added | François G. Dorais | It's unclear to me that there is a definite gain at the complexity level. In order to use a definition, you must decode it, at least in part. For example, even if "G is a group" is known, you need extra information to know that it has an identity element and the decoding process seems to be just as lengthy as the long description of a group. Perhaps there is some gain in partial decoding, if you only need the fact that G is a monoid, but such gains can be had just with appropriate uses of the cut-rule. This is a good question. I wonder if there is a real gain in the end. | |
| Apr 5, 2010 at 2:34 | history | edited | Zavosh | CC BY-SA 2.5 |
nitpicking over my own wording, not changing content
|
| Apr 5, 2010 at 1:47 | answer | added | abcdxyz | timeline score: 4 | |
| Apr 5, 2010 at 0:57 | answer | added | mathy | timeline score: 3 | |
| Apr 5, 2010 at 0:52 | history | edited | Zavosh | CC BY-SA 2.5 |
got rid of annoying quotes around vague words
|
| Apr 5, 2010 at 0:43 | history | asked | Zavosh | CC BY-SA 2.5 |