McCarthy 91 Function - History

History

The 91 function was introduced in papers published by Zohar Manna, Amir Pnueli and John McCarthy in 1970. These papers represented early developments towards the application of formal methods to program verification. The 91 function was chosen for having a complex recursion pattern (contrasted with simple patterns, such as defining by means of ). The example was popularized by Manna's book, Mathematical Theory of Computation (1974). As the field of Formal Methods advanced, this example appeared repeatedly in the research literature. In particular, it is viewed as a "challenge problem" for automated program verification.

Often, it is easier to reason about non-recursive computation. As one of the examples used to demonstrate such reasoning, Manna's book includes a non-recursive algorithm that simulates the original (recursive) 91 function. Many of the papers that report an "automated verification" (or termination proof) of the 91 function only handle the non-recursive version.

A formal derivation of the non-recursive version from the recursive one was given in a 1980 article by Mitchell Wand, based on the use of continuations.

Read more about this topic:  McCarthy 91 Function

Famous quotes containing the word history:

    Whenever we read the obscene stories, the voluptuous debaucheries, the cruel and torturous executions, the unrelenting vindictiveness, with which more than half the Bible is filled, it would be more consistent that we called it the word of a demon than the Word of God. It is a history of wickedness that has served to corrupt and brutalize mankind.
    Thomas Paine (1737–1809)

    To summarize the contentions of this paper then. Firstly, the phrase ‘the meaning of a word’ is a spurious phrase. Secondly and consequently, a re-examination is needed of phrases like the two which I discuss, ‘being a part of the meaning of’ and ‘having the same meaning.’ On these matters, dogmatists require prodding: although history indeed suggests that it may sometimes be better to let sleeping dogmatists lie.
    —J.L. (John Langshaw)

    The history of all hitherto existing society is the history of class struggles.
    Karl Marx (1818–1883)