Compositional termination [Re: [Agda] Termination checking: valid or invalid]

[Andreas Abel]

Hi Wojciech,

funny you should ask the same question as recently posted on the bug tracker

   http://code.google.com/p/agda/issues/detail?id=695

The problem is that the current termination-check is non-compositional, 
i.e., you cannot abstract out expressions (like application in your 
case) without breaking the termination check.

In the contrary, type-based termination is compositional, so if you use 
sized types, your example checks.

I have picked up work on a smoother integration of sized types into Agda 
again, but for now, you have to do something manually:

{-# OPTIONS --sized-types #-}
module WojciechJedynakTermination where

open import Size

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

postulate
   A : Set

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

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

mirror : ∀ {i} → Tree {i} → Tree {i}
mirror leaf = leaf
mirror (node a fts) = node a (λ i → mirror (fts (reverse-fin i)))

-- works now:
mirror2 : ∀ {i} → Tree {i} → Tree {i}
mirror2 leaf = leaf
mirror2 (node a fts) = node a (λ i → mirror2 $ fts (reverse-fin i))

Cheers,
Andreas

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/