[Agda] Re: Strict positivity and indices

[Andreas Abel]

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.

Summing up, a function f green = rhss is strictly positive in green if 
no green stuff ends up to the left of an arrow on the rhss.
A function f red = rhss has an 'unused' argument red if no red stuff 
ends up on a rhs of f.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/