Nuprl Definition : HofstadterF
This is an example of definition that uses mutual recursion
(see Error :HofstadterM).
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 :HofstadterF_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).⋅
HofstadterF(n) ==
if (n) < (1) then 1 else eval p = n - 1 in eval f = HofstadterF(p) in eval m = HofstadterM(f) in n - m
Definitions occuring in Statement :
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,
subtract: n - m
FDL editor aliases :
HofstadterF
Latex:
HofstadterF(n) ==
if (n) < (1)
then 1
else eval p = n - 1 in
eval f = HofstadterF(p) in
eval m = HofstadterM(f) in
n - m
Date html generated:
2018_05_21-PM-09_06_47
Last ObjectModification:
2018_01_13-PM-01_52_54
Theory : general
Home
Index