
Peter Gammie wrote:
What I want: a class of functions that don't all terminate, don't all not terminate, and furthermore I can tell how a given element of the class will behave without running it. It must have at least some expressiveness; this is up for grabs, but it'll have to encompass at least primitive recursion to be interesting.
Let us consider a first-order language of functions defined with the help of addition, multiplication, branching-on-zero, and NPFIX. Functional applications are allowed provided they use the names of previously defined functions. (NPFIX n) is the n-th Church numeral (aka fold) NPFIX n f seed --> f (f ... (f seed)) n times (n>=0) seed otherwise The second argument of NPFIX is the name of a previously defined function (a known name, a functional constant). The domain of our functions consists of integers and a special value 'undefined' (to be called NaN for short). The reduction rules are as usual, with an addition NaN + x -> NaN + x for any x, etc. That is, any operation with NaN leads to non-termination. The language obviously includes every primitive recursive function. There are terminating expressions (any expression that never directly or indirectly mentions NaN always terminates). There are obviously non-terminating functions, such as f(x) = x + NaN. It is also clear that the halting predicate for our language is decidable. Given an expressing, we examine it and the body of all involved functions. If we don't find any NaN, we yield TRUE. If we find a NaN, we "abstractly" interpret our expression. That is, we execute it step by step until we come across a step that tries to add, compare, multiply NaN. At this point we yield FALSE. If our abstract interpreter halts, we yield TRUE. Obviously our abstract interpreter is just the concrete interpreter with one small change. Because any sequence of NaN-free reductions in our language is a sequence of reductions for some primitive recursive function, such sequence must terminate. We're a bit running afoul of the requirement:
I can tell how a given element of the class will behave without running it
but then, a decision procedure must take some 'deciding', so to speak -- if it is non-trivial. We must have a deciding machine. In our example, the deciding machine is the original machine with a slight modification.
participants (1)
-
oleg@pobox.com