[Agda] proving termination trouble again

[Andreas Abel]

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