4 ms·
I recently came across the notion that you need inductive data types (and can't just use Church encodings) if you want to do theorem proving, like proving that
by gugagore 2y ago
I recently came across the notion that you need inductive data types (and can't just use Church encodings) if you want to do theorem proving, like proving that `0 != 1`.
I threw up some content up here: https://intellec7.notion.site/Drinking-SICP-hatorade-and-why-you-need-inductive-data-types-14121476bd0a8083b96ee8bc36a3bd94 https://intellec7.notion.site/Drinking-SICP-hatorade-and-why... , along with an unrelated criticism of SICP.
I'd like to better understand what the limitations are of "everything is just a function".
- schoen 2y agoI think you could prove 0 ≠ 1 if you had some other concrete fact about inequality to make use of. You could reason from the theorem "f = g -> f x = g x" to create your inequality fact on the right side and then take the contrapositive. It seems correct to me that you can't directly prove inequality between Church numerals without starting with some other fact about inequality. Whereas with inductive data types, a proof system can directly "observe" the equality or inequality of two concrete instances of the same inductive type, by recursively removing the outermost constructor application from each instance.
- schoen 2y agoLooking at the linked references, I'm not sure what else is being assumed to be available or not available when considering proofs using the Church numerals. I guess that will matter a lot, and I don't know enough to make more general statements about what is or isn't sufficient here.
- gugagore 2y agofixed link: https://goosetaco.notion.site/Drinking-SICP-hatorade-and-why-you-need-inductive-data-types-14121476bd0a8083b96ee8bc36a3bd94 https://goosetaco.notion.site/Drinking-SICP-hatorade-and-why...
- solomonb 2y agoWell for theorem proving you need Sigma and Pi types plus some notion of equality. Can you achieve those with Scott or Church encoding?