[Agda] Re: Strict positivity and indices

[Andreas Abel]

A comment:  To accept \mu, it is sufficient to recognize that \cdot is 
strictly positive in its second argument.

I am a bit surprised that it is also s.pos. in its first argument.  The 
first argument is matched upon, so I'd given it mixed variance.  That 
makes me wonder what the meaning of "strictly positive" actually is.

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?

Cheers,
Andreas


On 14.05.12 1:17 PM, Nils Anders Danielsson wrote:
> On 2012-05-10 21:29, Stefan Monnier wrote:
> Take the following example:
>
> infixr 9 _·_
> infixr 2 _⊗_
> infixr 1 _⊕_
>
> -- Polynomial functors.
>
> data Functor : Set1 where
> Id : Functor
> K : (A : Set) → Functor
> _⊕_ _⊗_ : (F₁ F₂ : Functor) → Functor
>
> -- Functor application.
>
> _·_ : Functor → Set → Set
> Id · B = B
> K A · B = A
> (F₁ ⊕ F₂) · B = F₁ · B ⊎ F₂ · B
> (F₁ ⊗ F₂) · B = F₁ · B × F₂ · B
>
> -- Inductive types.
>
> data μ (F : Functor) : Set where
> inn : (x : F · μ F) → μ F
>
> Why is μ accepted? Take _·_, to start with. Agda computes and records
> the following information:
>
> * The first argument of _·_ occurs strictly positively in _·_.
> * The second argument of _·_ occurs strictly positively in _·_.
>
> When Agda later checks μ this information is used to deduce that μ F
> occurs strictly positively in μ.
>
> How is the information about _·_ computed? Agda builds a positivity
> graph, containing local information about where _·_ and its arguments
> are used (making use of previously computed information about _⊎_ and
> _×_). Global information is obtained by taking the transitive closure of
> this graph. See Agda.TypeChecking.Positivity for details.
>

-- 
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/