Content deleted Content added
Omnipaedista (talk | contribs) not linked from the template |
Undid revision 1198945212 by EmilJ (talk) |
||
Line 313:
== 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
First, the term
The combinatory logic analogue of [[Rice's theorem]] says that there is no complete nontrivial predicate. A ''predicate'' is a combinator that, when applied, returns either '''T''' or '''F''' (where {{math|'''T'''}} and {{math|'''F'''}} represent the conventional [[Church encoding]]s of true and false, ''λx''.''λy''.''x'' and ''λx''.''λy''.''y'', transformed into combinatory logic; he combinatory versions have {{math|1='''T''' = '''K'''}} and {{math|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''. The analogue of Rice's theorem then says that every complete predicate is trivial. The proof of this theorem is rather simple.▼
:'''Ω''' = ('''S''' '''I''' '''I''' ('''S''' '''I''' '''I'''))
has no normal form, because it reduces to itself after three steps, as follows:
:('''S''' '''I''' '''I''' ('''S''' '''I''' '''I'''))
:= ('''I''' ('''S''' '''I''' '''I''') ('''I''' ('''S''' '''I''' '''I''')))
:= ('''S''' '''I''' '''I''' ('''I''' ('''S''' '''I''' '''I''')))
:= ('''S''' '''I''' '''I''' ('''S''' '''I''' '''I'''))
and clearly no other reduction order can make the expression shorter.
Now, suppose '''N''' were a combinator for detecting normal forms, such that
:<math>(\mathbf{N} \ x) = \begin{cases} \mathbf{T}, \text{ if } x \text{ has a normal form} \\
\mathbf{F}, \text{ otherwise.} \end{cases}</math>
:(Where {{math|'''T'''}} and {{math|'''F'''}} represent the conventional [[Church encoding]]s of true and false, ''λx''.''λy''.''x'' and ''λx''.''λy''.''y'', transformed into combinatory logic. The combinatory versions have {{math|1='''T''' = '''K'''}} and {{math|1='''F''' = ('''K''' '''I''')}}.)
Now let
:''Z'' = ('''C''' ('''C''' ('''B''' '''N''' ('''S''' '''I''' '''I''')) '''Ω''') '''I''')
now consider the term ('''S''' '''I''' '''I''' ''Z''). Does ('''S''' '''I''' '''I''' ''Z'') have a normal
form? It does if and only if the following do also:
:{{spaces|2}}('''S''' '''I''' '''I''' ''Z'')
:= ('''I''' ''Z'' ('''I''' ''Z''))
:= (''Z'' ('''I''' ''Z''))
:= (''Z'' ''Z'')
:= ('''C''' ('''C''' ('''B''' '''N''' ('''S''' '''I''' '''I''')) '''Ω''') '''I''' ''Z'') (definition of ''Z'')
:= ('''C''' ('''B''' '''N''' ('''S''' '''I''' '''I''')) '''Ω''' ''Z'' '''I''')
:= ('''B''' '''N''' ('''S''' '''I''' '''I''') ''Z'' '''Ω''' '''I''')
:= ('''N''' ('''S''' '''I''' '''I''' ''Z'') '''Ω''' '''I''')
Now we need to apply '''N''' to ('''S''' '''I''' '''I''' ''Z'').
Either ('''S''' '''I''' '''I''' ''Z'') has a normal form, or it does not. If it ''does'' have a normal form, then the foregoing reduces as follows:
:{{spaces|2}}('''N''' ('''S''' '''I''' '''I''' ''Z'') '''Ω''' '''I''')
:= ('''K''' '''Ω''' '''I''') (definition of '''N''')
:= '''Ω'''
but '''Ω''' does ''not'' have a normal form, so we have a contradiction. But
if ('''S''' '''I''' '''I''' ''Z'') does ''not'' have a normal form, the foregoing reduces as follows:
:{{spaces|2}}('''N''' ('''S''' '''I''' '''I''' ''Z'') '''Ω''' '''I''')
:= ('''K''' '''I''' '''Ω''' '''I''') (definition of '''N''')
:= ('''I''' '''I''')
:= '''I'''
which means that the normal form of ('''S''' '''I''' '''I''' ''Z'') is simply '''I''', another
contradiction. Therefore, the hypothetical normal-form combinator '''N''' cannot exist.
▲The combinatory logic analogue of [[Rice's theorem]] says that there is no complete nontrivial predicate. A ''predicate'' is a combinator that, when applied, returns either '''T''' or '''F'
{{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
Line 336 ⟶ 385:
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
:(EQUAL ''A B'') = '''T''' if ''A'' = ''B'' and
:(EQUAL ''A B'') = '''F''' if ''A'' ≠ ''B''.
| |||