[Agda] Re: Strict positivity and indices

[Ulf Norell]

On Tue, May 15, 2012 at 2:29 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> On 05/15/2012 11:17 AM, Nils Anders Danielsson wrote:
>
>> On 2012-05-14 21:32, Andreas Abel wrote:
>>
>>> For instance in
>>>
>>> monus : Nat -> Nat -> Nat
>>> monus zero y = zero
>>> monus (suc x) zero = suc x
>>> monus (suc x) (suc y) = monus x y
>>>
>>> are both arguments strictly positive? And what does it mean then?
>>>
>>
>> Agda states that the first argument is used strictly positively, and
>> that the other one is unused.
>>
>> I don't know what this means (I didn't implement this feature, I only
>> optimised it).
>>
>
> Ah, ok so if you call
>
>  monus red green
>
> 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.
>
> 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.
>

Yes, although Sets can be embedded in terms and revealed by pattern
matching, which is why the positivity checker looks at patterns.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120516/39c43130/attachment-0001.html