The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Hello Lukasz,

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

There is some people here and there were working on the topic you mentioned. 
You can take a look to the following references:

- Bruno Barras' PhD thesis, which contains a typing system where termination  
  is based on a marking system.
- G Barthe, M J Frade, E Giménez, L Pinto, T Uustalu. Type-based termination 
of recursive definitions. Accepted for publication in Math Struct in Comp 
Science (I can send you a copy if you are interested in it). This article 
describes a system like the one you are interested in, and its main 
properties, but only for simply-typed lambda calculus. It also contains a 
comparison with other approaches and systems.
-   Structural Recursive Definitions in Type Theory, by Eduardo Giménez    
(ICALP'98). An extended veresion of the article can be downloaded from my web 
page (http://pauillac.inria.fr/~gimenez). This article extends CIC with a 
marking system where "marks" are actually type variables, like in Milner's 
calculus.

Best wishes,
Eduardo Gimenez

On Monday 07 October 2002 19:06, you wrote:
>  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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club