Talk:Primitive recursive functional

Isolationistic arithmetic[edit]

What is it? Thanks, Bill Wvbailey (talk) 14:45, 17 May 2009 (UTC)[reply]

It was supposed to be "intuitionistic". Either I drifted off when typing, or my spell checker was confused. — Carl (CBM · talk) 14:50, 17 May 2009 (UTC)[reply]

higher-type computability[edit]

"In recursion theory, the primitive recursive functionals are an example of higher-type computability, as primitive recursive functions are examples of Turing computability."

Is that right? It looks like all the functionals described in the article are Turing-computable, though I guess not primitive recursive. 69.228.171.150 (talk) 12:19, 9 November 2009 (UTC)[reply]

An object of type (1→1)→1 cannot possibly be Turing computable in the literal sense. Type 1 objects are elements of ω^ω, so an object of type (1→1)→1 takes an arbitrary function from ω^ω to ω^ω and returns an element of ω^ω. There is no way to feed an arbitrary function from ω^ω to ω^ω into a Turing machine, because in general such functions require an uncountable amount of information to represent.

It is true, on the other hand, that the collection of primitive recursive functionals described in the article right now is very weak, and in particular any function of type 0→0 will be primitive recursive in the usual sense. More strength would be gained if you add the ability to do more complicated recursions (although then I am not certain the functions would be called primitive recursive). — Carl (CBM · talk) 13:26, 9 November 2009 (UTC)[reply]

But the system doesn't seem to contain arbitrary functions from ω^ω to ω^ω. It only contains the ones constructable from the type 0 objects and some recursive combinators. Or do you mean the notion of a primitive recursive functional is different in recursion theory than in the type-theoretic definition given further down? It would be good to say so explicitly in that case. 69.228.171.150 (talk) 23:55, 9 November 2009 (UTC)[reply]

Even in the type theoretic definition, it follows from the definitions that, for example, the functional A of type (1×(1 → 1))→1 defined by (λ x¹,y^1->1 . y(x)) is a primitive recursive functional. However, there is no way in general to pass a functional of type 1→1 to a Turing machine, so there is no way to say that A is Turing computable even though A is very simple.

It is true that the collection of higher-type primitive recursive functionals (as defined in this article) is very limited, but it still goes beyond what can be done with a Turing machine for trivial reasons such as uncountability. — Carl (CBM · talk) 01:08, 10 November 2009 (UTC)[reply]

PS I do agree there is much more that could be added to this article – of course. It is just a stub right now, which can obscure things due to lack of complete coverage. — Carl (CBM · talk) 01:17, 10 November 2009 (UTC)[reply]

But the functionals of type 1→1 are not an uncountable domain under the article's definition. The only functionals of that type that actually exist in the system the ones constructable through recursive operations from lower type objects. That limited class is all computable. There are lots of (uncountably many) functions f:ω→ω, including some partial-recursive but still Turing-computable ones, that might exist in set theory but that the system described in the article simply does not contain, so an encoding of A doesn't have to worry about the unconstructable inputs. Am I making sense? I'm sorry if this seems to be going around in circles. 69.228.171.150 (talk) 01:34, 10 November 2009 (UTC)[reply]

I think I see what the issue is now. A primitive functional of type 1→1 does not just take primitive recursive functionals as arguments. A functional of type ρ→τ is a function from the set of all objects of type ρ that returns objects of type τ. A primitive recursive functional is, first and foremost, a functional. It just happens to be a functional that is definable using a particular small set of creation rules. So, for example, in the fifth bullet of the article, I was thinking of R(f,g) as a primitive recursive functional of type 0→τ that is defined using the "parameters" f and g. The way you are looking at it, you want to think of R as a primitive recursive functional of type τ→(0→τ→τ)→0→τ.

Now I see that the article is not very clear about this at all (it is a stub, after all). I will try to fix it over the next week. — Carl (CBM · talk) 01:54, 10 November 2009 (UTC)[reply]

OK, that explains it. Thanks! 69.228.171.150 (talk) 01:56, 10 November 2009 (UTC)[reply]

preprint[edit]

arXiv:1011.6353 looks interesting, if not for this article then maybe for some related one. 71.141.88.54 (talk) 02:21, 28 February 2011 (UTC)[reply]

System T?[edit]

Shouldn't the page be linked from System T and from Dialectica interpretation, and the text being more explicit on the System T terminology for primitive recursive functional? It should also probably itself link to Ackermann function. Hugo Herbelin (talk) 22:15, 10 February 2013 (UTC)[reply]