We're off to a good start! We went over the first set of slides in the meeting, and everyone had ideas to contribute.
One of the things we wondered about was why exponentiation of Church-encoded numerals can be done just by applying the exponent to the base, as a function. Working through an example helped:
One of the questions we were left with was this: Supposedly the point of Church-encoding data is so that you can do computations with it. But when you get your result, how can you interpret it? We are not guaranteed that the lambda expression will reduce to a normal form (as opposed to continuing infinitely). If it does converge to an irreducible expression, how do we know whether that expression is equivalent to a particular Church numeral? In general it's undecidable whether two lambda expressions are equivalent.
Perry said that Mayer Goldberg had produced a program that could interpret lambda calculus results, that is, "decode" the Church encoding. I'd be interested to see that. I'm sure there would be edge cases where it wouldn't work, but perhaps it works most of the time. Interestingly, Goldberg also wrote a paper
showing that any equality predicate on Church numerals could be circumvented - that is, we can construct a term that satisfies the equality test with all