Editing Lambda calculus (section)

=== Abstraction elimination ===
{{Further|Combinatory logic#Completeness of the S-K basis}}
If ''N'' is a lambda-term without abstraction, but possibly containing named constants ([[combinatory logic|combinators]]), then there exists a lambda-term ''T''({{Mono|''x''}},''N'') which is equivalent to {{Mono|λ''x''.}}''N'' but lacks abstraction (except as part of the named constants, if these are considered non-atomic). This can also be viewed as anonymising variables, as ''T''({{Mono|''x''}},''N'') removes all occurrences of {{Mono|''x''}} from ''N'', while still allowing argument values to be substituted into the positions where ''N'' contains an {{Mono|''x''}}. The conversion function ''T'' can be defined by:
: ''T''({{Mono|''x''}}, {{Mono|''x''}}) := '''I'''
: ''T''({{Mono|''x''}}, ''N'') := '''K''' ''N'' if {{Mono|''x''}} is not free in ''N''.
: ''T''({{Mono|''x''}}, ''M'' ''N'') := '''S''' ''T''({{Mono|''x''}}, ''M'') ''T''({{Mono|''x''}}, ''N'')
In either case, a term of the form ''T''({{Mono|''x''}},''N'') ''P'' can reduce by having the initial combinator '''I''', '''K''', or '''S''' grab the argument ''P'', just like β-reduction of {{Mono|(λ''x''.}}''N''{{Mono|)}} ''P'' would do. '''I''' returns that argument. '''K''' throws the argument away, just like {{Mono|(λ''x''.}}''N''{{Mono|)}} would do if {{Mono|''x''}} has no free occurrence in ''N''. '''S''' passes the argument on to both subterms of the application, and then applies the result of the first to the result of the second.

The combinators '''B''' and '''C''' are similar to '''S''', but pass the argument on to only one subterm of an application ('''B''' to the "argument" subterm and '''C''' to the "function" subterm), thus saving a subsequent '''K''' if there is no occurrence of {{Mono|''x''}} in one subterm. In comparison to '''B''' and '''C''', the '''S''' combinator actually conflates two functionalities: rearranging arguments, and duplicating an argument so that it may be used in two places. The '''W''' combinator does only the latter, yielding the [[B, C, K, W system]] as an alternative to [[SKI combinator calculus]].