The lambda calculus

What Hacker News says

1. erwanNov 2018
   Here's a short-list:

   - Calculating space by Konrad Zuse (See: https://news.ycombinator.com/item?id=18325689)

   - The Annotated Turing by Charles Petzlod

   - Introduction to Lambda Calculus by H. Barendregt (do the exercises/proofs)

   - Propositions as Types by Philip Wadler

   - Part III. of Languages and Machines by Thomas Sudkamp

   Show morethread
2. dill_dayJul 2013
   I guess it must be a joke, but that's a fun review. "I accidently bought this book thinking I was buying a traditional calculus book in order to prepare for a standardized test I had to take. After a few chapters I realized this was no ordinary Calculus book."

   Anyway, there is a reprint available now for $25 http://www.amazon.com/The-Lambda-Calculus-Syntax-Semantics/d...

   thread
3. sbDec 2012
   Nice article (the Stanford Encyclopedia of Philosophy has many more, btw.), but I like the "Introduction to Lambda Calculus" by Henk Barendregt (one of the people working in Lambda calculus, see for instance the citation to his book "The Lambda Calculus: Its syntax and semantics." in the references), which has the added benefit of being free:

   http://www.cse.chalmers.se/research/group/logic/TypesSS05/Ex... (also covers typed lambda calculus AFAIR)

   Show morethread
4. sbDec 2011
   Queinnec's Lisp in Small Pieces is a superb book, if you liked that you might also like Henderson's book on implementation of functional PLs (particularly SECD machines.)

   Regarding the list: I think it's a nice effort, but lacks several excellent and remarkable books. Just quickly browsing, I found the following essential books missing:

     * In algorithms: 
       - Aho, Hopcroft, Ullman: The Design and Analysis of Algorithms.
       - Wirth: Algorithms and Data Structures.
     * In Compilers:
       - Wirth: Compiler Construction.
       - Grune, Bal, Jacobs, Cerial: Modern Compiler Design.
       - Muchnick: Advanced Compiler Design and Implementation.
     * In Lambda calculus:
       - Barendregt: Introduction to Lambda Calculus.
     * In theoretical computer science:
       - Kozen: Automata and Computability.
       - Davis: Computability and Unsolvability.
     * In concepts of PLs:
       - Turbak, Gifford, Sheldon: Design Concepts in Programming Languages.
   

   (In general, the list does not mention any of Wirth's books, which is a shame. The Project Oberon book should also be mentioned in OS stuff, I guess...)

   Regarding compiler construction: As has been previously mentioned several times on HN, Cooper's and Torczon's "Engineering a Compiler" is a more recent and (IMHO much more readable and accessible) choice.

   Show morethread
5. sbJan 2011
   While this is a nice article on compiling to lambda calculus, the uninitiated might find Barendregt's "Introduction to Lambda Calculus" (ftp://ftp.cs.ru.nl/pub/CompMath.Found/lambda.pdf) an invaluable resource. (IMHO, it's the best work for groking lambda calculus, at least it was for me and my learning prefernece/style)
   thread
6. groovy2shoesAug 2016
   Your intuition that Clojure's macro system is unhygienic are correct.

   Hygiene in this context was coined by Henk Barendregt in the context of the lambda calculus:

   > For reasons of hygiene, it will always be assumed that the bound variables that occur in a certain expression are different from the free ones. [0]

   This may seem nonsensical at first, but consider two different functions, f(x) and g(x): although both f and g take an x, they are in fact different variables. So, if some expression has x free, and another has x bound, and one is substituted into the other, you must remember to differentiate between the two homonyms. One way to do this is to consistently rename one or both variables so that they no longer appear to be the same, but it's important not to get too hung up on the concept of renaming per se, because the only requirement is that they be regarded as different (Andre van Tonder's delightful implementation of syntax-case uses a painting algorithm rather than a renaming one, but the net effect is the same).

   In the case of syntactic transformers (macros), we're not concerned about the variables of the transformer itself, but rather the variables of the transformed code. Consider that full macro expansion occurs as a sequence of single expansions (transcription steps) until no further expansion can be done. Now, a macro is hygienic if all identifiers introduced during any given transcription step are unique to that transcription step (regardless of name). The introduced identifiers are analogized with bound variables while all other identifiers are analogized with free variables, just like how a lambda abstraction introduces its parameter variable.

   Note that even unhygienic macro systems are capable of expressing at least some hygienic macros: macros that do not introduce any identifiers are trivially hygienic. I contend that the explicit-renaming macro system is not actually hygienic, even though it allows you to write any hygienic macro. The reason being that, in essence, hygienic macro expansion is precisely the notion of lexical scoping applied to syntactic transformation; and just as we don't need to manually specify the scope of each variable in our basis language, we should not need to do so in our meta language. For the same reason, Clojure's requirement to gensym identifiers -- while it offers convenient shorthand for the operation, it is still explicit (and it solves only one of the two problems of unhygienic expansion, namely variable capture, while providing no protection from shadowing). In that vein, syntax-rules, syntax-case, and implicit-renaming macros all fit the bill.

   Just as dynamically-scoped variables can come in handy sometimes even in a lexically-scoped language (many Lisps have them, variously called "fluid variables", "special variables", or "parameters"), unhygienic injection of identifiers can come in handy sometimes (the classic example being anaphoric macros). The traditional way to do this is to simply circumvent, or "break", hygiene for a particular identifier, but Eli Barzilay and crew have also come up with the notion of "syntactic parameters" analogous to dynamically-scoped variables.

   [0]: Henk Barendregt, "Introduction to the Lambda Calculus".

   Show morethread