[Agda] (no subject)

[Andrea Vezzosi]

On Wed, Jun 25, 2014 at 10:36 PM, Ernesto Copello <ecopello at gmail.com> wrote:
> [...]
> In fact, I want to know why I have to give explicit information about the
> size of the elements of D in R ? I belive that when no information was
> given, then ∞ size was assumed, and ∞ unificates with any size. So I don't
> understand the error : ∞ != .ι that gives Agda's compiler with the original
> version of R.

∞ doesn't unificate with any size, but for inductive types like D we
have that D {i} is a subtype of D {∞}.

if D {∞} were equivalent to any other D {j} then also D {i} and D {↑
i} would be equivalent to each other by transitivity, making sizes
useless.

Cheers,
Andrea

> Cheers,
> Ernesto
>
>
> On Wed, Jun 25, 2014 at 4:24 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
> wrote:
>>
>> Hi Ernesto,
>>
>> you can generalize R to speak about the sized version of D:
>>
>>   data R : ∀{i} → D {i} → D {i} → Set where
>>     r1 : ∀{i}(n : ℕ) → R {↑ i} (d1 n) (d1 n)
>>     r2 : ∀{i}(d : D) → R {i} (op d) (op d) → R {↑ i} (d2 d) (d2 d)
>>
>> Then the following function termination-checks:
>>
>>   ρ-good :  {ι : Size} → Reflexive (R {ι})
>>   ρ-good {x = d1 x} = r1 x
>>   ρ-good {x = d2 x} = r2 x (ρ-good {x = op x})
>>
>> Cheers,
>> Andreas
>>
>> On 25.06.2014 15:04, Ernesto Copello wrote:
>>>
>>>
>>> {-# OPTIONS --sized-types #-}
>>> module problem where
>>>
>>> open import Size
>>> open import Data.Nat
>>>
>>> open import Relation.Binary
>>> open import Relation.Binary.PropositionalEquality
>>>
>>> data D : {ι : Size} → Set where
>>>    d1 : {ι : Size} → ℕ → D {↑ ι}
>>>    d2 : {ι : Size} → D {ι} → D {↑ ι}
>>>
>>> -- d1 n, d2 (.. d2 (d1 n))
>>>
>>>
>>> postulate
>>>    op : {ι : Size} → D {ι} → D {ι}
>>>    pr : {x : D} → op x ≡ x
>>>
>>> -- Some reflexive binary relation
>>> data R : D → D → Set where
>>>    r1 : (n : ℕ) → R (d1 n) (d1 n)
>>>    r2 : (d : D) → R (op d) (op d) → R (d2 d) (d2 d)
>>>
>>>
>>> -- r1 (d1 n) (d1 n), r2 (r1 (d1 n) (d1 n))
>>>
>>> good : D → D
>>> good x with op x | pr {x}
>>> ... | .x | refl = x
>>>
>>> -- We are not able to do the same as above with size information
>>> annotations, the following commented code does not compile:
>>>
>>> -- problem : {ι : Size} → D {ι} → D
>>> -- problem x with op x | pr {x}
>>> -- ... | .x | refl = {! !}
>>>
>>> ρ-good : Reflexive R
>>> ρ-good {x = d1 x} = r1 x
>>> ρ-good {x = d2 x} = r2 x (ρ-good {x = op x})
>>>
>>> -- To pass the termination checking algorithm, we add size information to
>>> the type signature of the previous code, but another problem arises, and now
>>> the proofs do not pass type checking.
>>>
>>> ρ-problem : {ι : Size} → Reflexive {A = D {ι}} R
>>> ρ-problem {x = d1 x} = {! r1 x!}
>>> ρ-problem {x = d2 x} = {! r2 x (ρ-problem {x = op x})!}
>>>
>>
>>
>> --
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>> Department of Computer Science and Engineering
>> Chalmers and Gothenburg University, Sweden
>>
>> andreas.abel at gu.se
>> http://www2.tcs.ifi.lmu.de/~abel/
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>