As an exercise, you can easily prove it (same strategy, if it is the case, then for any terms t and s, SKts = s). It seems that the third combinator is not important: that as soon as you have SK?, it is equivalent to I. Hurrah! It also reduce to t, so indeed, SKS and SKK are equivalent. To conclude our proof, we have to reduce SKSt and see whether it also reduces to t. So, the encoding of SKKt in the λ calculus reduces to t (as a sidenote, we just proved that SKK is equivalent to I here). We now just have to reduce it to a normal form (I detail every step, each time I reduce the leftmost λ, even tho it is not the fastest strategy): (λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.x)t So, let formalize your question: your question is whether, for any SKI term t, SKKt = SKSt? Well. A good exercise for you is to redo the proof, using the proper SKI semantics. In the rest of this answer, I'll take the same approach as you do, and convert SKI terms in λ terms. For instance, if you look at the wikipedia page, you can see that the semantics are not defined with lambda terms (and the fact that it correspond to lambda term is a (nice and expected) side effect). An other way to do it could have been to define directly SKI semantics. What you implicitly do in your question is that you express SKI in terms of λ terms and you rely on the semantics of the λ calculus. Now, there is a deep question, which is: what are the SKI-calculus? Actually, there is not a single way to answer that. "Behaviour" is an informal notion, which is formally capture by "semantics": if SKK and SKS are equals, then they should always reduce to the same term, according to the SKI-calculus semantics. So, how can we prove your statement? Simply by showing that SKK and SKS have the same behaviour. Your intuition is correct, but an intuition proves nothing (alas.) Perhaps that will be refined with practice. Particularly if a sort of order of operations can be explained-I regularly find myself confused when considering when to evaluate. Is my interpretation true? If not, can you provide an explanation? I would greatly appreciate it. (K z)returns the constant function that returns z, given another term input: (Y z). (Y z) is the application of Y to z, also a lambda term. The next lambda term will be substituted for y, let the term be Y. Everything I have read so far seems to use this convention). I am using the convention of “left-association” in my above notation, if that helps (And I tried to make that clear in the 4th term above with parentheses. the application of the application of S to K to Any-lambda-term is equivalent to the Identity combinator: SK(any-lambda-term) is also equivalent to I. S seems a little more complicated in the untyped lambda calculus. K essentially takes the next 2 (lambda) terms and gives back the first of those. SKK is equivalent to the Identity combinator, I. I started teaching myself lambda calculus last night and I am trying to determine if what I understand so far is correct.
0 Comments
Leave a Reply. |
Details
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |