I suppose the primitive recursive functions are supposed
to be those functions that provably terminate, is that right?

But there are functions that are not primitive recursive that provably
terminate.

I suppose the primitive recursive functions are supposed
to be those functions that provably terminate, is that right?
But there are functions that are not primitive recursive
that provably terminate.

It seems like the more useful approach would be just
to speak in terms of what provably terminates. That's
the important quality, is it not? For example, structurally
recursive functions provably always terminate, but I don't
see that they meet the definition of primitive recursive.
Any function with an algorithm that is recursive, has a
nonrecursive base case, and for which an order exists
for some subset of its arguments, such that recursive
invocations of the function (i.e., not the base case) uses
arguments that are strictly less than the previous invocation,
and whose domain is a set of elements greater than or
equal than the base case, provably terminates. This
is old hat stuff, but isn't covered by "primitive recursive."

(Also, is there any possible sense in which, say, a projection
function can be considered in any way "recursive"? I don't
see how. And yet it is "primitive recursive.")

On a related note, it seems that often the idea of totality
and termination are conflated. That seems wrong to me.
That a theorem prover may not return a result when asked
to prove a theorem is a very different case than a division
algorithm being asked to divide two arbitrary rational
numbers. Even though either one might fail to return a
value, in the first case you don't know if that's what's
happening, and in the second case you always do.

If I'm missing something, feel free to point and laugh,
only please be sure to tell me what it is I'm missing if
you do. Thanks.

Marshall

I suppose the primitive recursive functions are supposed
to be those functions that provably terminate, is that right?

But there are functions that are not primitive recursive
that provably terminate.

It seems like the more useful approach would be just
to speak in terms of what provably terminates. That's
the important quality, is it not?

For example, structurally
recursive functions provably always terminate, but I don't
see that they meet the definition of primitive recursive.

Any function with an algorithm that is recursive, has a
nonrecursive base case,

and for which an order exists
for some subset of its arguments, such that recursive
invocations of the function (i.e., not the base case) uses
arguments that are strictly less than the previous invocation,

and whose domain is a set of elements greater than or
equal than the base case, provably terminates. This
is old hat stuff, but isn't covered by "primitive recursive."

(Also, is there any possible sense in which, say, a projection
function can be considered in any way "recursive"? I don't
see how. And yet it is "primitive recursive.")

On a related note, it seems that often the idea of totality
and termination are conflated. That seems wrong to me.
That a theorem prover may not return a result when asked
to prove a theorem is a very different case than a division
algorithm being asked to divide two arbitrary rational
numbers. Even though either one might fail to return a
value, in the first case you don't know if that's what's
happening, and in the second case you always do.

MoeBlee wrote:

the
primitive recursive functions all have algorithms that require only a
"do for" loop and don't require a "do while" loop

I meant 'do until' not 'do while' there.

On May 7, 4:54 pm, MoeBlee <jazzm... at (no spam) hotmail.com> wrote:

the primitive recursive functions all have algorithms that require
only a "do for" loop and don't require a "do while" loop

I meant 'do until' not 'do while' there.

On Thu, 8 May 2008 09:46:45 -0700 (PDT), MoeBlee <jazzm... at (no spam) hotmail.com> said:

On May 7, 4:54 pm, MoeBlee <jazzm... at (no spam) hotmail.com> wrote:

the primitive recursive functions all have algorithms that require
only a "do for" loop and don't require a "do while" loop

I meant 'do until' not 'do while' there.

Either would do, no?  They differ slightly in behavior, but those
constructs are exactly equivalent in terms of computational strength.
Anything you can program in terms of the one you can program in terms of
the other.

Do you have any thoughts on my question about the notion of
'finitistic'. Why do people limit 'finitistic' to primitive recursive?
Why not take finitistic as anything total recursive?

On 2008-05-09, in sci.logic, MoeBlee wrote:

Do you have any thoughts on my question about the notion of
'finitistic'. Why do people limit 'finitistic' to primitive recursive?
Why not take finitistic as anything total recursive?

Because not all total recursive functions are recognisable as such by
finitistic principles.

The restriction to primitive recursive functions stems from the fact
that the principle of definition by primitive recursion is equivalent
to the principle of induction. Solely on basis of our basic
understanding of the naturals as what one obtains from 0 by repeatedly
applying the "add one"-operation the principle of induction and the
principle of definition by primitive recursive induction are equally
compelling. This is the reason for taking primitive recursive
arithmetic as the canonical formalisation for finitism; if we further
allow that properties definable from primitive recursive properties by
means of the usual logical operations of first-order logic --
including unrestricted quantification --, in effect accepting the
totality of the naturals as something determinate, we get PA.

--
Aatu Koskensilta (aatu.koskensi... at (no spam) xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

MoeBlee wrote:
MoeBlee wrote:

the primitive recursive functions all have algorithms that require
only a "do for" loop and don't require a "do while" loop

I meant 'do until' not 'do while' there.

"Do while X" = "Do until not-X".

On Thu, 08 May 2008 21:49:21 -0400, herbzet <herb... at (no spam) gmail.com> said:

I meant 'do until' not 'do while' there.

"Do while X" = "Do until not-X".

Well, yeah, 'cept if X is false, "Do while X" will skip the associated
procedure whilst "Do until not-X" will run through it once.

On 2008-05-10, in sci.logic, Chris Menzel wrote:
Well, yeah, 'cept if X is false, "Do while X" will skip the
associated procedure whilst "Do until not-X" will run through it
once.

That might well be. I'm not au courant on the intricacies of Pascal
and other such horrors of the programming language Pantheon.

MoeBlee's original point was, presumably, that primitive recursive
functions are those functions expressible in a programming language
with as its sole looping construct one that allows one to loop from n
to m, where m is a constant that must be determined prior to entering
the loop. That is, we can't have loping constructs of the kind "do
until condition X holds" or "do while condition X holds".

On May 11, 2:39 am, William Hale <h... at (no spam) tulane.edu> wrote:
In article
326dd4b2-5f53-45e8-a8dd-05e3d044e... at (no spam) w5g2000prd.googlegroups.com>,

Marshall <marshall.spi... at (no spam) gmail.com> wrote:
On May 10, 2:38 pm, Chris Menzel <cmen... at (no spam) remove-this.tamu.edu
wrote:
On Thu, 08 May 2008 21:49:21 -0400, herbzet <herb... at (no spam) gmail.com
said:

I meant 'do until' not 'do while' there.

"Do while X" = "Do until not-X".

Well, yeah, 'cept if X is false, "Do while X" will skip the
associated procedure whilst "Do until not-X" will run through it
once.

I'm feeling a bit of disorientation. We're talking Pascal
terminology now, right?

The above distinction between "do while" and "do until" applies not
only to Pascal, but to all the common programming languages.

Sure. Or anyway, the distinction between a loop construct that
executes at least once and one that doesn't is common. The Pascal-y
flavor of the choice of terms I still find disorienting, though.
Pascal as a thought-leader! It is as if I woke up and found that
teenagers now think John Wayne is cool.

On Thu, 08 May 2008 21:49:21 -0400, herbzet <herbzet at (no spam) gmail.com> said:
MoeBlee wrote:
MoeBlee wrote:

the primitive recursive functions all have algorithms that require
only a "do for" loop and don't require a "do while" loop

I meant 'do until' not 'do while' there.

"Do while X" = "Do until not-X".

Well, yeah, 'cept if X is false, "Do while X" will skip the associated
procedure whilst "Do until not-X" will run through it once.