(no subject)

[chrisamaphone]

climbed for a long time today. majority of time was spent playing the climbing-"horse" game, where you pick a VB (very easy route) and try to do it with fewer holds than the person before you until no one can do better.

seminar was awesome today, because we discovered that the well-known classic result known as the church-rosser theorem, as originally described and proved in church and rosser's "some properties of conversion", is in fact describing properties of a "strict" lambda calculus where bound variables must occur in the body, and some of the central results are in fact false with the admission of such functions (most clearly seen from considering [λ_.M] Ω, which has a normal form that's not finitely reachable via all reduction paths). crazy!

Comments

[demarko (from livejournal.com)]

on a more serious note:
[λ_.M]Ω looks like an extremely disfigured yet omegaembarrassed smiley face

[simrob.livejournal.com]

You will be embarrassed forever!!!

[chrisamaphone]

oh, is that what that does? dang it, i knew i never should have run that emoticon as a child.

[simrob.livejournal.com]

Well, you're not embarrassed forever under all paths unless M=Ω, so just make sure to apply beta reduction directly to your nose rather than your left eye.

[ikeepaleopard]

So the lesson is that only eager people have to be embarrassed forever?

[wjl.livejournal.com]

eager's a dumb name for call-by-value/applicative order evaluation. 'cause hey, what if i just wanna substitute right away, without bothering to reduce the argument? isn't that a kind of eagerness?