Wednesday, December 1, 2010

Es taut nicht

The subject is German, meaning "it doesn't thaw", which is rather true: as I write this we have chilly -10 °C (14 °F) and 25 cm (10 inches) snow on the ground. And it keeps snowing. I cannot remember a winter like this.

But this is not the reason of my posting! Instead I have hidden a pun in there: "there is no tau", yes, the Greek letter (τ). Which proposition is definitely false, because as of today I succeeded to encode de Bruijn's higher degree binders in Ωmega. I've fought a lot (on and off) against this fortress...

The code is here, see and comment.

PS: Does anybody know a better quality URL for this paper?

1 comment:

heisenbug said...

for the record, a google query with these keywords
quantifier lambda calculus Bloo Nederpelt
will open a treasure trove of research on the subject, especially in Bologna much of the formalization has been done already