The Coq mailing list

["Lukasz Stafiniak" <l_stafiniak AT hoga.pl>]

 Hi List! This will be my first scientific publication :)

        Extending CIC to incorporate recursive calls guarding at type
        level.

The idea is to extend CIC constructs to represent the relation of
being structuraly smaller. For example, one can introduce a subclass
of the product types, marked with a tag <decreasing>. An expresion of
such type will "type-check" - be properly typed - iff the body of
abstraction will be recognized as structurally smaller than the
argument. A function will be called "decreasing with respect to ith
argument", if ith product of its type is marked <decreasing>. (Such
function is thus a destructor of its ith argument). (It seems that
function can be "decreasing" with respect to only one argument). Each
type will be annotated with information - subtyping - whether values
of that type are (forced to be) structurally smaller than given value
(denoted by term) from the context. Lets denote <decreasing> product
of a:T and U by (a:T)>>U, and restriction (annotation) of U to be
structrally smaller than a by U<<a, then we have (<<a means assuming
that a belongs to the context):

(R1) T : (Type i); U<<a : (Type j) |- (a:T)>>U : (Type k), i,j <= k

(for sorts Set and Prop accordingly) (decreasing function),

(R2) T : Sort; U<<a : Sort |- ((x:T)U)<<a : Sort,

(R3) T : Sort; ((x:T)U)<<a : Sort |- U<<a : Sort, x =/= a,

(R4) x : (b:T)>>U; a:T |- (x a) : U<<a (preservation through
                                       decreasing function),

(R5) b : U<<a; c : U<<b |- c : U<<a (transitivity),

(R6) (a bit tough to formulate formally due to elimination
     restrictions): if x is a pattern variable of type T inside Cases
     c of f1 ... fn then x:(T<<c)

(R7) Recursive call restriction: each recursive function specifies
     which is its decreasing argument (not the function is decreasing,
     but the argument); say we call fi (with decreasing argument no
     ki) from fj (with decreasing argument named xj): then the type of
     ki-th argument applied to fi should be of the form T<<xj

In R7 the type restriction is not at abstraction time, but at
application time, so it is still not-that-type-theoretic. Yet, the
presented concept seems much better than being prone to unpleasant
surprises after the "Subtree proved!" communicate has put us into good
mood. We will not need to worry about the order of eliminations, we
will see which functions can be applied to our decreasing arguments so
that they actually decrease, the automation tactics will be more
powerful with applying functions recursively.

I have just read in the archive an Eduardo Gimenez letter about the
matter. Maybe when such type-annotations are nicely implemented the
time consumption decreases enough to allow immediate checking of
recursive-calls arguments (even without making it type-theoretic and
transparent to the user)? And, all in all, is it better to dwell into
the generated recursion "procedures" _ind, _rec, _rect, and avoid Fix
tactic? The Fix tactic seems more direct to me. It fits into
"programming-by-tactics" paradigm ;)

Is there a research on this topic related to Coq system?

Best Regards and waiting to hear from you,
Lukasz S.

------------------------------------------------------------
Dwie ksi±¿ki po 5 z³ + jedna ksi±¿ka za darmo - tylko teraz!
http://www.zapisz-sie.ksk.pl/hoga/
------------------------------------------------------------
Ju¿ wkrótce w sprzeda¿y nowa wersja programu mks_vir 2003 !!!
wiêcej informacji na temat nowej  wersji 2003 na stronie : www.mks.com.pl