[Agda] Non-termination help!

[Andreas Abel]

 > Basically the termination
 > checker now sees that I am calling *size (as x)* with *as* being smaller
 > than *In (C, as)*, am I correct?

Exactly!

And sumUp is defined by recursion on the hidden argument n.

--Andreas


On 07.12.2017 19:21, Martín wrote:
> 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
>>
>>
> 

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