[Agda] how to count 0..n-1

[Nils Anders Danielsson]

On 2011-02-11 17:44, gallais @ EnsL.org wrote:
> I ended up defining a more powerful map function which is actually quite
> convenient (not only to define allFin) and which is able to generate allFin
> more efficiently.

Are you sure that allFin′ is (asymptotically) more efficient than
allFin? Your algorithm can be seen as building up the functions

   λ p → p
   λ p → (λ p → p) (suc p)
   λ p → (λ p → (λ p → p) (suc p)) (suc p)
   ⋮

(ignoring the unused arguments) and then applying all these functions to
zero. Usual reduction strategies do not involve reduction under lambdas,
so under such a strategy normalisation of the n-th function application
requires O(n) reductions.

With reduction under lambda one could arrive at the following sequence
of functions instead, at the cost of one extra reduction per function:

   λ p → p
   λ p → suc p
   λ p → suc (suc p)
   ⋮

Applications of these functions to values normalise using a single
reduction.

-- 
/NAD