Metablog

As an exercise, to get some experience with Metamath’s formal system, I’ve been working on a formalization of the Lambda Calculus. (That article should provide more than enough background for this post.) I’ve run into a little issue, though. When defining combinators (certain fixed expressions with special meaning), one needs to use dummy variables. For instance, the S combinator is λxyz.xy(xz), where “x”, “y”, and “z” could be any three letters. You could choose them as needed not to collide with any other variables you’re using. However, when expanding these definitions in Metamath, it becomes impossible to avoid having to prove things like “x is not free in M”, even though of course it’s not free. For example, through beta reduction, we have

As the next step, we’d like to substitute y for N, yielding (MN(Mz))[z := L]. But we can’t do this without also proving that y is not free in M, because, expanding the steps in more detail, we have

There is no way to eliminate the [y := N] after the M without proving that doing so would not change the meaning of the term. Of course, I could eliminate that requirement from the axiom, but I fear the system would become unsound. Now, we know that this is a fine step to do, because we know that in the definition of the S combinator the variables x, y, and z are postulated not to match any of the other variables in the terms you’re substituting for them. The problem, however, is representing this notion in the formal system.

The paper I’m working on, available here, provides a fairly thorough and rigorous introduction to the subject, and so is pretty much ideal for what I’m using it for. However, it deal with the problem presented here by postulating that bound variables and free variables are drawn from two distinct sets. I don’t believe this approach is practical for Metamath.

Filed under Math. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.