Jan Wedekind <[email protected]> writes: > Hi, > After reading John Tromp's paper [1] (also see De Bruijn Index [2]) > I got very interested in Binary Lambda Calculus (BLC). In my little > spare time I implemented a BLC interpreter in C [3, 4]. > > I thought it would be interesting to share it on this mailing list > since the motivation behind BLC is similar to the one behind VPRI's > Nile [5] and Maru [6]. The test suite [7] gives a rough overview on > how BLC works: > > * 10, 110, 1110, ... are variables. 10 refers to the top of the stack > (the local environment), 110 refers to the next variable in the stack > and so on. > * 00M, where M is a term, defines a lambda expression expecting one > value on the stack. E.g. 0010 is the identity function which in Scheme > would be (lambda (x) x). > * 01MN, where M and N are terms, is a function > application. E.g. 0100100010 is the same as ((lambda (x) x) (lambda > (x) x)) in Scheme.
This encoding is a path down a binary tree. I rambled about the relation between stacks and de Bruijn indices in a recent blog post, as well as defining a tiny Lambda-Calculus-with-de-Bruijn-esque DSL inside Python ( http://chriswarbo.net/index.php?page=news&type=view&id=admin-s-blog%2Fanonymous-closures-in ). Apologies for the stream-of-consciousness style; I treat my blog as a place to jot down and explore ideas as they're forming in my head ;) > John Tromp's paper furthermore shows how boolean values are > represented using 0000110 and 000010 (i.e. functions taking two > arguments and returning the first or second argument). Scheme's cons > is represented by a function accepting a boolean and returning the > head or the tail of the list. An empty list is represented by 000010 > (false). The paper shows a meta-circular interpreter implemented in > 210 bits! This is generally known as Church Encoding. It has some nice applications, for example it's strongly related to parametricity in Type Theory. > I'm still undecided about how to approach some things: > * How does parallel processing fit into the picture? BLC is just a syntax for regular untyped lambda calculus, so all of the properties of lambda calculus apply, notably the Church-Rosser property ( http://en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem ). This tells us that every evaluation order will end up with the same result (if it terminates), so we can farm-out the evaluation of any term to as many machines as we like and the nondeterministic interleaving of results won't make a difference. The purity of BLC (its lack of side-effects) also means that there are no out-of-order problems with IO. The trick is determining what needs evaluating. For example Haskell's 'par' function is like the "false" function mentioned above: do_something_with (par foo bar) This is semantically equivalent to "do_something bar" but, due to low-level hackery, this is also a hint to Haskell that it should start evaluating "foo" in another thread if possible, since it may be needed soon. > * What's the best way to implement a DSL including booleans, integers, > floating point numbers, strings, .. on top of BLC? BLC is just a (binary) syntax for lambda calculus, so really you're asking for syntax on top of syntax. You can cut out the middle man and make your own syntax for lambda calculus, in which case you'll end up with something like Scheme ;) In reality, pretty much every functional language can be described as a layer of syntax on top of some variety of lambda calculus (Scheme, ML, Haskell, Clean, Agda, Coq, etc.). > * Is it possible to describe the electronics of integer addition and > multiplication in BLC and still have it jit-compiled to run > efficiently on x86 hardware? Not sure about this. You could use some kind of bit-vector type, which would correspond to a native int, then have your arithmetic functions auto-promote it to a bignum rather than overflowing. > * How to implement I/O (maybe use monadic objects)? Could the I/O > implementation provide equivalent functions to Scheme's quote and > eval, too? Monads are the way to go, since every other way I know of handling effects in a pure language (Algebraic Effect Handlers, Linear Types, etc.) require implementation machinery in the interpreter. Monadic IO can be done easily in any language with first-class functions, although it's a bit pointless when you're not required to be pure (although, of course, there are many more Monads out there which are very useful in any language). Cheers, Chris _______________________________________________ fonc mailing list [email protected] http://vpri.org/mailman/listinfo/fonc
