[Agda] Relaxing the strict positivity requirement

[Andreas Abel]

Hello Daniel,

first of all, I think it is not inconsistent, because you have already 
given it a semantics in terms of recursion.  You can even define Context 
by recursion over a natural number (its length).

Second, your suggestion to use the termination checker on inductive 
families comes natural if you understand inductive families as being 
defined by recursion over some suitably large enough ordinal in the 
first place.  Then also, the inductive-inductive-coinductive-recursive 
jungle disappears.

Of course, I am aware that induction-recursion is proof-theoretically 
stronger than just inductive types.  (So, if you want to build your 
ordinals constructively, they might come in handy.)  However, inductive 
*families* add no proof-theoretic strength, they are just convenience.

To find sound rules for a relaxed positivity checker, I propose the 
following road map:

- describe mutual induction-coinduction-recursion in terms of sized types
- translate them to just mutual recursion over suitable ordinals
- termination check the translated definitions

I could do that formally if MiniAgda already had bounded existentials...

Cheers,
Andreas

On 12/6/11 7:58 PM, Daniel Peebles wrote:
> Hi all,
>
> I was fooling around with the usual inductive-recursive dependent
> context construction the other day:
>
> |module  Envwhere
>
> open  import  Data.Unit
> open  import  Data.Nat
> open  import  Data.Finhiding  (_+_)
> open  import  Data.Vechiding  (lookup)
> open  import  Data.Product
>
> mutual
>    data  Context  :Set₁where
>      ε   :Context
>      _,_ : (Γ :Context) (S  :Env  Γ →Set) →Context
>
>    Env  :Context  →Set
>    Env  ε = ⊤
>    Env  (Γ ,S) = Σ (Env  Γ)S
>
> I then wondered if I could make it inductive-inductive, because we love inductive families around here:
> |   data  Context′ :Set₁where
>      ε   :Context′
>      _,_ : (Γ :Context′) (S  :Env′ Γ →Set) →Context′
>
>    data  Env′ :Context′ →Set₁where
>      ε   :Env′ ε
>      _,_ : ∀ {ΓS} (xs :Env′ Γ) (x :S  xs) →Env′ (Γ ,S)
 >
> |But unfortunately, Agda (correctly) rejects this definition as not
> being strictly positive, because |Env′ carries its Context′ index in an
> implicit parameter and that appears in a negative position in Context′.
> This type does, however, "feel" quite safe. I have a feeling my feeling
> of safety comes from the fact that the index is structurally decreasing,
> but I can't really put my finger on it. I spoke to Ulf on IRC about it
> and he said he had a similar feeling, and other instances of the same
> kind of pattern arose with a HOAS AST for the STLC.
>
> Anyway, I was wondering if anyone knew of any work on relaxing the
> strict positivity requirement and giving it a bit more of a "structural
> recursion" flavor so the above definition could typecheck. I'd also be
> interested to hear if the definition is actually unsafe (i.e., someone
> turns off positivity checking and can prove false using that type).


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