[Agda] Non-termination help!

[Martín]

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

[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

Post by Martín
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
https://lists.chalmers.se/mailman/listinfo/agda

[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.

--

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

Post by Martín
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
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by 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.
--

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

Post by Martín
Hello everyone. I am struggling with Agda's termination checker.
The idea is to define a recursive function like *size* over terms µ
µ 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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by 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

Post by 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.
--

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

Post by Martín
Hello everyone. I am struggling with Agda's termination checker.
The idea is to define a recursive function like *size* over terms µ
µ 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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Andreas Abel]

Post by Martín
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

Post by 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.
--

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

Post by Martín
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
https://lists.chalmers.se/mailman/listinfo/agda