The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

For the past few days, I have been trying to summarize the wealth of information (and opinions) in this thread and the one at
https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html

I would like to share that summary and I'll be glad to know if there are mistakes in my understanding (specially about sized types).
I tried to fill some details about things that were not obvious to me and I have some questions below.

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

These methods make different trade-offs between the properties 1)-4) above. I'll discuss them one by one. I'll end the discussion on each one with a list of pros and cons.

a) Recursors/Eliminators of inductive types . In many proof assistants (e.g. HoTT, Nuprl) this is the fundamental way to use/eliminate an element of an inductive type. Functions defined using these recursors are guaranteed to be terminating. However,
as Bruno mentioned in the earlier thread, using recursors often does not produce readable code. He gives an example of a function (div2) function that can be concisely written using pattern matching, but becomes ugly when written using recursors. The following link shows both his concise and ugly versions in Coq.
http://www.cs.cornell.edu/~aa755/div2.html
(replace .html by .v to get the raw Coq code)

Another suggestion was to automatically translate functions written in the "beautiful" pattern matching syntax down to recursors.
(Cristina Cornes' PhD thesis deals with this translation; probably, there are no known translations of this to English.)
However, as Matthieu pointed out, this translation might incur a run-time overhead. Also, as Cody mentioned, it is unnatural for users (including myself) to write some function and have to prove properties about some other function (obtained after translation). Ideally the user should never have to see the translated version.

pros : logical simplicity
cons: code readability, efficiency?

b) Guardedness predicate: This is the method currently used in Coq. Aside from being suspected as the root cause of at least 2 bugs discovered in Coq, this method is not compositional. To do guardedness checking, Coq has to unfold all the definitions used in the body of the function, do reductions, e.t.c.
This makes typechecking extremely slow at times. Also, the unfoldings can cause the code to bloat by orders of magnitude and become impossible to debug. More importantly, minor syntactic changes to some definitions used in the body (while preserving semantics) can cause the type-checker to reject a legitimate function. See an example in the subsection 1.2.1 in [1]. The same subsection also explains why this guardedness predicate is also involved in loss of SN (strong normalization).

pros: code readability, efficiency?
cons: logical simplicity (lack of compositionality), code readability while debugging.

c) Coq also provides a way to write arbitrary recursive function as long as one can provide a well founded relation and prove that all recursive calls are performed on arguments that are "less" according to the well founded relation. I'm not sure about the official way to achieve this. However, one way is to use the Function construct
See the 4^th variant in  http://coq.inria.fr/refman/Reference-Manual004.html#sec75
Again a problem is that the function that actually goes to Coq's kernel is much more complicated than what we write.
As far as I understand, the only other downside is that a lot of work might be required from the users. A user has to figure out
a well founded relation and prove that the recursive calls are made on "lesser" elements according to this relation.
(Personally, I don't think that this is a big deal. We can build powerful hint databases and tactics to automate much of these proofs.)
As far as I understand, there is no additional run-time overhead. The extracted code looks pretty much like the original code that the user writes down. The proofs are thrown away
presumably because they are in Prop. So I guess one can use classical axioms in the proofs and still have the Ocaml extract run w/o getting stuck. Am I right, Matthieu?
In this sense, this method might be more expressive than others.
I have an example in the following link that shows the kernel code and the extracted code that result when the div2 function above is expressed using the Function construct.
http://www.cs.cornell.edu/~aa755/div2.html#div2_Fun

pros : logical simplicity, efficient extracts, readability of extract and user-written-code
cons : readability of the function that goes into kernel (users have to deal with this version in proofs),  may need more work from the users.

d) Sized Types :
I have many questions about this approach and my description below might have some errors.
I've mainly read the version in [1].
The key idea is to consider approximations of an inductive type.
An strictly positive inductive type can be obtained by iterating the corresponding endofunction (in some universe) over some ordinal. 
For an inductive type T, T^s  denotes the members that can be (cumulatively) obtained by iterating until the ordinal (size) s. To typecheck a recursive function on the type T, it suffices that the recursive calls are made only on  members of an approximation of T that corresponds to a lesser ordinal.
Despite the use of ordinals in the semantics, there are no ordinals in the syntax.
There is only a successor and an infinity operator in the size-language.
Moreover, the end user does not have to bother even with these sizes terms.
The typechecker introduces size variables and and maintains constraints among them.
This is probably analogous to the way Coq currently maintains automatically maintains level variables and constraints for each use of "Type" 
A user just indicates the  decreasing argument of a fix. 
If the type of that argument is same as the return type, the return type can be tagged to indicate that the function is size-preserving (e.g. map).
Note that size preserving just means that the output is of "less or equal" size.
In [1], there is no way to express more precise size-specifications like the fact that the size of append's output is the sum of the sizes of its inputs. 
(see the discussion after definition 2.1 in [1])
One could opt for a more expressive syntax for sizes (e.g. include operators for addition, maximum), but that might break the completeness of size inference and one of the
design goals is to not let users mess with size expressions.
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)

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?

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

On 09/01/14 21:54, Andreas Abel wrote:

Brigitte's and my ICFP 2013 paper includes both an intuitive account and
a formal termination proof for sized types in the "inflationary style". See

http://www2.tcs.ifi.lmu.de/~abel/publications.html#icfp13

for conference and long version (with complete proof).

Also, there are papers of Jorge Sacchini on integrating sized types into
the CIC.

Cheers,
Andreas

On 09.01.2014 19:10, Cody Roux wrote:

On 01/09/2014 12:49 PM, Nikhil Swamy wrote:

This is a very interesting discussion ... thanks! Although it's a bit
hard to keep up with it all! : )

I wonder if someone here would be able to provide a suitable reading
list on sized types. I have read Andreas Abel's MiniAgda paper, which
provides nice examples and good intuition, but not much on the
metatheory side. Is there something more comprehensive that you would
recommend to study? Abel's LMCS 2008 paper? Something even more
recent (or older)?

In addition to Andreas' excellent paper, you might want to look at
his PhD dissertation, which is a nice read with a wealth of very nice
examples and counter-examples. You might want to look at the MiniAgda
paper as well. The other paper I enjoyed the most was Barthe /et. al./

Typed based termination of recursive definitions
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.4933

That explains the situation for simple types, which I think is a good
start.

Hope this helps!

Best,
Cody

Thanks!
-Nik

-----Original Message-----
From:coq-club-request AT inria.fr [mailto:coq-club-request@inria.fr] On
Behalf Of Bruno Barras
Sent: Thursday, January 9, 2014 3:45 AM
To: Altenkirch Thorsten; Cody Roux; Jean Goubault-Larrecq; coq-
club AT inria.fr
Subject: Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about
homotopy theory & advantage of UF/Coq

On 09/01/2014 11:42, Altenkirch Thorsten wrote:

About K: Coq has managed to describe a pattern-match whI wonder if
someone here would be able to provide a suitable reading list on
sized types. I have read Andreas Abel's MiniAgda paper, which
provides nice examples and good intuition, but not much on the
metatheory side. Is there something more comprehensive that you
would recommend to study? Abel's LMCS 2008 paper? Something even
more recent (or older)?

Thanks!
-Nik
ich does not
allow it (by making less unification information available in the
branches), and I don't think it's that relevant to the problem at
hand, which is mostly concerned about when a term is a subterm of

another.

I don't agree!

If the only proof of equality is refl then it is clear that subst
should preserve the structural ordering.

It's not clear to me. Proof-irrelevance does not mean that any equality
admits refl as a proof!
If you apply subst with a proof of 0=1 (or, less controversially
(False->True) = True), I see a priori no reason why it should
preserve the
structural ordering. This ordering should remain well-founded even in
inconsistent contexts.

This reasoning is sound only when you do that for proofs of x=x, and
then
yes this is obviously related to K.

Bruno.