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!

Date: 2009-09-15 11:55 am (UTC)From: [identity profile] 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.

Date: 2009-09-15 02:52 pm (UTC)From: [identity profile] 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.

Date: 2009-09-15 03:16 pm (UTC)From: [identity profile] 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.

Date: 2009-09-15 02:54 pm (UTC)From: [identity profile] 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.

Date: 2009-09-15 03:13 pm (UTC)From: [identity profile] 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).

Date: 2009-09-16 03:42 am (UTC)From: [identity profile] 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

Date: 2009-09-16 03:44 am (UTC)From: [identity profile] 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

Date: 2009-09-16 02:10 pm (UTC)From: [identity profile] 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)

Date: 2009-09-15 03:38 pm (UTC)From: [identity profile] demarko (from livejournal.com)
on a more serious note:
[λ_.M]Ω looks like an extremely disfigured yet omegaembarrassed smiley face

Date: 2009-09-16 02:11 pm (UTC)From: [identity profile] simrob.livejournal.com
You will be embarrassed forever!!!

Date: 2009-09-16 03:30 pm (UTC)From: [identity profile] 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.

Date: 2009-09-16 03:32 pm (UTC)From: [personal profile] ikeepaleopard
ikeepaleopard: (Default)
So the lesson is that only eager people have to be embarrassed forever?

Date: 2009-09-19 03:59 pm (UTC)From: [identity profile] 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?

Profile

chrisamaphone

August 2014

S M T W T F S
     12
3456789
10111213141516
17181920 21 2223
24252627282930
31      

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Oct. 21st, 2017 05:47 pm
Powered by Dreamwidth Studios