Metablog

Hello, world. I’m learning Scala. It’s a pretty neat language, despite my initial negative reaction based on the name, logo, and color scheme of the site. I think I’ve finally gotten over liking Lisp especially. F# doesn’t seem especially impressive to me compared to Scala. Or even SML, to be honest.

Still single, and miserable. There’s no one out there like me. Well, close enough to no one that I haven’t been able to find them after three years of looking, off and on, through dating sites. Only a couple people that even come close, and those ones don’t respond.

They say that suicide is a disease in itself. Aside from depression, it takes a life of its own, and eats away at you even when you’d otherwise be happy. I’m not quite happy, but I’m close to it. Closer than I was a year ago. I still have plenty to justify suicide. I just wonder if I will ever run out of things to justify it. I clearly have a will to live. Just not a very strong one.

I’m learning Isabelle. I want to write a new user interface for it. Something awesome. I have a good idea of how to make it awesome, but I haven’t yet decided how to approach it. Or how to spend my free time working on it. Or how to deal with the stress of my job. Or the lack of a desire to live. Anyway, I’ve thought that I might take a bottom-up approach, reading the source code in order of how the compiler compiles it, which is guaranteed to be the most linear bottom-up approach available. (Unlike in languages like C# where source files can have circular dependencies up to the assembly (dll) level, which makes bottom-up reading potentially impossible.) But I’m not sure I’ll do that.

Due to an unfortunate incident, I’m required to attend AA meetings. It’s a shame, since I’m not an alcoholic, that I’m being forced to intrude on these meetings, but seeing the camaraderie between these people makes me want to attend something more appropriate for me. A bipolar meeting, perhaps? I don’t see anything in my city. Shame. I should call some hotlines that have better resources than google on this issue.

No real progress on lucid dreaming, despite the post title. I remember bits of dreams every few days. That’s about it. I promise not to subject you to any of my dreams. I may post here of some revelation I’ve had as a result of some dream. But that’ll be it. So far, the most significance any dream has had is that I needed to pee while I slept.

You know, I’m not even sure why I do this type of post. It’s not like there’s anyone who enjoys them. Now, my last post. That was one with popular appeal.

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.