The Coq mailing list

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

I did try this, but then we run into a problem in a predicative setting. If nat is polymorphic in Type_n, then (nat -> nat) has type Type_{n+1}, so one can't do the application "m (nat -> nat)". Indeed, by defining nat in Prop this works just fine.

On Thu, Feb 14, 2013 at 7:42 AM, Colm Bhandal <bhandalc AT tcd.ie> wrote:

Try this:

Definition next (u : nat) (f : nat -> nat -> nat) (n m : nat) : nat :=
  m (nat -> nat) (f n) u.

Here, u is the right unit of f, f is the lower order function, and n, m are the arguments to the higher order function. So for example:

Definition mult := next 0 plus.

Where 0 := fun X f x => x

Expanded out this is:

fun n m => m (nat -> nat) (plus n) 0.

Not sure if this will work but it's an idea.

On 13 February 2013 20:50, Arthur Azevedo de Amorim <arthur.aa AT gmail.com> wrote:

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

--
Arthur Azevedo de Amorim