Sized Types [Re: [Agda] proving termination trouble again]

[Andreas Abel]

Hi Ruben,

here is a translation of your code into something very similiar that  
uses a sized type of natural numbers.  Unfortunately, sized types are  
not well integrated into Agda yet, so a sizes have to be declared  
explicitely, and the standard library, which does not use sized types,  
is not usable.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: ZilibowitzRubenHenner2.agda
Type: application/octet-stream
Size: 1376 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100116/64460f23/ZilibowitzRubenHenner2.obj
-------------- next part --------------


A few things you need to know:
- Unspecified sizes default to \infty.  For instance, "Nat" is really  
"Nat {\infty}"
- The successor \uparrow is not a constructor, it cannot be matched,  
but it can appear in dot-patterns.
- Things are a bit fiddly, so I had to try a bit which sizes I need to  
mention explicitly and which can be inferred sensibly.
- It is advisable to turn on hidden arguments to see where stuff fails.

If you look at the example where I made sizes more explicit, you see  
that the mutual functions j and helper terminate on the first argument  
"size".  It is decreasing in the call j-->helper and unchanged in the  
call back.

j : ? {size} ? Nat {size} -> Nat
j zero = zero
j .{? size} (suc {size} n) = helper {size} (suc n) (z (suc n) (s?s  
z?n))
  where
  helper : {size : Size} -> (sn : Nat {? size}) -> ? {Nat {size}}  
(? n ? n < sn) -> Nat
  helper {size} sn (n , _) = j {size} n

Hope that helps,
Cheers,
Andreas

On Jan 16, 2010, at 12:25 AM, Ruben Henner Zilibowitz wrote:

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

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41