[Agda] Non-termination help!

[Andreas Abel]

Martín,

a bit ironically, to define "size" you need "sized types". ;-)

The termination checker per se does not see that in the call

   map size as

function "size" will be only applied to arguments that are structurally 
smaller than "In (C , as)"; simply, because it cannot even "see" an 
argument to "size".

To help the termination checker, you need to index type \mu with a Size 
(built-in notion for an upper bound on the height).

   open import Size

   data µ (S : Signature) (i : Size) : Set where
     In : {j : Size< i} → Σ S (µ S j) -> µ S i

   size : ∀{i} {S : Signature} -> µ S i -> ℕ
   size (In (C , as)) = suc (sum (map size as))

Now "size" has an additional argument "i" which decreases in recursive 
calls.

Alternatively, you can define "size" mutually with a function "mapSize" 
which is an inling of the code for "map size".

Cheers,
Andreas

On 06.12.2017 14:56, Martín wrote:
> Hello everyone. I am struggling with Agda's termination checker.
> 
> The idea is to define a recursive function like *size* over terms µ S 
> for some signature S (definitions are bellow). I can destruct (t : µ S) 
> to obtain some symbol and its 'arguments', such arguments should be 
> smaller since µ S is strictly positive. Therefore, I should be able to 
> recursively call size, right?.
> 
> Here is an example where I leave the holes to be filled. I have tried 
> different approaches to help the termination checker such as views and 
> sized types. Sized types fix these simple functions, but it complicates 
> matters in further proofs.
> 
> Cheers,
> 
> Martín.
> 
> ----
> 
> module Q where
> 
> open import Data.Vec
> open import Data.Nat
> 
> open import Level renaming (zero to lzero ; suc to lsuc)
> 
> record Signature : Set (lsuc lzero) where
>    constructor sig
>    field
>      σ : Set
>      arity : σ -> ℕ
> 
> record Σ (Sig : Signature) (X : Set) : Set where
>    constructor _,_
>    field
>      C : Signature.σ Sig
>      as : Vec X (Signature.arity Sig C)
> 
> data µ (S : Signature) : Set where
>    In : Σ S (µ S) -> µ S
> 
> size : {S : Signature} -> µ S -> ℕ
> size (In (C , as)) = suc (sum (map {!size!} as))
> 
> size' : {S : Signature} -> µ S -> ℕ
> size' {sig σ arity} (In (C , as)) with arity C
> size' {sig σ arity} (In (C , [])) | zero = 0
> size' {sig σ arity} (In (C , (x ∷ as))) | suc arC = suc (sum (map 
> {!size'!} (x ∷ as) ))
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/
-------------- next part --------------

open import Size
open import Level renaming (zero to lzero ; suc to lsuc)

open import Data.Vec
open import Data.Nat

record Signature : Set (lsuc lzero) where
  constructor sig
  field
    σ : Set
    arity : σ -> ℕ

record Σ (Sig : Signature) (X : Set) : Set where
  constructor _,_
  field
    C : Signature.σ Sig
    as : Vec X (Signature.arity Sig C)

data µ (S : Signature) (i : Size) : Set where
  In : {j : Size< i} → Σ S (µ S j) -> µ S i

size : ∀{i} {S : Signature} -> µ S i -> ℕ
size (In (C , as)) = suc (sum (map size as))