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

Andreas Abel andreas.abel at ifi.lmu.de
Tue Sep 25 10:13:08 CEST 2012

```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/
```

More information about the Agda mailing list