Editing Combinatory logic (section)

== Undecidability of combinatorial calculus ==

A [[normal form (abstract rewriting)|normal form]] is any combinatory term in which the primitive combinators that occur, if any, are not applied to enough arguments to be simplified. It is undecidable whether a general combinatory term has a normal form; whether two combinatory terms are equivalent, etc. This can be shown in a similar way as for the corresponding problems for lambda terms.

=== Undefinability by predicates ===
The undecidable problems above (equivalence, existence of normal form, etc.) take as input syntactic representations of terms under a suitable encoding (e.g., [[Church encoding]]). One may also consider a toy trivial computation model where we "compute" properties of terms by means of combinators applied directly to the terms themselves as arguments, rather than to their syntactic representations. More precisely, let a ''predicate'' be a combinator that, when applied,  returns either '''T''' or '''F''' (where '''T''' and '''F''' represent the conventional [[Church encoding#Church Booleans|Church encodings of true and false]], ''λx''.''λy''.''x'' and ''λx''.''λy''.''y'', transformed into combinatory logic; the combinatory versions have {{nowrap|1='''T''' = '''K'''}} and {{nowrap|1='''F''' = ('''K''' '''I''')}}). A predicate '''N''' is ''nontrivial'' if there are two arguments ''A'' and ''B'' such that '''N''' ''A'' = '''T''' and '''N''' ''B'' = '''F'''. A combinator '''N''' is ''complete'' if '''N'''''M'' has a normal form for every argument ''M''.  An analogue of Rice's theorem for this toy model then says that every complete predicate is trivial. The proof of this theorem is rather simple.{{sfn|Engeler|1995}}
{{math proof
| proof = By reductio ad absurdum. Suppose there is a complete non trivial predicate, say '''N'''. Because '''N''' is supposed to be non trivial there are combinators ''A'' and ''B'' such that
:('''N''' ''A'') = '''T''' and
:('''N''' ''B'') = '''F'''.

:Define NEGATION ≡ ''λx''.(if ('''N''' ''x'') then ''B'' else ''A'') ≡ ''λx''.(('''N''' ''x'') ''B'' ''A'')
:Define ABSURDUM ≡ ('''Y''' NEGATION)

Fixed point theorem gives: ABSURDUM = (NEGATION ABSURDUM), for
:ABSURDUM ≡ ('''Y''' NEGATION) = (NEGATION ('''Y''' NEGATION)) ≡ (NEGATION ABSURDUM).

Because '''N''' is supposed to be complete either:
# ('''N''' ABSURDUM) = '''F''' or
# ('''N''' ABSURDUM) = '''T'''

* Case 1: '''F''' = ('''N''' ABSURDUM) = '''N''' (NEGATION ABSURDUM) = ('''N''' ''A'') = '''T''', a contradiction.
* Case 2: '''T''' = ('''N''' ABSURDUM) = '''N''' (NEGATION ABSURDUM) = ('''N''' ''B'') = '''F''', again a contradiction.

Hence ('''N''' ABSURDUM) is neither '''T''' nor '''F''', which contradicts the presupposition that '''N''' would be a complete non trivial predicate. '''[[Q.E.D.]]'''
}}
From this undefinability theorem it immediately follows that there is no complete predicate that can discriminate between terms that have a normal form and terms that do not have a normal form. It also follows that there is '''no''' complete predicate, say EQUAL, such that:
:(EQUAL ''A B'') = '''T''' if ''A'' = ''B'' and
:(EQUAL ''A B'') = '''F''' if ''A'' ≠ ''B''.
If EQUAL would exist, then for all ''A'', ''λx.''(EQUAL ''x A'') would have to be a complete non trivial predicate.

However, note that it also immediately follows from this undefinability theorem that many properties of terms that are obviously decidable are not definable by complete predicates either: e.g., there is no predicate that could tell whether the first primitive function letter occurring in a term is a '''K'''. This shows that definability by predicates is a not a reasonable model of decidability.