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

[Andreas Abel]

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