[Agda] Termination checking: valid or invalid

Wojciech Jedynak wjedynak at gmail.com
Tue Sep 25 01:24:32 CEST 2012

Hello everybody,

I'm attaching a small example function on rose trees implemented using
a function instead of a list of subtrees. The 'mirror' function is
written in two flavors and only the first one passes termination
checking. Should the second version be accepted as well?
I'm using the Darcs Agda from a few days ago.



module Question where

open import Data.Nat
open import Data.Fin
open import Function
open import Data.Vec

  A : Set

data Tree : Set where
  leaf : Tree
  node : A → {n : ℕ} → (Fin n → Tree) → Tree

-- find the "complement" of the given i
reverse-fin : ∀ {n} → Fin n → Fin n
reverse-fin i = lookup i (reverse (allFin _))

-- passes termination checking
mirror : Tree → Tree
mirror leaf = leaf
mirror (node a fts) = node a (λ i → mirror (fts (reverse-fin i)))

-- fails termination checking
mirror2 : Tree → Tree
mirror2 leaf = leaf
mirror2 (node a fts) = node a (λ i → mirror2 $ fts (reverse-fin i))


More information about the Agda mailing list