The Coq mailing list

[Cody Roux <cody.roux AT andrew.cmu.edu>]

On 03/14/2014 03:42 PM, Abhishek Anand wrote:

===Summary====

For the "types as propositions" paradigm to work, we need the types denoting non-trivial logical propositions to NOT have diverging elements.
So, proof assistants based on the "types as propositions" idea need ways to ensure that certain types are total.
The following properties are desirable of the methods that these proof assistants make available for writing such terminating functions/proofs

1) Readability of  code
2) Logical simplicity. Compositionality is very important here 
3) Efficiency
4) Minimal annotations/proofs required from users.

At first, I included expressivity in the list above, but It seems to me that for all the methods considered in this thread, a terminating function expressible by one method can be expressed by another method using a complicated-enough translation. One exception is noted below.

I think that people mainly considered the methods a)-d) below in this thread. 

a) Recursors/Eliminators of inductive types
b) Guardedness predicate
c) Well founded relations
d) Sized Types

    This is a really nice summary! I'll only address point d), with a small comment concerning the translation between a)/b):

    The following paper of Gimenez's details the translation of a simple guard condition for Coq into recursors:

    Codifying guarded definitions with recursive schemes
    http://link.springer.com/chapter/10.1007%2F3-540-60579-7_3

    (I'm afraid I can't seem to find an open version online at the moment). The guard condition has evolved significantly since then though, so the translation has become accordingly more complex, and I'm not aware of any article detailing it.

d) Sized Types :
I'm surprised to read that functions that satisfy the guardedness checker will also satisfy the new sized type based typechecker.
Part of the surprise is because is the (internal) syntax of sizes is pretty limited and cannot express very precise size-specifications, as mentioned above. 

For example, I don't see how  a sized-types based typechecker would accept NPeano.gcd:
http://coq.inria.fr/stdlib/Coq.Numbers.Natural.Peano.NPeano.html#gcd 
It can probably infer that mod is size preserving but that is not enough.
(Note that it not allowed to look inside the definition of mod, unlike the guardedness based typechecker)

    Well the system described by Barthe et. al probably doesn't accept this definition though, and I believe that's one of the reasons the switch hasn't been made yet. However, there are several versions of size-based termination, in particular there is a version that accepts this definition almost verbatim.

The idea is to give the following type to mod:

    mod : nat a+1 -> nat inf -> nat a

    where nat s denotes the elements of nat of size 's'. This would disallow the application mod 0 x, but that's ok: this case is a "garbage case" anyways! The problem though is that for technical reasons, the Barthe et al system gives size 1 to 0, which doesn't allow this type to be appropriate.

    I think without too much effort, one could devise and implement a system which accepts all currently guarded programs in Coq with the simple size language. Andreas Abel describes most common functions like "gcd" in his (excellent) phd dissertation.

pros: logically simple (compositional), minimal work from users when it works.
cons: users might still have to often use other mechanisms like c) on top of this.

Can the Function mechanism mentioned in c) be built on top of sized types?

    Yes of course. Here's something which users should be aware of: the functions nat -> nat it is possible to *define* in Coq are the same in CIC with recursors, with guard conditions and with size-types (essentially, all provably total functions in HOL). The only difference is the *complexity of the definition* and the *equational behavior on open terms*, two things that are very important in practice.


All the best,


Cody

References:
[1] :  Jorge Luis Sacchini. On Type-Based Termination and Dependent Pattern Matching in the Calculus of Inductive Constructions. PhD thesis, Ecole  ́ Nationale Sup ́erieure des Mines de Paris, 2011. http://pastel.archives-ouvertes.fr/docs/00/62/24/29/PDF/21076_SACCHINI_2011_archivage.pdf

Thanks,
Abhishek

On Fri, Jan 10, 2014 at 7:58 AM, Jorge Luis Sacchini <sacchini AT qatar.cmu.edu> wrote:
You may also want to look at the following papers:

  Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski.
  Practical inference for type-based termination in a polymorphic
  setting.
  TLCA 2005.

  Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski.
  CIC^ : Type-based termination of recursive definitions in the
  Calculus of Inductive Constructions.
  LPAR 2006.

They describe type systems with sized types for system F and CIC, including a size-inference algorithm. My work on sized types builds directly on top of these systems.

There is also this tutorial:

   Gilles Barthe, Benjamin Grégoire, and Colin Riba.
   A Tutorial on Type-Based Termination.
   LERNET 2008 summer school.

which may have more examples and metatheory (I don't remember the details very well).


-- Jorge