The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Does Coq still allow impredicativity? In any case as part of this you need to prove that the termination is terminating which seems to include that at least some fragment of CoC is terminating. I guess that you have a stronger system because you have some extra universes? Still that is a bit of work.

 

Given the condition on the proof it would be easier to obtain a fast growing function using ordinals. However, a fast growing function on its own isn’t so useful because you have to produce just one number and it is not obvious when exactly your function will do this. Hence, I am not sure whether this is so helpful given the conditions you gave.

 

Thorsten

 

From: <coq-club-request AT inria.fr> on behalf of roux cody <cody.roux AT gmail.com>
Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Monday, 2 December 2019 at 13:26
To: roux cody <cody.roux AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Can you name the biggest number?

 

Someone else just pointed this out to me! As I was saying, I'd be happy to declare this the winning entry, as long as it was formalized in Coq and proven to be larger than current contender :).

 

Cody

 

On Mon, Dec 2, 2019, 8:18 AM Emilio Jesús Gallego Arias <e AT x80.org> wrote:

roux cody <cody.roux AT gmail.com> writes:

>     I'd like you invite the enthusiasts of Coq and proof theory in general
> to participate in a small and fun ongoing challenge, which I have hosted on
> Github for lack of better ideas (but I'm open to suggestions):
>
> https://github.com/codyroux/name-the-biggest-number

It is worth recalling the winner of the BIGNUM BAKEOFF contest by Ralph
Loader: http://djm.cc/bignum-results.txt

,----
| The final and winning entry, {loader.c}, diagonalizes over the
| Huet-Coquand `calculus of constructions'.  This is a highly polymorphic
| lambda calculus such that every well-formed term in the calculus is
| strongly normalizing; or, to put it another way, a relatively powerful
| programming language which has the property that every well-formed
| program in the language terminates.  The program's main function is
| called D.  (D's return value depends on a global variable, so it is in
| fact not a pure function, but this will not be important.) D works
| approximately as follows: given an argument x, it iterates over all bit
| strings with binary value less than or equal to x, and, if such a bit
| string codes for a well-formed program (`term' in lambda-calculus
| language), it runs the program (`strongly normalizes the term' in
| lambda-calculus language.)  The return value of D is then obtained by
| packaging together the return values of all these programs.  The
| program's return value is D@@5(99).  It is possible to simulate the
| computation of D(99) and prove that D(99) >= E(30419).  Also, it is easy
| to prove that D(z) >= z and that D(z) is increasing with z.  Therefore,
| the value output by the program is at least D(E(30419)).  However, in
| {FLO}, Fortune et al.  explain how to code F[omega**k] and F[epsilon_0]
| in the second-order typed lambda calculus.  The second-order typed
| lambda calculus is a subset of the calculus of constructions, and the
| methods in {FLO} can easily be used to code, say, F[epsilon_0 +
| omega**3](1000000) in a relatively short program, which can be expressed
| by a bit string of length well under E(30419).  {loader.c} is therefore
| the winner.
`----

E.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.