Editing SKI combinator calculus (section)

===Boolean logic===
SKI combinator calculus can also implement [[Boolean logic]] in the form of an ''if-then-else'' structure.  An ''if-then-else'' structure consists of a Boolean expression that is either true ('''T''') or false ('''F''') and two arguments, such that:
: '''T'''''xy'' = ''x''
and
: '''F'''''xy'' = ''y''

The key is in defining the two Boolean expressions.  The first works just like one of our basic combinators:
: '''T''' = '''K'''
: '''K'''''xy'' = ''x''

The second is also fairly simple:
: '''F''' = '''SK'''
: '''SK'''''xy'' = '''K'''''y(xy)'' = y

Once true and false are defined, all Boolean logic can be implemented in terms of ''if-then-else'' structures.

Boolean '''NOT''' (which returns the opposite of a given Boolean) works the same as the ''if-then-else'' structure, with '''F''' and '''T''' as the second and third values, so it can be implemented as a postfix operation:
: '''NOT''' = λb.b ('''F''')('''T''') = λb.b ('''SK''')('''K''')
If this is put in an ''if-then-else'' structure, it can be shown that this has the expected result
: ('''T''')'''NOT''' = '''T'''('''F''')('''T''') = '''F'''
: ('''F''')'''NOT''' = '''F'''('''F''')('''T''') = '''T'''

Boolean '''OR''' (which returns '''T''' if either of the two Boolean values surrounding it is '''T''') works the same as an ''if-then-else'' structure with '''T''' as the second value, so it can be implemented as an infix operation:
: '''OR''' = '''T''' = '''K'''
If this is put in an ''if-then-else'' structure, it can be shown that this has the expected result:
: ('''T''')'''OR'''('''T''') = '''T'''('''T''')('''T''') = '''T'''
: ('''T''')'''OR'''('''F''') = '''T'''('''T''')('''F''') = '''T'''
: ('''F''')'''OR'''('''T''') = '''F'''('''T''')('''T''') = '''T'''
: ('''F''')'''OR'''('''F''') = '''F'''('''T''')('''F''') = '''F'''

Boolean '''AND''' (which returns '''T''' if both of the two Boolean values surrounding it are '''T''') works the same as an ''if-then-else'' structure with '''F''' as the third value, so it can be implemented as a postfix operation:
: '''AND''' = '''F''' = '''SK'''
If this is put in an ''if-then-else'' structure, it can be shown that this has the expected result:
: ('''T''')('''T''')'''AND''' = '''T'''('''T''')('''F''') = '''T'''
: ('''T''')('''F''')'''AND''' = '''T'''('''F''')('''F''') = '''F'''
: ('''F''')('''T''')'''AND''' = '''F'''('''T''')('''F''') = '''F'''
: ('''F''')('''F''')'''AND''' = '''F'''('''F''')('''F''') = '''F'''

Because this defines '''T''', '''F''', '''NOT''' (as a postfix operator), '''OR''' (as an infix operator), and '''AND''' (as a postfix operator) in terms of SKI notation, this proves that the SKI system can fully express Boolean logic.

As the SKI calculus is [[Combinatory logic#Completeness of the S-K basis|complete]], it is also possible to express '''NOT''', '''OR''' and '''AND''' as prefix operators:
: '''NOT''' = '''S'''('''SI'''('''KF'''))('''KT''') (as '''S'''('''SI'''('''KF'''))('''KT''')''x'' = '''SI'''('''KF''')''x''('''KT'''''x'') = '''I'''''x''('''KF'''''x'')'''T''' = ''x'''''FT''')
: '''OR''' = '''SI'''('''KT''') (as '''SI'''('''KT''')''xy'' = '''I'''''x''('''KT'''''x'')''y'' = ''x'''''T'''''y'')
: '''AND''' = '''SS'''('''K'''('''KF''')) (as '''SS'''('''K'''('''KF'''))''xy'' = '''S'''''x''('''K'''('''KF''')''x'')''y'' = ''xy''('''KF'''''y'') = ''xy'''''F''')