Timeline for Is functional programming a branch of mathematics?
Current License: CC BY-SA 2.5
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 20, 2010 at 9:18 | comment | added | Charles Stewart | Accept: I'm not convinced, but you have certainly given me something to think about, and I guess new readers should have the benefit of reading this before the other comments. | |
| Jan 20, 2010 at 9:17 | vote | accept | Charles Stewart | ||
| Jan 20, 2010 at 9:14 | comment | added | Charles Stewart | Omega rules aren't syntax! I'm not sure whether they can be functional programming, either. Can you give me a ref (Zeilberger is less taxing than Girard): I'd like to think this through for myself. | |
| Jan 19, 2010 at 11:12 | comment | added | Neel Krishnaswami | If you use an omega-rule for list elimination, then bubble sort and merge sort will have the same canonical form. (The necessary infinitary syntax can be represented either in a higher-order fashion, the way Noam Zeilberger does it, or coinductively, the way Girard does in Ludics.) | |
| Jan 19, 2010 at 9:38 | comment | added | Charles Stewart | You can have a monad that specifies the intended computational meaning of a function. Then regular functions of the lambda calculus become denotationally determined, operationally underspecified programs. I'd be surprised, though, if you could fix things so that bubblesort and mergesort are both computational realisations of some underdetermined lambda expression. | |
| Jan 17, 2010 at 9:52 | vote | accept | Charles Stewart | ||
| Jan 17, 2010 at 9:52 | |||||
| Jan 16, 2010 at 15:48 | comment | added | Neel Krishnaswami | The same function can have wildly (eg, arbitrary towers of exponentials) different runtimes under different evaluation orders. Since even intensional MLTT is consistent with any evaluation order, I don't think the operational properties of purely functional programs have a type-theoretic/logical reading, yet. | |
| Jan 16, 2010 at 14:24 | comment | added | Charles Stewart | "Bubble sort and merge sort are the same function under the lens of beta-eta equality" - Not so fast! Even after you have figured out the right algebraic treatment of program state, and have proved that both will give the same outputs on every input, you will still only have proven propositional equality: beta-eta equality is normally something else in intensional type theory. | |
| Jan 16, 2010 at 10:11 | history | answered | Neel Krishnaswami | CC BY-SA 2.5 |