In 1936, Post developed, independently of
Alan Turing, a mathematical model of computation that was essentially equivalent to the
Turing machine model. Intending this as the first of a series of models of equivalent power but increasing complexity, he titled his paper
Formulation 1. This model is sometimes called "Post's machine" or a
Post–Turing machine, but is not to be confused with
Post's tag machines or other special kinds of
Post canonical system, a computational model using
string rewriting and developed by Post in the 1920s but first published in 1943. Post's rewrite technique is now ubiquitous in programming language specification and design, and so with
Church's
lambda calculus is a salient influence of classical modern logic on practical computing. Post devised a method of 'auxiliary symbols' by which he could canonically represent any Post-generative language, and indeed any
computable function or
computable set at all. Correspondence systems were introduced by Post in 1946 to give simple examples of
undecidability. He showed that the
Post correspondence problem (PCP) of satisfying their constraints is, in general, undecidable. The undecidability of the correspondence problem turned out to be exactly what was needed to obtain undecidability results in the theory of
formal languages. In an influential address to the
American Mathematical Society in 1944, he raised the question of the existence of an uncomputable
recursively enumerable set whose
Turing degree is less than that of the
halting problem. This question, which became known as
Post's problem, stimulated much research. It was solved in the affirmative in the 1950s by the introduction of the powerful
priority method in
computability theory. ==Polyadic groups==