Nuprl Definition : HofstadterM

This is an example of definition that uses mutual recursion
(see HofstadterF).

The two functions are called "married" functions by Douglas Hofstadter.

We prove a joint well-formedness lemma Error :Hofstadter_wf
from which we then derive the typing lemma Error :HofstadterM_wf.

We use explict callbyvalue in the definition because otherwise the
computation is extremely inefficient.
Even with callbyvalue, the recursion is inefficent without memoization.

The memoized version is given in Error :HofstadterL (see Error :HofstadterL_wf)⋅

HofstadterM(n) ==

  if (n) < (1)  then 0  else eval p = n - 1 in eval m = HofstadterM(p) in eval f = HofstadterF(m) in   n - f

Definitions occuring in Statement : HofstadterF: HofstadterF(n), callbyvalue: callbyvalue, less: if (a) < (b) then c else d, subtract: n - m, natural_number: $n
Definitions occuring in definition : less: if (a) < (b) then c else d, natural_number: $n, callbyvalue: callbyvalue, HofstadterF: HofstadterF(n), subtract: n - m
FDL editor aliases : HofstadterM

Latex:
HofstadterM(n) == if (n) < (1) then 0 else eval p = n - 1 in eval m = HofstadterM(p) in eval f = HofstadterF(m) in n - f Date html generated: 2018_05_21-PM-09_07_02 Last ObjectModification: 2018_01_13-PM-01_54_31 Theory : general Home Index