[TYPES] Expressivity of primitive recursion (was: Eliminators in type theory)

[Simone Martini]

I would like to make a side-remark on the thread on eliminators.

The thread focussed on what could be done
with higher-order types and the inductive type of natural
numbers.

In particular Seldin pointed out that Curry had a proof
that all primitive recursive functions get a type in a system
where Elim_Nat is used only with output of type Nat.
It would indeed be interesting to see if this restriction
could be enforced also for the representability of n-recursive  
functions,
since this is a huge class of functions, well beyond (first-order)  
primitive
recursion.

However, bounding the recursion rank is not the only way of limiting
the expressive power of higher-order recursion.

Another approach consists in tailoring the use of duplication, without
altering the higher-order nature of recursion. This has been  
investigated
for some time in fragments of Goedel's T
(e.g., by Hofmann, Bellantoni, Niggl, Schwichtenberg, etc.).

A recent paper by Ugo Dal Lago
(The geometry of linear higher-order recursion, in Lics 2005)
shows that the usual formulation of T, but with the contraction
restricted only to base types (natural numbers) exactly characterizes
first-order primitive recursion.

-sm
---------------------------------------------------
Simone Martini                          tel: +39 051 2094979
Universita' di Bologna                  fax: +39 051 2094510
Dip. di Scienze dell'Informazione
Mura Anteo Zamboni, 7
40127 Bologna BO                        www.cs.unibo.it/~martini
Italy