Recommendation: do the math-y sections in HTDP. This will give you a flavor of the kind of mathematics you get in SICP, even though there are non-overlapping examples in each. I would especially focus on the examples from calculus (numeric differentiation, integration, taylor series etc) but the graph traversal (network flow) things are good for you too. Once you are at east with those, you can tackle SICP and get through fast
–Matthias
(via PLT)
The formal semantics of R6RS are described using PLT Redex. I don’t understand this field of study or where to start so I asked about it on the PLT discussion list and Robby replied here:
Start by reading the introduction to the formal semantics. Then download it and look at the README file (there are some examples in there to get you going).
If you’re interested in learning more about the style of semantics, as background on the R6 semantics, you can start with the redex web site and ask questions here. There is a book that should be coming out in a few months that might also be helpful.
— Robby
Jos also explained here:
Redex is a tool that allows:
1: the description of the grammar of a language
2: the description of how an expression of that language is to be reduced to the value of that expression (reduction relation)
3: after having done steps 1 and 2, redex (in casu procedures traces and apply-reduction-relation) can show you how an expression is reduced to its value.
Although Redex is far more general than just a tool to play with Lambda Calculus (LC) and Combinatory Logic (CL), my path was the following:
0: Imperative programming.
1: The Little LISPer, which is a great primer before glancing into 4. (about recursion, not really a book about programming, imho)
2: Greg Michaelson, An Introduction to Functional Programming through Lambda Calculus (not a masterpiece, but easy to read)
3: Playing with Scheme (particularly preparing lots of interpreters.
4: 1984. The Lambda Calculus, Its Syntax and Semantics, Vol. 103 in Studies in Logic and the Foundations of Mathematics. North-Holland. ISBN 0-444-87508-5. Not easy but very comprehensive.
5: SICP (transformation to continuatian passing style and storage passing style)
6: Redex, which allows me to check my understanding of LC and CL.
You can regard LC and CL as the ultimate mathematical abstractions of programming languages. In fact LC consists of the ultimate lambda and applications only, nothing else. CL goes even further. It has applications only, no lambda, just a few primitive functions (possibly only one) Yet CL and LC can be proven to incorporate all “definable functions”. These are not programming languages for practical use, They are formal mathematical systems of outraging beauty. If you want to make working programs, you’d better not follow my path, I think.
LC is an important piece of mathematics for the formal study of the properties of real life programming languages. It is used extensively in scientific studies on real life programming languages. Scheme can rather easily be described with mathematical precision in terms of LC. IIRC Algol60 has been described in terms of LC too. As an example, the semantical description of Scheme-R6RS is based on knowledge based on LC.
— Jos
In this post; Ryan explains why unhygienic macros inside of unhygienic macros are often difficult.
;; the working if-it & when-it
(define-syntax (if-it stx)
(syntax-case stx ()
((if-it test? then else)
(with-syntax ((it (datum->syntax #'if-it 'it)))
#'(let ((it test?))
(if it then else))))))
(define-syntax (when-it stx)
(syntax-case stx ()
((~ test? exp exp2 ...)
(with-syntax ((it (datum->syntax #'~ 'it)))
#'(let ((it test?)) (when it exp exp2 ...))))))
;; the non-working cond-it
(define-syntax (cond-it stx)
(syntax-case stx (else)
((cond-it (else exp exp2 ...))
#'(begin exp exp2 ...))
((cond-it (test? exp exp2 ...))
#'(when-it test? exp exp2 ...))
((cond-it (test? exp exp2 ...) cond1 cond2 ...)
#'(if-it test? (begin exp exp2 ...)
(cond-it cond1 cond2 ...)))))
When ‘cond-it’ expands and produces an ‘if-it’ expression, the ‘if-it’ is marked by the macro expander as coming from a macro. That means its lexical context is different from the ‘it’ variables in the branches. That means that the ‘it’ variable binding produced by ‘if-it’ does not capture the ‘it’ references in the branches.
— Ryan
Functional Java is an open source library that aims to prepare the Java programming language for the inclusion of closures. It also serves as a platform for learning functional programming concepts by introducing these concepts using a familiar language. The library is intended for use in production applications and is thoroughly tested using the technique of automated specification-based testing with ScalaCheck.
(via PLT)
…you won’t believe it but by reaching part VI, you have mastered a significant chunk of mathematics that you would have never considered within reach had I told you at the outset of your studies that you’d understand rudimentary concepts from “higher” algebra (advanced college material).
— Matthias Felleisen
(via PLT)
The package is intended as a supplement to any standard logic text or for use by anyone who wants to learn the language of first order logic. The main body of the book contains a collection of exericses which use the Tarski’s World software to teach the language and semantics of first order logic. The Tarski’s World application allows the evaluation of first-order sentences within blocks world which users may construct using a simple editor. The worlds consist of collections of blocks of varying sizes and shapes, and placed on a checkerboard. We use an interpreted first-order language which allows users to write sentences about these worlds and evaluate their truth. A Henkin-Hintikka game may be used to elucidate the evaluation procedure.
Via PLT, where a few folks shared that this package is quite good.
Nils has release all of his works for free, asking that if you wish to provide some sort of compensation that you commit to any number of practices listed on his site. Everything is explained here.
(via comp.lang.scheme)
I asked “What is a good book on automata theory?” because I don’t recall much of it from college. Marco replied here: Elements of the Theory of Computation by Lewis and Papadimitriou.
Do you know of any more?
Addendum: 19/02/09
Prabhakar added:
The 1979 edition of “Introduction to Automata Theory, Languages, and Computation“, by Hopcroft and Ullman. The algorithms are pretty imperative, though.
Addendum: 20/02/09 at 2:25CST
Jos added:
I very much appreciate: Formal Languages and their |Relation to Automata by John E. Hopcroft and Jeffrey D. Ullman. My first read through it was 40 years ago, but even nowadays I consult it now and then.
Folks might be interested to see that in R6RS Scheme:
I was asking about the difference in practice between letrec and letrec* here and got a bunch of great replies.
I didn’t understand why you would bother to use letrec at all when you could only expect it to work predictably when binding mutually recursive lambda expressions since the order of evaluation was not guaranteed (it occurs in some unspecified order). Thanks to everyone’s feedback I realized that the answer lay in my confusion: the value of letrec is specifically to indicate the fact that order of evaluation is not of concern. That is the whole point of providing both letrec and letrec*: the former tells the reader that it is purely functional, the latter that it is not. Perhaps this is a big “doh!” on my part; but I am glad that I asked.
On review of the R6RS rationale here; one finds that this was indeed the intent:
9.1 Unspecified evaluation order
The order in which the subexpressions of an application are evaluated is unspecified, as is the order in which certain subexpressions of some other forms such as letrec are evaluated. While this causes occasional confusion, it encourages programmers to write programs that do not depend on a specific evaluation order, and thus may be easier to read. Moreover, it allows the programmer to express that the evaluation order really does not matter for the result. A secondary consideration is that some compilers are able to generate better code if they can choose evaluation order.