Sized Types [Re: [Agda] proving termination trouble again]
Ruben Henner Zilibowitz
rzilibowitz at yahoo.com.au
Tue Mar 23 06:51:31 CET 2010
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
>
>
>
More information about the Agda
mailing list