[Agda] Positivity checker

[Peter Dybjer]

So T is the operation which takes the type of ordinals of the nth  
number class to the type of ordinals of the n+1st number class. And  
then this operation is iterated transfinitely along some well- 
ordering. Type-theoretically, we would probably need to have a T which  
goes from all predecessors, what about

T : ((x : A) -> B x -> Set) -> Set
O : W A B-> Set

O (sup a b) = T(\x y -> O(b y))?

But wouldn't this still be within the world of strictly postiive data  
types? (Actually how would T be defined?)

Peter



On Dec 10, 2008, at 12:33 PM, Peter Hancock wrote:

> It occurred to me there *is* an inductive definition a bit like
> Wouter's which has been rather well studied, and exhibits what
> may be a similar kind of "negativity".
>
> In the 60's logicians began to study systems they called ID_{< alpha},
> where principle that takes you from A to T_A = mu X. 1 -> (A -> X)
> is iterated a transfinite number of times, along a given wellordering
> <, typically of order type w^w, or epsilon0.  So you would get a
> predicate O : (a:Nat) -> (b:Nat) -> Set, where the first argument a
> is really over the wellordering (here, coded in Nat), and the second b
> is for things that satisfy the predicate O(a,_).  The crucial
> thing is that the predicate O(a) is closed under some operation
> whose operand has type \all n : Nat. O(a',n) -> O(a,{f}n), where a'  
> < a.
> -- in that case one would have O(a,2^a*3^a'*5^f). [{f}(_) is Kleene
> application.]  Or something like that.
>
> Now this is a bit messy and old-fashioned, and it would need some  
> effort
> to present it in a manner palatable to you youngsters.  But I mention
> it in case someone (Peter?) will know what I am referring to, and can
> make that effort more quickly than me. (The papers I am
> thinking of straight off are by Feferman, Friedman, and are in the  
> 1968
> "Buffalo volume".)
>
> In those (pre-universe) days, people didn't have much problem in
> thinking of models of such (transfinitely iterated) g.i.d's.  But
> perhaps the justification for them was really in terms of a recursive
> definition along {<} into Set.
>
> Hank
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda