Editing Combinatory logic (section)

==== One-point basis ====

There are one-point bases from which every combinator can be composed extensionally equal to ''any'' lambda term. A simple example of such a basis is {'''X'''} where:

:'''X''' ≡ ''λx''.((x'''S''')'''K''')

It is not difficult to verify that:
:'''X''' ('''X''' ('''X''' '''X''')) =<sup>β</sup> '''K''' and
:'''X''' ('''X''' ('''X''' ('''X''' '''X'''))) =<sup>β</sup> '''S'''.

Since {'''K''', '''S'''} is a basis, it follows that {'''X'''} is a basis too. The [[Iota and Jot|Iota]] programming language uses '''X''' as its sole combinator.

Another simple example of a one-point basis is:

:'''X'''' ≡ ''λx''.(x '''K''' '''S''' '''K''') with
:('''X'''' '''X'''') '''X'''' =<sup>β</sup> '''K''' and
:'''X'''' ('''X'''' '''X'''') =<sup>β</sup> '''S'''

The simplest known one-point basis is a slight modification of '''S''':

:'''S'''' ≡ ''λxλyλz''. (x z) (y (λw. z))) with
:'''S'''' ('''S'''' '''S'''') ('''S'''' ('''S'''' '''S'''') '''S'''' '''S'''' '''S'''' '''S'''' '''S'''') = <sup>β</sup> '''K''' and
:'''S'''' ('''S'''' ('''S'''' '''S'''' ('''S'''' '''S'''' ('''S'''' '''S''''))('''S'''' ('''S'''' ('''S'''' '''S'''' ('''S'''' '''S'''')))))) '''S'''' '''S'''' = <sup>β</sup> '''S'''.

In fact, there exist infinitely many such bases.{{sfn|Goldberg|2004}}