<br><div class="gmail_quote">On Tue, May 15, 2012 at 2:29 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">
<div class="im">On 05/15/2012 11:17 AM, Nils Anders Danielsson wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On 2012-05-14 21:32, Andreas Abel wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
For instance in<br>
<br>
monus : Nat -> Nat -> Nat<br>
monus zero y = zero<br>
monus (suc x) zero = suc x<br>
monus (suc x) (suc y) = monus x y<br>
<br>
are both arguments strictly positive? And what does it mean then?<br>
</blockquote>
<br>
Agda states that the first argument is used strictly positively, and<br>
that the other one is unused.<br>
<br>
I don't know what this means (I didn't implement this feature, I only<br>
optimised it).<br>
</blockquote>
<br></div>
Ah, ok so if you call<br>
<br>
monus red green<br>
<br>
where red is a natural number expressions painted red and green is a Nat painted green, then the result will not contain any green stuff, it will only contain red stuff and stuff added by the right hand sides.<br>
<br>
This looks sound when we are only interested in positivity of Set arguments. Since Set arguments cannot be taken apart by matching, they can only travel to the right hand side as a whole. Thus, the coloring semantics seems appropriate.<br>
</blockquote><div><br></div><div>Yes, although Sets can be embedded in terms and revealed by pattern matching, which is why the positivity checker looks at patterns.</div><div><br></div><div>/ Ulf </div></div>