Lambda the Ultimate

S is one of the two combinators forming the SK basis of combinatory logic.

You can think of a combinator as a funtion that converts functions into other functions.

The left inverse is another function that, when you apply it to the output of an application of S, gives you back the original input you fed to S.

So, for example, if you start with X, apply S to it to get S(X), then a left inverse L would give you L(S(X)) = X.

Hope that helps. ;-)

Thank you .. it definitely wasn't clear from the heading what 'S' this was.

Here's an article with some definitions.

Since T^-1 (S^-1 (S T)) = id, we have \x. T^-1(S^-1(x)) is the inverse of (S T), so a basis being invertible implies everything is invertible, by induction. ?

Edit: Ignore this terrible post :)

Rick Statman had some results (mid 80s, maybe?) about what properties a combinator basis had to have. The properties were syntactic in nature, so I don't know about non-injectivity. I recall there had to be at least some "parentheses" on the RHS of at least one combinator, perhaps something K-like (variable dropped from left to the right side), something S-like (in the sense that a LHS variable had to be repeated on the RHS).

OK, I googled it: the paper is from the 1986 LICS conference, but CiteSeer doesn't have a copy. The best I can find is a citation (but perhaps it's available at ACM if you have access -- I don't from home).

Statman, R., "On Translating Lambda Terms into Combinators: the Basis Problem." Proceedings of the 1st Symposium on Logic In Computer Science, pp 378--382. Cambridge, MA. June, 1986.

Will the SK basis do? If I'm not mistaken, k has an inverse too, k' = (\x -> x 42)

An injective basis only implies that a composition of combinators (x . y) has an inverse, not that (x y) has one.

(otherwise (k 42) would have an inverse, and that would just be weird)

Of course you (and Charles below) are right. Like I said, I hadn't thought about it very hard... :)

...and so S's inverse does not have a left inverse.