The Coq mailing list

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

 No it’s not the same. The idea that some computation will terminate eventually even if we are not able to perform it in practice is clearly understandable and communicable among humans. It is different to ignoring the need for constructive explanations altogether.

Sent from my iPhone

On 3 Jun 2021, at 18:34, roux cody <cody.roux AT gmail.com> wrote:



It certainly feels very hard to distinguish between Very Large Numbers and Non Standard ones, and the distinction does seem very closely related to normalization.

But I'd advocate a slightly more subtle position than "There are absolutely less than 10^74 integers", but rather, "Gee, it sure gets hard to name (most) numbers bigger than 2^10^74..."

The same way intuitionism doesn't say: "This specific machine, M, neither terminates nor runs forever" but says "Maybe we shouldn't make the blanket assumption that *all* machines either terminate or run forever".

I suspect this agnosticism is what I'm really advocating (but one can't really be too sure...)

Best,

Cody

Best,

Cody

On Thu, Jun 3, 2021 at 12:26 PM Eddy Westbrook <westbrook AT galois.com> wrote:

Cody,

My initial reaction was that Ack 5 5 will eventually compute to a specific finite natural number, so at some point c_gtN will be inconsistent.

But I think your argument has an interesting twist: you are basically arguing using a version of Ultrafinitism, that there are finite numbers that are just too big to represent in the 10^74 atoms in the universe. What you are saying is that it is not possible to actually write down a counterexample.

A counter-argument, then: if we are starting from ultrafinitism, then there are definitely no infinitary natural numbers, because there are in fact only finitely many elements of any type.

-Eddy

On Jun 3, 2021, at 9:13 AM, roux cody <cody.roux AT gmail.com> wrote:

Sadly, it is possible to compute non-standard numbers in Coq without axioms. Here is an example:

Fixpoint Ack m := fix A_m n :=
  match m with
    | 0 => n + 1
    | S pm =>
      match n with
        | 0 => Ack pm 1
        | S pn => Ack pm (A_m pn)
      end
  end.

Definition c : nat := Ack 5 5.

Indeed adding axioms like c_gt0, c_gtS0, ... (as many as you like!) will all be consistent.

In practice, though, you can pretend that such numbers do not exist, and things will go on relatively undisturbed.

Best,

Cody

On Thu, Jun 3, 2021 at 10:16 AM Vincent Semeria <vincent.semeria AT gmail.com> wrote:

Hi Eddy, 

On the contrary, I would like to avoid non standard numbers, so that the normalization property of Coq does mean that every computation of a nat term terminates.

But since we established that Coq cannot refute non standard nat terms, I am trying to measure the risk that I accidentally try to compute a non standard nat (without any axioms posed). 

On Thu, Jun 3, 2021, 16:06 Eddy Westbrook <westbrook AT galois.com> wrote:

Vincent,

There are certainly non-standard models of Coq (Gödel ensures us of that), but they are bound to be a lot more complicated than non-standard models of Peano arithmetic, which is where the notion of non-standard naturals comes from. The reason for this is that Coq can express a general notion of well-foundedness and induction in the logic (this is in fact the heart of Evan’s answer, that you can use induction in Coq), whereas Peano arithmetic cannot.

If what you really want is non-standard models of Peano arithmetic, then you will probably have to formalize Peano arithmetic, or at least a simpler form of it. I would guess that there are formalizations of it in Coq out there, but am not sure. A simpler form of Peano arithmetic might just be to define a signature (or, better, a type class) of types that have a 0 and successor but not necessarily induction.

If what you want is just infinite natural numbers, maybe you should look at Coq’s coinductive types? These let you define a Coq type that can contain infinite sequences of successors.

Hope this helps,

-Eddy

On Jun 3, 2021, at 6:53 AM, Vincent Semeria <vincent.semeria AT gmail.com> wrote:

How do these non standard integers cope with the normalization property of Coq? A non standard integer would compute to an infinite sequence of successors, so it does not terminate.

Is it a property of Coq that all definable nat terms are standard? If so, how is "standard" defined? 

On Wed, Jun 2, 2021, 22:25 roux cody <cody.roux AT gmail.com> wrote:

Sure, I mean your notional proof that the axiom schema is consistent.

On Wed, Jun 2, 2021 at 4:10 PM Evan Marzion <emarzion AT gmail.com> wrote:

By induction, c is greater than n for all n.  Thus, c > c, a contradiction.

On Wed, Jun 2, 2021 at 2:53 PM Vincent Semeria <vincent.semeria AT gmail.com> wrote:

Dear Coq club,

Is it possible to axiomatize a term c : nat, such as c is greater than all standard natural numbers ? The first 2 lines are easy,

Axiom c : nat.
Axiom c_gt0 : 0 < c.

But then, could we consistently add this axiom ?

Axiom c_non_standard : forall n:nat, n < c -> S n < c.

If the last axiom is not consistent, we could modify Coq's type checker to interpret all names of the form c_gtSSSS...S0 as closed terms of the corresponding types SSSS...S0 < c. I am pretty sure that these terms are consistent, because if they introduced a proof of False, that proof would be a finite lambda-term with only a finite number of these c_gt terms. Then c could be replaced by the greatest of these terms, and we would obtain a proof of False in basic Coq.

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.