Functional Combinators - sgml/signature GitHub Wiki

If M is x, you replace λx.x with id (id is usually denoted by I in combinatory logic).

If M doesn't contain x, you replace the term with const M (const is usually denoted by K in combinatory logic).

If M is PQ, that is the term is λx.PQ, you want to "push" x inside both parts of the function application so that you can recursively process both parts. This is accomplished by using the S combinator defined as λfgx.(fx)(gx), that is, it takes two functions and passes x to both of them, and applies the results together. You can easily verify that that λx.PQ is equivalent to S(λx.P)(λx.Q), and we can recursively process both subterms.

Identity Function