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!