<div dir="ltr"><div><div><div>Thanks very much for your quick response !<br><br></div>Ok
I need to generalize R to the sized version of D. But don't you think the next
version of R is more specific ?<br><div class="im">
<br>data R : D → D → Set where<br></div> r1 : ∀{i}(n : ℕ) → R (d1 {i} n) (d1 {i} n)<br> r2 : ∀{i}(d : D {i}) → R (op d) (op d) → R (d2 d) (d2 d)<br><br></div><div>I already check that this version works too.<br></div>
<div><br>I understand your version indirectly size the elements of D, sizing the elements of R. While in this version I only size D elements not the hole relation R. In this example only D must
be sized, because of I am doing induction in the length of D, not R. <br><br></div><div>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.<br>
</div><div><br></div>Cheers,<br></div>Ernesto</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jun 25, 2014 at 4:24 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ernesto,<br>
<br>
you can generalize R to speak about the sized version of D:<br>
<br>
data R : ∀{i} → D {i} → D {i} → Set where<br>
r1 : ∀{i}(n : ℕ) → R {↑ i} (d1 n) (d1 n)<br>
r2 : ∀{i}(d : D) → R {i} (op d) (op d) → R {↑ i} (d2 d) (d2 d)<br>
<br>
Then the following function termination-checks:<br>
<br>
ρ-good : {ι : Size} → Reflexive (R {ι})<br>
ρ-good {x = d1 x} = r1 x<br>
ρ-good {x = d2 x} = r2 x (ρ-good {x = op x})<br>
<br>
Cheers,<br>
Andreas<br>
<br>
On <a href="tel:25.06.2014%2015" value="+12506201415" target="_blank">25.06.2014 15</a>:04, Ernesto Copello wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
{-# OPTIONS --sized-types #-}<br>
module problem where<br>
<br>
open import Size<br>
open import Data.Nat<br>
<br>
open import Relation.Binary<br>
open import Relation.Binary.<u></u>PropositionalEquality<br>
<br>
data D : {ι : Size} → Set where<br>
d1 : {ι : Size} → ℕ → D {↑ ι}<br>
d2 : {ι : Size} → D {ι} → D {↑ ι}<br>
<br>
-- d1 n, d2 (.. d2 (d1 n))<br>
<br>
<br>
postulate<br>
op : {ι : Size} → D {ι} → D {ι}<br>
pr : {x : D} → op x ≡ x<br>
<br>
-- Some reflexive binary relation<br>
data R : D → D → Set where<br>
r1 : (n : ℕ) → R (d1 n) (d1 n)<br>
r2 : (d : D) → R (op d) (op d) → R (d2 d) (d2 d)<br>
<br>
<br>
-- r1 (d1 n) (d1 n), r2 (r1 (d1 n) (d1 n))<br>
<br>
good : D → D<br>
good x with op x | pr {x}<br>
... | .x | refl = x<br>
<br>
-- We are not able to do the same as above with size information annotations, the following commented code does not compile:<br>
<br>
-- problem : {ι : Size} → D {ι} → D<br>
-- problem x with op x | pr {x}<br>
-- ... | .x | refl = {! !}<br>
<br>
ρ-good : Reflexive R<br>
ρ-good {x = d1 x} = r1 x<br>
ρ-good {x = d2 x} = r2 x (ρ-good {x = op x})<br>
<br>
-- 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.<br>
<br>
ρ-problem : {ι : Size} → Reflexive {A = D {ι}} R<br>
ρ-problem {x = d1 x} = {! r1 x!}<br>
ρ-problem {x = d2 x} = {! r2 x (ρ-problem {x = op x})!}<br>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br></div>