(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

[jcreed.livejournal.com]

I thought church-rosser was just confluence? I don't see why [λ_.M] Ω is a counterexample to that. You do some reduction steps on Ω, but you can still get back to M.

[simrob.livejournal.com]

Nope! This is a sloppy terminology that Karl blamed on Barendrecht I think.

Confluence is that if A ->* B and A ->* C then there exists a D such that B ->* D and C ->* D. Church Rosser is the property that if B is convertible to C by an arbitrary series of beta reductions and expansions, then there is a D such that B ->* D and C ->* D. Church Rosser proves all sorts of things, such as the uniqueness of normal forms (when they exist) all by itself.

Obviously, Church Rosser implies confluence (just expand B to A, and then reduce A to C - so B and C are convertible and have a common descendent). In some settings, I'm pretty sure we prove Church Rosser by proving confluence, but this leads to really unfortunate non-proofs in a lot of situations for reasons that are difficult to describe non-graphically.

[chrisamaphone]

e:f;b.

by the way, wikipedia also says church-rosser is confluence.

[simrob.livejournal.com]

By the way, if anyone else is as confused by Chris' kids-these-days-and-their-internet-speech, e:f;b. on urbandictionary.

[simrob.livejournal.com]

Oh - and now I understand your comment better. Church-Rosser, as I just described, is Theorem 1. Theorem 2 is that, if a normal form B of some term A exists, any evaluation strategy (any sequence of beta reductions) will eventually get to it - it's kind of a "strong normalization" result for the untyped lambda calculus, and it's false for the not-strict untyped lambda calculus.

[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)

[chrisamaphone]

i also thought church rosser was confluence! but this paper never actually mentions confluence; the property it does mention that apparently everyone in the POP group these days calls the church-rosser property is: given any ol' conversion sequence from A to B with reductions and expansions possibly intermixed, you can turn it into a conversion from A to B where you do all the reductions first and then all the expansions (or, similarly, you can find a common reduct of A and B, although i'm actually still slightly confused about how these two readings are interchangeable).

*that* result is still true for ordinary nonstrict lambda calc, but requires some tweaks to the proofs of the lemmas.

but he paper also proves that given a reduction sequence from A to B, all reduction sequences from A to B terminate, along with the corollary that if a formula has a normal form then all subformulas of it have a normal form, both of which are false for nonstrict lambda calc via the [λ_.M] Ω example.

[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?