[Agda] Non-termination help!

[Guillaume Allais]

Hi Martín,

This representation works because the subterm relationship between
`as` and `as x` is self-evident from Agda's point of view. However,
when you have a vector of subterms and you step through it via `map`,
you add one level of indirection which hides from Agda the fact that
the recursive calls are performed on direct subterms.

As Andreas said, the old-school solution to this issue is to write
a mutually defined `mapSize`, an inlined and specialised version of
`map` partially applied to `size`. And the modern approach to this
problem is to use sized types so that the *type* is explicit about
the fact that `map` doesn't do anything funky with the induction
hypothesis it is handed down.

You have demonstrated a third way which is to use the duality between
a finite data structure and its lookup function (or dually: between a
function with a finite domain and its tabulation). However this will
probably create some trouble whenever you want to prove things equal
(unless you're willing to postulate functional extensionality) because
vectors are much more permissive than functions when it comes to proving
them propositionally equal.

Cheers,
--
gallais

On 07/12/17 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
>>
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda