A merry gang

Last Wednesday, FLIB’s kick-off meeting took place at Oblong’s Barcelona lab, with a dozen deliciously crazy people attending.

Due to lack of time and seriousness on my side, the main talk was given by Jos, who gave us an overview of his work with PLT Redex to model lambda calculus. Redex provides an embedded DSL to create context-sensitive term-rewriting systems, if you’ll pardon my buzzwording. In a hand-waving nutshell, term-rewriting systems are syntax-rules on steroids: one specifies a set of rules for transforming (rewriting, or reducing) terms to other terms according to their structure, possibly depending on context. Jos has a very nice example of such a system taken from GEB (Best. Book. Ever.), the MIU formal system, whose formal rules can be expressed in Redex as:

  (--> (‹symbol›  ... I) (‹symbol› ... I U))
  (--> (M ‹symbol› ..) (M ‹symbol› ... ‹symbol› ...))
  (--> (‹symbol›_0 ... I I I ‹symbol›_1 ...) (‹symbol›_0 ... U ‹symbol›_1 ...))

that is, if you find a trailing I, you can append U; if you find M, you can duplicate the rest of the string; and three consecutive Is can be reduced to a single U. Now, you can start with a given string (or axiom) and apply the rules to produce new ones (theorems). Note how the rules are contextual, and how there’s in general more than one that is applicable. Redex will do that for you, creating a tree with all possible reductions.

MIU reductions in Redex

Of course, there’s more to Redex than this simple example. For instance, it’s been used to provide an operational semantics for R6RS. Jos’ work is somewhere in the middle: while the reduction rules in lambda calculus are even simpler than in MIU, issues of scope quickly complicate things; moreover, Jos explores classical topics in lambda calculus, such as reduction to normal form, fixed point combinators or Church numerals to name a few, always using Redex (the staggering conceptual richness embodied by the humble premises of lambda calculus always amazes me). All in all, a beautiful 32-pages long paper, with accompanying code, that serves as a nice hands-on introduction to both lambda calculus and Redex, and which you can get at Jos homepage.

After the presentation, we devoted some time to talk about the future of FLIB. Monthly presentations, lightning talks on demand and a reading group. I like the latter a lot, because having a physical meeting among readers every month is an excellent way of keeping reading groups alive. We’re still deciding on our first book, but PLAI followed by LiSP seems to be gaining momentum right now. Another nice thing about the reading group is that it opens the possibility for people not able to come to the meetings to participate: just subscribe to our mailing list and join the discussions about the book du jour.

And then we just sat down around a table with some beer and snacks, and start talking about life and programming languages. I found it very stimulating because of the varied people’s backgrounds: we had guys from academia and industry; ones just starting their graduate courses, others with twenty years of teaching under their belts; people from several different countries; schemers obsessed with call/cc, smalltalkers, python experts, C++ loathers and programmers who secretly enjoy it, perlmongers and ruby or haskell aficionados. But, they all, people with a passion for programming: i think everybody was happy to have found a bunch of keen souls.

Perhaps it was inevitable that much of the discussion gravitated around our frustrations as programmers and teachers, given the sad state of computer science in both industry and academia, and the insurmountable barriers for adoption faced by the kind of languages we like. But, with that out of the way, here’s hope (as expressed by Andy after the meeting) that future meetings will concentrate on brighter fields.

A great evening, and no mistake. I hope you’ll join the fun next July 22nd!

One Response to “A merry gang”

  1. Jos Koot Says:

    Jao, thanks for I nice survey of our first meeting. And for your kind words.

    There is a typo (mine) in the third line of the grammar of MIU: replace 2 with 1. (The source code does not have this typo)

    I would like to add that in my talk I did not come so far as showing redex-match and redex-check. Only after my talk I mentioned it at the table with refreshments. These two tools are very important when designing a grammar and its semantics, for you certainly will want to check that the grammar and semantics have the desired properties (for example being normalizing) and inspect for errors, typos of course, but more importantly: fundamental design errors.

    I am sure I’ll attribute a lightning talk next July 22nd, although at the moment I don’t yet know about what.

    Jos


Leave a Reply