[Agda] mutual recursion on vectors?

[Oleg Grenrus]

I can think of two options:
- using well founded recursion
- exposing constraint on the sum variable:

vecsum : {n : ℕ} → Vec ℕ n → ℕ

fn′ :  {n : ℕ} → (index : Fin n) → (vec : Vec ℕ n) → (sum : ℕ) → (vecsum vec ≡ sum)  → ℕ
fn′ = {!!} -- sum is decreasing argument

fn : {n : ℕ} → (index : Fin n) → Vec ℕ n → ℕ
fn index vec = fn′ index vec (vecsum vec) refl

Essentially both solutions are the same, as in well founded recursion you’ll calculate vecsum anyway.

> On 21 Jun 2015, at 09:05, Kenichi Asai <asai at is.ocha.ac.jp> wrote:
> 
> One can easily write a function that recurse over a natural number:
> 
> f1 : ℕ → ℕ
> f1 zero = zero
> f1 (suc x) = f1 x
> 
> Given an argument m, it returns zero after m recursive calls.  For two
> argument function, one can define:
> 
> mutual
>  f2a : ℕ → ℕ → ℕ
>  f2a zero zero = zero
>  f2a zero (suc y) = f2b zero y
>  f2a (suc x) y = f2a x y
> 
>  f2b : ℕ → ℕ → ℕ
>  f2b zero zero = zero
>  f2b (suc x) zero = f2a x zero
>  f2b x (suc y) = f2b x y
> 
> where f2a is called recursively when its first argument decreases
> (with the second argument unchanged), and f2b is called recursively
> when its second argument decreases (with the first argument unchanged).
> Given arguments m1 and m2, it returns zero after m1+m2 recursive calls.
> 
> Can I generalize this to n argument case?
> 
> fn : {n : ℕ} → (index : Fin n) → Vec ℕ n → ℕ
> fn {n} index v = {!!}
> 
> Namely, given an index and a vector of n numbers, it defines n
> functions mutually recursively.  fn i will be called recursively when
> its ith argument decreases (with all the other arguments unchanged).
> Given a vector of n numbers, m0, ..., m_{n-1}, it returns zero after
> m0 + ...  + m_{n-1} recursive calls.
> 
> It appears I can define it by adding an extra argument keeping the
> sum of all the numbers.  But then I lose the mutual recursive
> structure: even if sum is not zero, I don't know which of the n
> numbers is non zero, and even I have to have the case where all the
> numbers are zero, which can't happen if sum is zero.
> 
> Sincerely,
> 
> --
> Kenichi Asai
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150621/bb9c6cb6/signature.bin