Everything Is Just Functions: 1 week with David Beazley and SICP

(ezzeriesa.notion.site)

389 points kurinikku | 2 comments | 17 Nov 24 15:07 UTC | HN request time: 0.399s | source

Show context

gugagore ◴[17 Nov 24 20:05 UTC] No.42166709[source]▶

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... , along with an unrelated criticism of SICP.

I'd like to better understand what the limitations are of "everything is just a function".

replies(3): >>42168230 #>>42169214 #>>42169475 #

1. schoen ◴[17 Nov 24 23:17 UTC] No.42168230[source]▶

>>42166709 #

I 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.

replies(1): >>42169512 #

2. schoen ◴[18 Nov 24 03:35 UTC] No.42169512[source]▶

>>42168230 (TP) #

Looking 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.

↑