26 Aug 2002 raph   » (Master)

Metamath

I believe that the formulation of lambda I was wondering about yesterday is:

$d y A $.
df-lambda $a |- ( lambda x A ) = { <. x , y >. | y = A } $.

This lets me prove such things as ( ( lambda x x ) ` y ) = y. I'm probably not at the full power of the lambda calculus, though, because here "y" is required to be a set, while a lambda term is a class. So it's not clear I can apply this lambda term to itself.

School

Tomorrow is Alan's first day of 1st grade. It promises to be exciting.

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!