[Agda] Non-termination help!

[Martín]

Hello Andreas,

Thank you very much for the quick response. As I told you I wanted to 
avoid sized types and after a bit we came up with another solution.

We use *Fin* datatype to represent N-Ary product instead of Vec.

     open import Data.Fin

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

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

     data µM (S : Signature) : Set where
       In : Σ S (µM S) -> µM S

     sumUp : {n : ℕ} -> (Fin n -> ℕ) -> ℕ
     sumUp {zero} f = zero
     sumUp {suc n} f =  f zero + sumUp λ x → f (suc x)

     size : {Sig : Signature} -> µM Sig -> ℕ
     size {Sig} (In (C , as)) = suc (sumUp λ x → size (as x))

Sadly I am a bit confused now. Why does this representation work? I know 
that *FIn* is an indexed type, but my guess is that I also have more 
power from the higher order function *as*. Basically the termination 
checker now sees that I am calling *size (as x)* with *as* being smaller 
than *In (C, as)*, am I correct?

Thank you again for your time!

Cheers,

Martín.

--

On 12/07/2017 05:29 AM, Andreas Abel wrote:
> 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
>
>