Lambda the Ultimate

Okay, as is so often the case, in trying to formulate my problem more precisely, I think I made some progress on it. The language whose semantics I'm trying to define (call it "BD") is basically just an alternate way of stating a set of recursive equations. So I started out giving the semantics for BD by translating BD to equations, thus I felt like I was "generating code."

So this strategy I took assumes that the defining language has a "letrec" or similar construct. Maybe I can get this to work, but this assumption has two problems, as I see it.

• One is that this is not usually the level at which denotational semantics are given, i.e. the defining language (usually a lightly sugared lambda calculus) doesn't have a "letrec", in fact "letrec" has to be defined (using the fixed point operator, e.g. "fix").
• The other problem is that the equations that are the sub-parts of a letrec aren't really expressions, i.e. do not have a value, whereas usually the units of meaning in denotational semantics seem to be expressions, i.e. things like the letrec as a whole. I think the usual way of handling this is to turn the n individual equations of the letrec into a single equation with n-tuples on both sides. I need to find an example of this.

I believe the mathematical mechanism you are searching for is frequently called definite description. See the entry in the Enpsychlopedia ('cause that's such a nifty name), which is just a copy of the Wikipedia entry.

You are right that most denotational semantics do not tend to define meaning this way. They are more direct, except for the use of "fix". But definite description is a fairly obvious generalization of fixed-point definitions! The theorem prover IMPS uses this extensively, and outside of PVS is probably the most automated of the interactive theorem provers.

I am actually working (with a couple of colleagues) on something similar, where the semantics of the core part of the language is given by such a Solution Of mechanism. This has a very declarative flavour, but with a more traditional mathematics bent than the usual Prolog-esque logic programming flavour. Since it is a DSL (for Signal Processing), this looks like it will work. Doing so for a general purpose language would be scary, given the current state of the art.

Very interesting, indeed what you're working on sounds quite similar, since "BD" is in fact a DSL for Signal Processing as well (plus controls)! It stands for "Block Diagram" and is inspired by/seeks to improve upon some aspects of software like Simulink and Ptolemy.

Thanks for the links, I will take a look at them.

... C++ templates demonstrated that syntactic extension didn't have to be either textual substitution (the C preprocessor) or expose a ridiculously attenuated abstract syntax tree to the workaday programmer (LISP). Following these observations to their logical conclusion leads to something like camlp4, one of the few really good "Algol-like" syntactic extension systems around.

Off the top of my head, here's a few things that made templates look more "legitimate" to me than C preprocessor macros. (And because they seemed to provide a more "legitimate" way to generate code, this made me consider code generation in general to be a more "legitimate" programming technique.)

• They obey scoping rules. So, for example, you can avoid name clashes between different header files by wrapping one or more of them in namespaces.
• They can only produce functions or classes. Like many things, this could be considered an annoying limitation, but I consider it a good feature. So you can't do "cute" things like "#define K * 1024" and then "const oneK = 1 K". Or have things that look like functions have "returns" or goto in them.
• When used to type-parameterize functions, they provide the language with some type-inferencing capabilities.

So are you saying that your idea of code generation was limited to the C preprocessor? What do (or did) you think of writing a real program that generates other programs (think swig here)? Or do you consider that unrelated?

At the time, the examples of code generation I was aware of were probably

• the C preprocessor
• lex
• yacc
• (if I thought about it carefully enough) compilers

Cpre looked illegit to me since not only was it so limited but also its most common applications were to get around annoying limitations of C and/or C compilers (e.g. lack of function inlining, lack of constants).

It seemed to me that if you "fixed" C, the need for Cpre would go away, therefore the need to generate code seemed more like a crutch for a broken language than a legit programming technique. Indeed, the need for Cpre largely went away (at least in my programming style) with the "fix" of C that is C++.

I'm wasn't (and still am not) too familiar with lex & yacc but I suspected that, like Cpre, a lot of their reason for being was to get around annoying limitations of C.

I'm sure I thought compilers were legit.

My perspective really began to change when I worked at The Mathworks on a product called Real-Time Workshop (has very little to do with real time, actually), which "compiles" Simulink block diagrams by generating C code (used to generate Ada as well, but not any more).