Timeline for Is the SK2 calculus a complete basis, where K2 is the flipped K combinator?
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 2, 2019 at 23:28 | history | edited | Z. A. K. | CC BY-SA 4.0 | Edited according to the comments to show that this is only a partial answer |
| May 2, 2019 at 22:49 | comment | added | Z. A. K. | Charles Stewart's observation is correct. While it is true that every well-typed proper combinator that can be defined in the SKI calculus can also be defined in the simply-typed SKI calculus, the same thing need not be (a priori) true of the SK2I calculus. | |
| May 2, 2019 at 19:33 | comment | added | cole | I’m afraid that I’m a little in over my head here, so I’m going to remove my acceptance of this answer and update my question to indicate that I’d be fine with either an argument that it’s Turing (in)complete or an (in)complete basis. I’ll try to check in later to see if I should leave the question unaccepted. | |
| May 2, 2019 at 17:44 | comment | added | chi | @NoamZeilberger I also agree. This argument unfortunately seems insufficient: in the untyped calculus you might be able to obtain $K$ using a construction which involves (sub)terms which have no type. One should prove that if you can achieve that, you can also do the same using only typed terms, but that looks hard to prove to me. | |
| May 2, 2019 at 16:08 | comment | added | Noam Zeilberger | I agree with Charles Stewart (over here: twitter.com/txtpf/status/1123962607306706944) that it's not clear how to pass from uninhabitation in simply-typed lambda calculus to inexpressibility using combinators. There might be an argument specific for K, but the initial step "...then one could also do the same thing in the simply-typed λ-calculus" doesn't hold in general (Charles mentioned the counterexample of the Y combinator). Do you see of making this argument rigorous? | |
| May 1, 2019 at 21:53 | vote | accept | cole | ||
| May 2, 2019 at 19:33 | |||||
| May 1, 2019 at 18:13 | history | edited | Z. A. K. | CC BY-SA 4.0 | clarified language |
| May 1, 2019 at 16:34 | history | edited | Z. A. K. | CC BY-SA 4.0 | minor clarifications |
| May 1, 2019 at 16:31 | comment | added | Z. A. K. | @robin-houston: please see my edit (I've also added a different, semantic argument with the same conclusion). | |
| May 1, 2019 at 16:02 | history | edited | Z. A. K. | CC BY-SA 4.0 | Added a simple semantic proof, commented on missing parts of original argument. |
| May 1, 2019 at 13:07 | comment | added | Robin Houston | Can you sketch how to prove S in this restricted sequent calculus? It doesn’t seem to be possible with the rules I guessed you might mean. | |
| May 1, 2019 at 12:00 | comment | added | Noam Zeilberger | I like the approach, but could you clarify what rules you are taking as your sequent calculus? | |
| May 1, 2019 at 11:07 | history | edited | Z. A. K. | CC BY-SA 4.0 | corrected typos, slight rewording, formatting |
| May 1, 2019 at 11:05 | review | First posts | |||
| May 1, 2019 at 12:38 | |||||
| May 1, 2019 at 11:02 | history | answered | Z. A. K. | CC BY-SA 4.0 |