Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: natural numbers type

Bottom of Page

1 to 10 of 10

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeDec 2nd 2012

    created natural numbers type (we had had type of natural numbers, but only as a redirect to natural numbers object).

    I filled the entry (only) with material copied over from inductive type (for the moment).

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeDec 2nd 2012

    Thanks. Maybe we should remove some of that detail from inductive type, then, and say “see natural numbers type”.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeDec 3rd 2012

    Yes. I can do it later when I have time. But I won’t mind if somebody else does it…

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeJan 22nd 2017
    • (edited Jan 22nd 2017)

    I fixed the suspected syntax errors in the elimination rule, added the requested computation rules, threw in the type formation rule for good measure, and added some formatting features (line breaks and semicolons) for increased readability.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeDec 31st 2022
    • (edited Dec 31st 2022)

    previously the discussion (here) of the categorical semantics of recursion was too restrictive, as it didn’t take the possible ℕ\mathbb{N}-dependency of the FF-algebra’s successor function into account, i.e. it didn’t consider passing to the slice.

    I have now expanded this out by adding discussion of the categorical semantics of the full recursion principle (now starting here).

    In the course of this I made various slight adjustments and rearrangements throughout the entry, in an attempt to polish it up a little.

    diff, v7, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJan 1st 2023
    • (edited Jan 3rd 2023)

    Best wishes for the New Year to everyone!

    \,

    I have re-typeset the inference rules for the natural numbers type:

    • more whitespace

    • hierarchized parenthesis

    • more suggestive term names

    in order to guide the eye about how the syntax tree is meant to be branching and to make it more readily graspable what all the symbols want to mean

    Currently it looks as follows:

    1. type formation rule:

      | |ℕ:Type \frac{}{ \mathclap{\phantom{\vert^{\vert}}} \mathbb{N} \,\colon\, Type }

    2. term introduction rules:

      | |0:ℕn:ℕ| || |succ(n):ℕ \frac{}{ \mathclap{\phantom{\vert^{\vert}}} 0 \,\colon\, \mathbb{N} } \;\;\;\;\;\;\;\; \frac{ n \,\colon\, \mathbb{N} \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} succ(n) \,\colon\, \mathbb{N} }

    3. term elimination rule:

      n:ℕ⊢P(n):Type;⊢0 P:P(0);n:ℕ,p:P(x)⊢succ P(n,p):P(succ(n))| || |n:ℕ⊢ind (P,0 P,succ P)(n):P(n) \frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(n) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) \;\vdash\; succ_P(n,\,p) \,\colon\, P\big(succ(n)\big) \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} n \,\colon\, \mathbb{N} \;\vdash\; ind_{(P, 0_P, succ_P)}(n) \,\colon\, P(n) }

    4. computation rules:

      n:ℕ⊢P(n):Type;⊢0 P:P(0);n:ℕ,p:P(x)⊢succ P(n,p):P(succ(n))| || |ind (P,0 P,succ P)(0)=0 P \frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(n) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) \;\vdash\; succ_P(n,p) \,\colon\, P\big(succ(n)\big) \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(P, 0_P, succ_P)}(0) \,=\, 0_P }

      and

      n:ℕ⊢P(x):Type;⊢0 P:P(0);n:ℕ,p:P(x)⊢succ P(x,p):P(sx);⊢n:ℕ| || |ind (P,0 P,succ P)(succ(n))=succ P(n,rec P n(0 P,succ P)) \frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(x) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) \;\vdash\; succ_P(x,p) \,\colon\, P(s x) \;; \;\;\;\; \vdash\; n \,\colon\, \mathbb{N} \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(P, 0_P, succ_P)}\big(succ(n)\big) \,=\, succ_P\big(n,\, rec^n_P(0_P,\, succ_P)\big) }

    will be adjusting the rest of the entry accordingly

    diff, v8, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 1st 2023
    • (edited Jan 1st 2023)

    added pointer to:

    diff, v9, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJan 3rd 2023
    • (edited Jan 3rd 2023)

    added pointer to page and verse in the the original articles by Coquand & Paulin and by Dybjer where the natural numbers type is considered

    the article

    • Christine Paulin-Mohring, §1.3 in: Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) [doi:10.1007/BFb0037116]

    is the only one which I have seen, so far, which pauses to explain why the naive non-dependent recursion scheme is not sufficient (which is maybe the most important point of the whole business, but traditionally goes without any comment). I have added a brief Remark on this point here

    diff, v11, current

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 3rd 2023

    Re #6, yes, Happy New Year everyone!

    • CommentRowNumber10.
    • CommentAuthorGuest
    • CommentTimeMar 26th 2023

    adding section about the extensionality principle of the natural numbers

    diff, v17, current

1 to 10 of 10

  1.