(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

[chrisamaphone]

what i wanna know is why the heck strict untyped lambda calculus was what they picked to examine in the first place. it's not terminating and it's not turing-complete. in william's words, seems like the worst of both worlds...

[simrob.livejournal.com]

They probably thought it terminated? The first and second Church papers both presented themselves primarily as a means of doing logic, not computation, which remember we hadn't figured out were the same yet. So Church's system also had a boatload of axioms, all of which happened to be strict.

It's not clear to me in my light reading of those two papers that they knew about the non-termination, nor is it clear what their response would have been had they known about the non-termination (i.e. if that would have screwed up their logic).

[wjl.livejournal.com]

i'm almost certain they knew of non-termination -- the proof of the strip lemma explicitly accounts for it! i don't remember the exact words, but they said something like, "even if the A1 -> A2 -> ... is extended infinitely, ...".

also, coming up with (\ x. x x) (\x. x x) is not that hard :P

[wjl.livejournal.com]

oh, i guess what i really mean is that (\x. x x) (\x. x x) is a perfectly valid and well-formed strict lambda-calculus term

[simrob.livejournal.com]

Right, omega is a strict term, but it's also possible that they were

1) Acting out of an abundance of caution, as they do in many other places
2) Newly aware of it, and had not been aware of it in the previous papers (in other words, the strictness assumption was in the first paper for ensuring termination, but then they realized it wasn't enough)