[Agda] proving termination trouble again

[Ruben Henner Zilibowitz]

Hi Andreas,

Below is a slightly simpler example. Function j does not termination check. Would you be so kind as to demonstrate how to use sized types to fix this?
I'm having some trouble figuring out how sized types are supposed to work exactly.

Thanks,
Ruben

-----------

module TerminationTwoConstructors where

open import Data.Nat
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Product

≤-refl : _≡_ ⇒ _≤_
≤-refl = IsPreorder.reflexive (IsPartialOrder.isPreorder (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder))))

z : (n : ℕ) → (0 < n) → ∃ (λ m → m < n)
z zero ()
z (suc n) _ = n , ≤-refl refl

j : ℕ -> ℕ
j zero = zero
j (suc n) = helper (suc n) (z (suc n) (s≤s z≤n))
  where
  helper : (sn : ℕ) -> ∃ (λ n → n < sn) -> ℕ
  helper sn (n , _) = j n

On 12/01/2010, at 8:41 PM, Andreas Abel wrote:

> Hi Ruben,
> 
> from the perspective of the termination checker, there is no difference in g and h.  The proofs of equality/leq are not used by the termination checker, it only honors structural ordering.  It "sees" that
> 
>   sn < suc (suc n)
> 
> by composing the calls g --> helper --> g.
> 
> For function i to termination check, it would have to evaluate proj_1 whee, but the termination checker does not do any evaluation (since evaluation (1) is safe only after termination checking, and (2) leads to unfeasible termination checking (see the Coq guardedness checker)).
> 
> If you want to propagate termination arguments (like sn < ssn) through functions and data structures, you need more informative typing, like sized types.
> 
> Cheers,
> Andreas
> 
> On Jan 11, 2010, at 2:24 PM, Ruben Henner Zilibowitz wrote:
> 
>> In relation to issue 59:
>> 
>> http://code.google.com/p/agda/issues/detail?id=59&can=1&q=termination
>> 
>> Here is another problem I've encountered along similar lines. In the code below, the functions f, g, h, and i all are in principal the same. However, only g and h pass the termination checker. Function f suffers from the problem in issue 59. Function g solves it with the same workaround suggested in issue 59. Function h solves it in a similar way. The problem is function i. It is very similar to function h but the argument (sn < ssn) in the helper function is concealed inside a product type and needs to be extracted using proj₂ which breaks this example. Is this a bug? Sorry for the hard to read code and function names..
>> 
>> The code below is based on Andreas Abel's earlier example..
>> 
>> Ruben
>> 
>> ----------
>> 
>> module TerminationTwoConstructors where
>> 
>> open import Data.Nat
>> open import Relation.Binary
>> open import Relation.Binary.PropositionalEquality
>> open import Data.Product
>> 
>> bla : ℕ -> ℕ
>> bla m = m
>> 
>> f : ℕ -> ℕ
>> f zero = zero
>> f (suc zero) = zero
>> f (suc (suc n)) with bla (suc (suc n))
>> ... | m = f (suc n)
>> 
>> g : ℕ -> ℕ
>> g zero = zero
>> g (suc zero) = zero
>> g (suc (suc n)) = helper (suc (suc n)) (suc n) refl (bla (suc (suc n)))
>>  where
>>  helper : (ssn : ℕ) -> (sn : ℕ) -> (suc sn ≡ ssn) -> (m : ℕ) -> ℕ
>>  helper ssn sn _ m = g sn
>> 
>> ≤-refl : _≡_ ⇒ _≤_
>> ≤-refl = IsPreorder.reflexive (IsPartialOrder.isPreorder (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder))))
>> 
>> h : ℕ -> ℕ
>> h zero = zero
>> h (suc zero) = zero
>> h (suc (suc n)) = helper (suc (suc n)) (suc n) (≤-refl refl) (bla (suc (suc n)))
>>  where
>>  helper : (ssn : ℕ) -> (sn : ℕ) -> (sn < ssn) -> (m : ℕ) -> ℕ
>>  helper ssn sn _ m = h sn
>> 
>> zog : (n : ℕ) -> (ℕ × n < suc n)
>> zog n = n , ≤-refl refl
>> 
>> i : ℕ -> ℕ
>> i zero = zero
>> i (suc zero) = zero
>> i (suc (suc n)) = let whee = zog (suc n) in helper (suc (suc n)) (proj₁ whee) (proj₂ whee) (bla (suc (suc n)))
>>  where
>>  helper : (ssn : ℕ) -> (sn : ℕ) -> (sn < ssn) -> (m : ℕ) -> ℕ
>>  helper ssn sn _ m = i sn
> 
> Andreas ABEL
> INRIA, Projet Pi.R2
> 23, avenue d'Italie
> F-75013 Paris
> Tel: +33.1.39.63.59.41
> 
> 
>