Toronto-based reading group that meets weekly to read computer science books and papers.
Currently reading: The Little Typer
Hey everyone! Friday night we discussed Classical Logic (13 PFPL) in a decidedly non-classical way. It was a somewhat surprising and mind bending to treat the same old logic statements we know and love in a very different way, thanks Harper!
Next week we will meet on Friday at 6:30pm at Bento Miso to cover Chapter 14 of PFPL, Generic Programming.
Sorry for the hiatus on recaps, Im hoping to fill in a couple of summary notes sections for chapters 10-12 rather than try to do catch up recaps.
Chapters 12 and 13 of PFPL discuss logic systems and how to construct a logic grammar using the same principles used earlier in the book. Chapter 12 uses the constructivist approach, “Only that which is proven is true”; whereas chapter 13 uses classical logic which is the common one taught in school, “all statements are either true or false”. These may seem the same at first but in constructivist logic equating truth with having a proof in hand gives rise to statements being “undecided” which isn’t possible in classical logic. This in turn lays the groundwork for the propositions as types principle in which there is an isomorphism between programs and proofs.
The classical logic section aims to replicate the mechanics of the normal logic operators you learn in school; i.e. and, or, not, if - then; by building a logic grammar following the same principles used to build the constructivist logic grammar in chapter 12. The symmetry between truth and falsehood seems to give rise to a more complex set of grammar rules and more complex programs than in the constructivist logic. Harper later claims that the classical logic is weaker than constructivist logic and equates this with the concept that sometimes when adding new features to a language they may actually weaken the language. We were undecided ourselves on whether we agree with that or not.
We went over a variety of examples of writing programs to prove logic statements in constructivist logic, but when we tried to do the same in the classical formulation we found it significantly more challenging. As all proofs in must be built upon an absurdity (I.e. True is false), it requires jumping back and forth between refutations of statements and proofs of statements and these are composed to construct a program. This seemed decidedly less intuitive than when using the constructivist approach, though it may just need more practice.
Looking forward to next week! Scott