Demonstrating Church-Turing Completeness

[orcmid]

The demonstration of Church=Turing Completeness is accomplished in the Miser Project by demonstration that all ob-computable functions are representable via the functions obap.ap(p, x) and/or obap.eval(e).

This is demonstrated by cross-simulation.

1. One key case involve demonstration of computational representations of the combinatory logic primitives S and K along with other important well-known combinators, including a Y-combinator and also representation of Church's base type, o, on which separation of ob cases is accomplished., made applicative via the quasi-combinator Uβ with β a base type on ob serving as representation of Church's type o. It is important to notice that this representation is accomplished entirely with functions on obs representing scripts for [ and/or e above.
2. Another key case involves demonstration of simulation of all single-tape Turing Machines with a finite alphabet of marks and starting with a tape and a finite sequence of marks on the tape that is positioned at the start of the TM's operation. The demonstration consists of a function defined from the initial alphabet, a list of the individual state rules, and that operates on the given initial state with initial tape positioning over the first, if any, mark on the tape.
3. With regard to the structure ‹ob› itself, it is also the case that the obs are denumerable. This is easily demonstrated by offering a context-free grammar for canonical expression of every ob there is. Effective representation of the (computable) functions on ob is by construction. IN this respect, a recursive function theory over ‹ob› is established. This is does not completely wrap up CT-completeness until there is demonstration that Peano arithmetic and the basic structures of recursive function theory are represented. This is accomplished by representing twos-complement arithmetic and the simulation of all the number-theoretic functions that are employed in recursive-function theory.

These are all cases of representation/simulation. We do not require construction of simulations in the reverse direction. We assume that Church's thesis holds and we have not transcended it, simply coming up with one more case of representability and simulation.