The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Thanks a lot Andreas, I will definitely have a look.

On Thu, Feb 14, 2013 at 5:28 AM, Andreas Abel <andreas.abel AT ifi.lmu.de> wrote:

Hello Arthur,

you can find an answer in the work of Leivant.  Quoting from http://ndanner.web.wesleyan.edu/personal/cv/papers.html

 In [D. Leivant, Finitely stratified polymorphism, Information and Computation, 93(1):93–114, 1991] one of the authors showed that when type abstraction in that calculus is stratified into levels, the definable numeric functions are precisely the super-elementary functions (level 4in the Grzegorczyk Hierarchy).

Cheers,
Andreas

Am 13.02.2013 21:50, schrieb Arthur Azevedo de Amorim:

I was playing a little bit with predicative Church numerals

Definition nat := forall X : Type, (X -> X) -> X -> X.

Some functions are easy to define...

Definition plus (n m : nat) : nat :=

  fun X f x => n X f (m X f x).

Definition mult (n m : nat) : nat :=

  fun X f x => n X (m X f) x.

Definition exp (n m : nat) : nat :=

  fun X f x => m (X -> X) (n X) f x.

... However, when trying to go one level up and code a tower of
exponentials, I got stuck. Can it be done at all with a predicative
encoding?

--
 Arthur Azevedo de Amorim

--
Andreas Abel  <><     Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/

--
Arthur Azevedo de Amorim