Some Combinatory Logic

I've been very much into combinatory logic recently- both the Illative Combinatory Logic iXi and SKI. This post just records some things I've been thinking about.

First off, the church encoding of natural numbers in SKI. In the lambda calculus 0 = (\f.\x.x) and 1 = (\f.\x.fx). Translated to SKI these are 0 = KI and 1 = S(S(KS)(S(KK)I))(KI). It seems strange that 1 is so complex and 0 so simple, but even though I did the translation from lambda terms to SKI by hand, checking it with an online reducing program (http://pages.cpsc.ucalgary.ca/~nicholss/research/cl_web/cl_web.php) shows that it is correct. I remember from using this translation (the one given on the wikipedia page on combinatory logic) that the terms resulting from these translations will be pretty long. In this case, lets find a term that does the same thing, but is shorter.

To start off, lets look at numbers as a specification. This is often how I start out when trying to define a combinator. For 0 we have 0fx = x, which KI definitely fulfills, and for 1 we have 1fx = fx. It should be pretty clear that I is just as good as S(S(KS)(S(KK)I))(KI) as the term representing 1 as application associates to the left, so Ifx can be written (If)x and reduce to fx. I'm not sure that this generalizes in any way (to give simple terms to each natural), but it is cool that the naturals start out so nicely with KI and I.

I've also been reading more on ""Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus" and I've understood several more pieces. First off, I can see how the G combinator defined as (\x.\y.\z.Zx(Syz)) (I'm writing Z for the letter Xi) is a dependent product. It says that for some types x and y and some term z it gives the type of things that give for all things "a" of type x, the thing za in the dependent type ya. In other words, it points out elements of a dependent type depending on the given term.

I'm still struggling with a couple of things. One is exactly what types are and when they are inhabited, as the notion seems looser than that of a usual type theory. Another thing is the assertive interpretation of terms. For example, implication is given by (\x.\y.Z(Kx)(Ky)). This says that for all "a", if Kxa then Kya. Since Kxa reduces to x and Kya reduces to y, this says that if x then y. The problem I have is that it also seems to say that all true propositions are inhabited by all objects. I can understand this when the type is T (true), the unit type, but it seems odd for an arbitrary proposition. What I have to guess is that this is saying that propositions are truth-valued (possibly related to proof irrelevance?). Then all true statements are the same as the proposition T, which very well may be the case. Unless I'm completely lost, we should be able to take some inhabited type p and say Kp, saying that it is true as an inhabited type is a true proposition. This points out some of my confusion with this system, as my intuitions about what is what don't seem to apply.

I still haven't read through and understood the whole thing, but I'm actually making progress with every reread.