Skip to main content

Lambda hackulus: machinery for Bohm's theorem

I've been distracting myself recently by doing some untyped-lambda-calculus hackery, so I may as well write it up, because I don't think I've seen this particular kind of hackery described elsewhere, and I'm trying to get better at day-to-day documentation. It's kind of cute and probably not very profound, but if anyone sees connections to other work, please point it out.

The context is here is that I was attempting to understand Bohm's Theorem (a la [1] or [2]), and Twelf is my usual tool for understanding things about lambda calculi. So I started with the bog-standard Twelf encoding of untyped lambda calculus:

exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

...with the goal in mind of eventually formalizing Bohm's Theorem. (I do still have that goal in mind, by the way, and will hopefully post about it when completed.)

The puzzle is how to write programs over such terms that implement the various meta-level functions in [2], i.e. REPLACE(k, S), SELECT(k, i), and ROTATE(k). Their definitions are given using the convenience of paper notation:

REPLACE(k, S) = λx_0.λx_1...λx_k.S
SELECT(k, i) = λx_0.λx_1...λx_k.x_i
ROTATE(k) = λx_0.λx_1...λx_k.x_k x_0 x_1 ... x_k-1

Looks straightforward, but given our standard binary tree structure of lambda terms, we need to uncover the inductive structure of these n-ary term-formers in order to write the corresponding elf programs. These programs are declared as follows:

replace : nat -> exp -> exp -> type.
select : nat -> nat -> exp -> type.
rotate : nat -> exp -> type.

Replace and select turn out to be pretty straightforward once we define

klam : nat -> (exp -> exp) -> type.
klam/0 : klam 0 ([x] x).
klam/s : klam (s K) ([x] lam [y] (M x))
          <- klam K ([x] M x).

An E for which there is a derivation of klam K ([x] E x) is expression beginning with K lambda bindings and ending in x; that is: klam(k) = [x] lam[x_1]...lam[x_k] x

Now we can write replace and select:

replace : nat -> exp -> exp -> type.
%mode replace +N +E -E'.
replace/i : replace K S (E S)
             <- klam K ([x] E x).

select : nat -> nat -> exp -> type.

select/0 : select (s K) 0 (lam [x0] E x0)

            <- klam K ([x] E x).

select/s : select (s K) (s I) (lam [x0] E)

            <- select K I E.

Rotation is significantly trickier. We can't use our klam trick because the body of the expression actually needs to mention every variable we bind. The inductive structure is also less apparent and, once discovered, annoyingly inside-out.

The first thing we can notice is that the inner-most variable is treated in a distinct way from every other part of the term, so let's try to separate concerns by leaving a hole for the function and building up the application to arguments inductively.

First, a slight digression:

Spine Form

Spine form refers to a way of writing down lambda terms to look more like C functions. Spines are simply lists of expressions, and application instead of consisting of two expressions consists of a head expression and a spine consisting of its arguments. (Usually there are some additional constraints like that the head is a variable or constant and the spine drives the head down to base type, but here we're only concerned with the syntactic structure.)

So in fact if we had encoded the lambda calculus as
sp : type.

exp : type.

nil : sp.

cons : exp -> sp -> sp.

lam : (exp -> exp) -> exp.

app : exp -> sp -> exp.

I expect ROTATE would be easier to write. The consequent code winds up looking a lot like the standard translation from spine form to traditional application.

Okay. So, I said that we're going to construct a term with a hole in it for a function to go eventually. A term with a hole in it is represented by the LF type (exp -> exp), and inhabited by things like ([x:exp] app x x).

I found it helpful to write down the inductive step in isolation. Suppose we have a context M containing a hole for the function, which is that inner variable x_k applied to some of its arguments, and now we want to apply it to one more argument all the way on the inside. Because we're working inside-out, from the last argument to the first one. So we need to go from \x_i...\x_k-1 (... ([HOLE] x_i) ...) x_k-1 to \x_i-1.\x_i...\x_k-1 ( ... (([HOLE] x_i-1) x_i ...) x_k-1, or in Twelf,

extend : (exp -> exp) -> (exp -> exp) -> type.

extend/i : extend ([f] M f) ([f] lam [x] M (app f x)).

(Shortly before this point, I showed the puzzle to William Lovas, who pointed out that my initial version of extend applied things in the wrong order. Thanks to him for that and for working on the remainder of the construction with me.)

Now let's implement the function that does this K times for a given K.

spine : nat -> (exp -> exp) -> type.

spine/0 : spine 0 ([f] f). 

spine/s : spine (s K) C'

           <- spine K C 
           <- extend C C'.

Finally we're ready to deal with creating the innermost lambda binding and applying the function to the spine. Effectively we have [f] \xs f xs, and we need \xs\f.f xs.

jam_in : (exp -> exp) -> exp -> type.

jam_in/lam : jam_in ([f] lam [x] M f x) (lam [x] M' x)

              <- ({x} jam_in ([f] M f x) (M' x)).

jam_in/at  : jam_in ([f] R f) (lam [f] R f).

Putting these pieces together at last lets us define rotation.

rot : nat -> exp -> type.

rot/i : rot K M 

         <- spine K C 

         <- jam_in C M.



  1. Hi thank you for the information. i was searching for the same thing your post is very useful to me.
    Tank Car Loading


Post a Comment

Popular posts from this blog

Using Twine for Games Research (Part II)

This preliminary discussion introduced my thoughts on using Twine as a tool for creating prototypes for games research. I'll start with documenting my first case study: a hack-and-slash RPG-like setting where the player character has a record of attributes ("stats") that evolve through actions that turn certain resources (money, health, items) into others. I've selected this hack-and-slash example because it falls outside the canonical "branching story" domain thought to be Twine's primary use case, but it is not too much trickier to implement. It relies crucially on the management of state in ways that simple branching stories would not, but it does so in a fairly straightforward way.

If all goes well, this post may also serve as a tutorial on the "basics" of Twine (links + variables + expressions). In particular, I'll be using Twine 2/Harlowe, and I haven't seen many tutorials for this new version published yet.

To me, the main "…

Using Twine for Games Research (Part III)

Where we last left off, I described Twine's basic capabilities and illustrated how to use them in Twine 2 by way of a tiny hack-and-slash RPG mechanic. You can play the result, and you should also be able to download that HTML file and use Twine 2's "import file" mechanism to load the editable source code/passage layout.

Notice that, in terms of game design, it's not much more sophisticated than a slot machine: the only interesting decision we've incorporated is for the player to determine when to stop pushing her luck with repeated adventures and go home with the current spoils.

What makes this type of RPG strategy more interesting to me is the sorts of decisions that can have longer-term effects, the ones where you spend an accumulation of resources on one of several things that might have a substantial payoff down the road. In a more character-based setting, this could be something like increasing skill levels or adding personality traits.

Often, the game-…

Why I don't like the term "AI"

Content note: I replicate some ableist language in this post for the sake of calling it out as ableist.

In games research, some people take pains to distinguish artificial intelligence from computational intelligence (Wikipedia summary), with the primary issue being that AI cares more about replicating human behavior, while CI is "human-behavior-inspired" approaches to solving concrete problems. I don't strongly identify with one of these sub-areas more than the other; the extent to which I hold an opinion is mainly that I find the distinction a bit silly, given that the practical effects seem mainly to be that there are two conferences (CIG and AIIDE) that attract the same people, and a journal (TCIAIG - Transactions on Computational Intelligence and Artificial Intelligence in Games) that seems to resolve the problem by replacing instances of "AI" with "CI/AI."

I have a vague, un-citeable memory of hearing another argument from people who dislike the…