[Agda] Non-termination help!

[Martín]

Hello Gallais,

Exactly! I have to postulate functional extensionality in order to prove 
equality between these functions.

The good thing is that I just use it when proving that every Signature 
defines an endofunctor in Set.

ΣEndo : Signature -> Endofunctor (Sets lzero)
ΣEndo Sig = record { F₀ = Σ Sig
                    ; F₁ = λ { x (C , as) → C , λ x₁ → x (as x₁)}
                    ; homomorphism = ≣-refl
                    ; F-resp-≡ = λ{ x {C , as} → ≣-cong (λ y → C , y) 
(ext λ a → x {as a})} -- <- here it is!
                    ; identity = ≣-refl
             }

Thank you for your answer!

Cheers,
Martín

On 12/07/2017 03:56 PM, Guillaume Allais wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda