# [Agda] Re: Strict positivity and indices

Andreas Abel andreas.abel at ifi.lmu.de
Mon May 14 21:32:59 CEST 2012

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/


More information about the Agda mailing list