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

[Andreas Abel]

The trick here is to specialize the types of z<=n and s<=s to size  
infty.

data _≤_ : Rel (ℕ {∞}) where
z≤n : ∀              {n : ℕ {∞}}               → zero {∞}  
≤ n
s≤s : ∀  {m : ℕ {∞}} {n : ℕ {∞}} (m≤n : m ≤ n) → suc  
{∞} m ≤ suc {∞} n

Ideally, your implementation should also work, but in practice, there  
are problems because the size indices get in the way.

Cheers,
Andreas

-------------- next part --------------
A non-text attachment was scrubbed...
Name: ZilibowitzRubenHenner4.agda
Type: application/octet-stream
Size: 902 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100324/fc865cb6/ZilibowitzRubenHenner4.obj
-------------- next part --------------


On Mar 23, 2010, at 2:51 PM, Ruben Henner Zilibowitz wrote:

> Must be. I've switched back to 2.2.6 and it works there. I'm trying  
> to work with the sized Nat type, generalising everything in Data.Nat  
> to use sized types. Unfortunately I'm having some trouble getting  
> the antisym function written. Is this possible?
>
> data ℕ : {_ : Size} -> Set where
> zero : ∀ {size} → ℕ {↑ size}
> suc  : ∀ {size} → ℕ {size} → ℕ {↑ size}
>
> data _≤_ : Rel (ℕ {∞}) zero where
> z≤n : ∀ {sm sn}                {n : ℕ {sn}}               →  
> zero {sm} ≤ n
> s≤s : ∀ {sm sn} {m : ℕ {sm}} {n : ℕ {sn}} (m≤n : m ≤ n)  
> → suc {sm} m ≤ suc {sn} n
>
> antisym : Antisymmetric _≡_ _≤_
> antisym z≤n       z≤n       = {!!}
> antisym (s≤s m≤n) (s≤s n≤m) with antisym m≤n n≤m
> ...                         | refl = {!!}
>
> Ruben
>
> On 22/03/2010, at 9:57 AM, Andreas Abel wrote:
>
>> This must be a freshly introduced bug in Agda-2.2.7
>>
>> z : ∀ {size} → (n : Nat {↑ size}) → (zero {size} < n) →  
>> ∃ {Nat {size}} (λ m → m < n)
>> z {i} (zero .{i}) ()
>> z (suc n) _ = n , (≤-refl (suc n))
>>
>> produces the same error message
>>
>> size' != size of type Size
>> when checking that the pattern zero {.i} has type Nat {↑ size}
>>
>> It is completely obscure to me what size' should be, and why i is  
>> not mentioned instead.  Anyway, there should not be an error in the  
>> first place.
>>
>> Andreas
>>
>> On Mar 21, 2010, at 5:27 PM, Ruben Henner Zilibowitz wrote:
>>
>>> This is an old thread. Nevertheless I tried the file  
>>> ZilibowitzRubenHenner2.agda with stdlib 0.2 and it still didn't  
>>> work. Here is the error.
>>>
>>> ZilibowitzRubenHenner2.agda:38,3-7
>>> size' != size of type Size
>>> when checking that the pattern zero has type Nat
>>>
>>> Ruben
>>>
>>> On 18/01/2010, at 10:45 PM, Andreas Abel wrote:
>>>
>>>> That is an issue with universe polymorphism.
>>>> I am using stdlib 0.2 without uni poly.
>>>>
>>>> Probably there is just a level argument (to Rel) missing?!
>>>>
>>>> Cheers,
>>>> Andreas
>>>>
>>>> On Jan 17, 2010, at 12:24 AM, Ruben Henner Zilibowitz wrote:
>>>>
>>>>> Hi Andreas,
>>>>>
>>>>> Thanks, but it doesn't work. I'm using agda 2.2.6 with standard  
>>>>> lib 0.3 by the way.
>>>>>
>>>>> ZilibowitzRubenHenner2.agda:26,12-25
>>>>> (ℓ : .Level.Level) → Set (.Level._⊔_ .Level.zero  
>>>>> (.Level.suc ℓ))
>>>>> !=< _18 of type Setω
>>>>> when checking that the expression Rel (Nat {∞}) has type _18
>>>>>
>>>>> Ruben
>>>>>
>>>>> On 16/01/2010, at 12:07 PM, Andreas Abel wrote:
>>>>>
>>>>>> 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.
>>>>>>
>>>>>> <ZilibowitzRubenHenner2.agda>
>>>>>>
>>>>>> 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
>>>>>>
>>>>>>
>>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>>> 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
>>
>>
>>
>
>
>

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