= 27d567bc2d48d9f40e9ccc20ea370b15)
Vladimir_Nesov comments on Sense, Denotation and Semantics - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (12)
Okay, I just tried to read through the thing, and it looks much too difficult for what it's trying to do. If anyone's really interested in the topic, I'd recommend starting with something like the Wikipedia page for System F and assimilating more material as needed; that'll certainly be easier for any programmer like me.
If the goal is good understanding of "foundations" (however Girard himself may mock the concept), I see the book as being at just the right level.
I slogged through the first 30 pages. Section 2.2.1 "Interpretation of the rules" was surprisingly unclear. I could make sense of it only after using the Curry-Howard isomorphism given later on (because I'm already familiar with typed functional programming).
Section 3.3 on "arbitrary pluggings" and "variables and values as dual aspects of the same plugging phenomenon" is both informal and unclear.
I also didn't see any definition of "abstraction", "closed", or "strictly simpler" in the corollary (p. 19) in section 3.4 on (head) normal form. "B strictly simpler (type) than A" probably means that A is built on top of B by one of:
The material is either not self-contained, or out of order (I didn't read the whole thing).
The book assumes a bit of familiarity with the subject and isn't bureaucratic in formality. Many ideas are hard to present formally or aren't even understood formally yet. I find the informal discussion in this book very valuable. It allows to see the motivation behind logic beyond text-crunching right from the beginning.
A closed term is one where all variables are bound (no free variables). Abstraction is a lambda-expression.