Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorDavid_Corfield
   • CommentTimeOct 20th 2011
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI thought it better to use $pred(n)$ rather than $n -1$ in the addition, since it's supposed to apply to $\infty$.

   I thought it better to use $pred(n)$ rather than $n -1$ in the addition, since it’s supposed to apply to $\infty$.

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeOct 21st 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexIs this the page [[corecursion]]? Well, $\infty - 1 = \pred \infty$ too (both are $\infty$ in the extended natural numbers), but (regardless of $\infty$) one probably shouldn't use subtraction in addition.

   Is this the page corecursion? Well, $\infty - 1 = \pred \infty$ too (both are $\infty$ in the extended natural numbers), but (regardless of $\infty$) one probably shouldn’t use subtraction in addition.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeOct 21st 2011
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexYes, that page.

   Yes, that page.

4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeOct 21st 2011
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIt's a little confusing of Adamek to call that binary function 'add', when it's really the morphism of a coalgebra which gives rise to the addition function.

   It’s a little confusing of Adamek to call that binary function ’add’, when it’s really the morphism of a coalgebra which gives rise to the addition function.

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeOct 21st 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexYeah; I may have clarified this a bit in the page.

   Yeah; I may have clarified this a bit in the page.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeSep 28th 2012
   • (edited Sep 28th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have a dumb and naive question about corecursion. May I say that the following is a corecursive definition of "smooth function": > A function $\mathbb{R} \to \mathbb{R}$ is _smooth_ if 1. it is continuous and 2. its derivative exists and is itself a smooth function. ?

   I have a dumb and naive question about corecursion.

   May I say that the following is a corecursive definition of “smooth function”:

   A function $\mathbb{R} \to \mathbb{R}$ is smooth if 1. it is continuous and 2. its derivative exists and is itself a smooth function.

   ?

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 28th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexYou can look at the stream terminal coalgebra (functions analytic at 0) for the functor $F: X \to \mathbb{R} \times X$. $$ F(f) = \langle f(0), f' \rangle. $$ See, e.g., [Calculus in coinductive form](http://www2.tcs.ifi.lmu.de/~miranda/public/cocalculus.pdf).

   You can look at the stream terminal coalgebra (functions analytic at 0) for the functor $F: X \to \mathbb{R} \times X$.

   $$F(f) = \langle f(0), f' \rangle.$$

   See, e.g., Calculus in coinductive form.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeSep 28th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexI just want a natural-language statement. Not a stream. If I write > A function $\mathbb{R} \to \mathbb{R}$ is _smooth_ if 1. it is continuous and 2. its derivative exists and is itself a smooth function. do you all nod and say "sure, that's a valid corecursive definition" or do you object?

   I just want a natural-language statement. Not a stream. If I write

   A function $\mathbb{R} \to \mathbb{R}$ is smooth if 1. it is continuous and 2. its derivative exists and is itself a smooth function.

   do you all nod and say “sure, that’s a valid corecursive definition” or do you object?

9. • CommentRowNumber9.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 28th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexSo what's an example of a comparable natural-language recursive definition? Don't those always work via initial algebras?

   So what’s an example of a comparable natural-language recursive definition? Don’t those always work via initial algebras?

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2012
    • (edited Sep 28th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexWhen you say "A natural number is either 0 or the succesor of a natural number." then you haven't said the word "initial algebra". All I am after is a sanity check on that blue boxed statement! :-)

    When you say “A natural number is either 0 or the succesor of a natural number.” then you haven’t said the word “initial algebra”.

    All I am after is a sanity check on that blue boxed statement! :-)

11. • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 28th 2012
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexI think the blue box statement is correct, but that doesn't mean I understand quite how to formalize it as a terminal coalgebra construction. "Derivative exists" currently puzzles me.

    I think the blue box statement is correct, but that doesn’t mean I understand quite how to formalize it as a terminal coalgebra construction. “Derivative exists” currently puzzles me.

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2012
    • (edited Sep 28th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, Todd. This just occurred to me when thinking about how to write, as you will have guessed, an expositional account of _[Cartesian spaces and smooth functions](http://ncatlab.org/nlab/show/geometry+of+physics#CartesianSpaces)_.

    Thanks, Todd.

    This just occurred to me when thinking about how to write, as you will have guessed, an expositional account of Cartesian spaces and smooth functions.

13. • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 28th 2012
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI'd like to know how this works. Can I say >An extended natural number is either 0 or has a predecessor which is an extended natural number?

    I’d like to know how this works. Can I say

    An extended natural number is either 0 or has a predecessor which is an extended natural number?

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI agree with this definition (and I like it a lot!). I also think you can omit clause 1, since differentiability implies continuity. However, I would say this is not a *corecursive* definition but rather a *coinductive* definition. And in reply to Todd, I would regard it as a corecursive definition of a *predicate* rather than a *type*, so that the corresponding terminal coalgebra lives on a poset. In this case, the poset is the power set of the set of functions $\mathbb{R}\to\mathbb{R}$, and the endofunctor takes a set $F$ of functions to the set of functions whose derivative exists and is in $F$. The terminal coalgebra of this endofunctor (i.e. greatest fixed point) is the set of smooth functions. If you want to use this as a definition of "smooth function" without having a prior notion of "function" in hand, then I guess things would be trickier.

    I agree with this definition (and I like it a lot!). I also think you can omit clause 1, since differentiability implies continuity.

    However, I would say this is not a corecursive definition but rather a coinductive definition. And in reply to Todd, I would regard it as a corecursive definition of a predicate rather than a type, so that the corresponding terminal coalgebra lives on a poset. In this case, the poset is the power set of the set of functions $\mathbb{R}\to\mathbb{R}$, and the endofunctor takes a set $F$ of functions to the set of functions whose derivative exists and is in $F$. The terminal coalgebra of this endofunctor (i.e. greatest fixed point) is the set of smooth functions.

    If you want to use this as a definition of “smooth function” without having a prior notion of “function” in hand, then I guess things would be trickier.

15. • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 28th 2012
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexAh, thank you Mike! I vaguely had in mind something similar, but didn't quite have the wherewithal to say it.

    Ah, thank you Mike! I vaguely had in mind something similar, but didn’t quite have the wherewithal to say it.

16. • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 28th 2012
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItex@David 13: yes, that's exactly right.

    @David 13: yes, that’s exactly right.

17. • CommentRowNumber17.
    • CommentAuthorTobyBartels
    • CommentTimeOct 1st 2012
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexYes, $C^n$ (for finite $n$) is defined by induction on $n$, while $C^\infty$ is defined by coinduction all at once. We similarly have inductive definitions of $n$-category for finite $n$ and also coinductive definitions for $\infty$-category all at once (although in this case it\'s also possible to define an $n$-category as an $\infty$-category with an extra property, so we usually don\'t mix these).

    Yes, $C^n$ (for finite $n$) is defined by induction on $n$, while $C^\infty$ is defined by coinduction all at once.

    We similarly have inductive definitions of $n$-category for finite $n$ and also coinductive definitions for $\infty$-category all at once (although in this case it's also possible to define an $n$-category as an $\infty$-category with an extra property, so we usually don't mix these).

18. • CommentRowNumber18.
    • CommentAuthorColin Tan
    • CommentTimeNov 27th 2018
    • (edited Nov 27th 2018)
    • PermaLink
    Author: Colin Tan
    Format: TextRegarding @David 13 and @Todd 16, it seems that what David wrote, "An extended natural number is either 0 or has a predecessor which is an extended natural number" doesn't quite serve to define the extended natural numbers. For that statement doesn't preclude the extended natural numbers to be {0, 1, 2, ...}, right? Indeed if n is an element of {0, 1, 2,...}, then it is also true that n is either 0 or n - 1 is an element of {0, 1, 2, ...}. Although it does seem to be true that the natural numbers is the smallest pointed set with basepoint called 0 equipped with an endomap called successor that satisfises Urs statement, "A natural number is either 0 or the sucessor of a natural number", but it doesn't seem to be true that the extended natural numbers it the largest set equiped with a partial endomap called predecessor whose domain of definition is the complement of {0} that satisfies David's statement.

    Regarding @David 13 and @Todd 16, it seems that what David wrote, "An extended natural number is either 0 or has a predecessor which is an extended natural number" doesn't quite serve to define the extended natural numbers. For that statement doesn't preclude the extended natural numbers to be {0, 1, 2, ...}, right? Indeed if n is an element of {0, 1, 2,...}, then it is also true that n is either 0 or n - 1 is an element of {0, 1, 2, ...}.
    
    Although it does seem to be true that the natural numbers is the smallest pointed set with basepoint called 0 equipped with an endomap called successor that satisfises Urs statement, "A natural number is either 0 or the sucessor of a natural number", but it doesn't seem to be true that the extended natural numbers it the largest set equiped with a partial endomap called predecessor whose domain of definition is the complement of {0} that satisfies David's statement.
19. • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex"The largest set" doesn't really make much sense. In fact "the smallest set" doesn't really make much sense either, structurally. What we mean is that the natural numbers are the *initial* such set, and the conatural numbers are the *terminal* such set.

    “The largest set” doesn’t really make much sense. In fact “the smallest set” doesn’t really make much sense either, structurally. What we mean is that the natural numbers are the initial such set, and the conatural numbers are the terminal such set.

20. • CommentRowNumber20.
    • CommentAuthorColin Tan
    • CommentTimeNov 29th 2018
    • PermaLink
    Author: Colin Tan
    Format: MarkdownItexI think it is not sufficient to say that the conatural numbers are the terminal set such that a conatural number is either 0 or has a predecessor that is a conatural number. This would mean only the existence of a unique morphism from those partial functions with the same set as its source and target whose domain of definition is the complement of a singleton. More correctly, it should be > The predecessor of a conatural number is either undefined or a conatural number. Then this allows the existence of a morphism from those partial functions p from a set X to itself which is undefined on more than one element of X. In this sense, corecursion still seems to me not quite to define exactly what an object is, but is more a definition in the old sense, the Aristotle sense of pointing the essence of something. I feel that the above phrasing in the blue box is more correct than the linguistically equivalence manner of speech: A conatural number either does not have a predecessor or has a predecessor that is a conatural number. In the sense, we are not really naming conatural numbers per se, but rather describing the effect of taking the predecessor of a conatural number.

    I think it is not sufficient to say that the conatural numbers are the terminal set such that a conatural number is either 0 or has a predecessor that is a conatural number. This would mean only the existence of a unique morphism from those partial functions with the same set as its source and target whose domain of definition is the complement of a singleton.

    More correctly, it should be

    The predecessor of a conatural number is either undefined or a conatural number.

    Then this allows the existence of a morphism from those partial functions p from a set X to itself which is undefined on more than one element of X.

    In this sense, corecursion still seems to me not quite to define exactly what an object is, but is more a definition in the old sense, the Aristotle sense of pointing the essence of something. I feel that the above phrasing in the blue box is more correct than the linguistically equivalence manner of speech: A conatural number either does not have a predecessor or has a predecessor that is a conatural number. In the sense, we are not really naming conatural numbers per se, but rather describing the effect of taking the predecessor of a conatural number.

21. • CommentRowNumber21.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 29th 2018
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItex"Conatural numbers" is the terminal object in the category of coalgebras of the endofunctor $F: Set \to Set$ defined by $F(X) = X + 1$ (thus, a coalgebra is a set $X$ equipped with a morphism $X \to X + 1$). That defines it uniquely up to isomorphism.

    “Conatural numbers” is the terminal object in the category of coalgebras of the endofunctor $F: Set \to Set$ defined by $F(X) = X + 1$ (thus, a coalgebra is a set $X$ equipped with a morphism $X \to X + 1$). That defines it uniquely up to isomorphism.

22. • CommentRowNumber22.
    • CommentAuthorColin Tan
    • CommentTimeNov 29th 2018
    • (edited Nov 29th 2018)
    • PermaLink
    Author: Colin Tan
    Format: MarkdownItexYes. I was trying to point that that it is insufficient to say that the conatural numbers is the terminal set equipped with a partial endo-function such that each element of this set is either some distinguished element or it sent via this partial endo-function to some element of this set, for that is not enough to identify all coalgebras, only those coalgebras where the morphism $f : X \to X + 1$ sends a unique element of X to $\ast \in 1$. As a general coalgebra is equivalent to a set equipped with a partial endo-function, thus the image of the partial endo-function on each element of this set is either undefined or is some element of this set. The partial endo-function could be undefined on more than on element. Which informally becomes: "the predecessor of a conatural number is either undefined or a conatural number". If we were to say informally "a conatural number is either 0 or has a predecessor that is a conatural number", we are implicitly specifically that the predecessor partial function is undefined only at 0.

    Yes. I was trying to point that that it is insufficient to say that the conatural numbers is the terminal set equipped with a partial endo-function such that each element of this set is either some distinguished element or it sent via this partial endo-function to some element of this set, for that is not enough to identify all coalgebras, only those coalgebras where the morphism $f : X \to X + 1$ sends a unique element of X to $\ast \in 1$.

    As a general coalgebra is equivalent to a set equipped with a partial endo-function, thus the image of the partial endo-function on each element of this set is either undefined or is some element of this set. The partial endo-function could be undefined on more than on element. Which informally becomes: “the predecessor of a conatural number is either undefined or a conatural number”. If we were to say informally “a conatural number is either 0 or has a predecessor that is a conatural number”, we are implicitly specifically that the predecessor partial function is undefined only at 0.

23. • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 29th 2018
    • (edited Nov 29th 2018)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexThere may be multiple ways of characterizing the sought-after conatural numbers. The (second-order) Peano definition for the natural numbers can be succinctly stated as an $F$-algebra $(X, \theta: X + 1 \to X)$ such that $\theta$ is monic and the algebra has only itself as subalgebra. I haven't checked this works, but it might be that a straighforward dualization (a coalgebra whose structure map is epic and has only itself as quotient coalgebra) also provides a correct characterization of conatural numbers. This might be a precise way to capture the informal intuitions described earlier.

    There may be multiple ways of characterizing the sought-after conatural numbers. The (second-order) Peano definition for the natural numbers can be succinctly stated as an $F$-algebra $(X, \theta: X + 1 \to X)$ such that $\theta$ is monic and the algebra has only itself as subalgebra. I haven’t checked this works, but it might be that a straighforward dualization (a coalgebra whose structure map is epic and has only itself as quotient coalgebra) also provides a correct characterization of conatural numbers. This might be a precise way to capture the informal intuitions described earlier.

24. • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWell, the terminal object in the category of *all* $X\mapsto X+1$ coalgebras is also the terminal object in any full subcategory thereof that contains it. The latter universal property is weaker, but still defines the same object.

    Well, the terminal object in the category of all $X\mapsto X+1$ coalgebras is also the terminal object in any full subcategory thereof that contains it. The latter universal property is weaker, but still defines the same object.

25. • CommentRowNumber25.
    • CommentAuthorGuest
    • CommentTimeJun 29th 2020
    • PermaLink
    Author: Guest
    Format: TextUpdated link for @Corfield comment 7: http://lya.fciencias.unam.mx/favio/publ/cocalculus.pdf

    Updated link for @Corfield comment 7:
    
    http://lya.fciencias.unam.mx/favio/publ/cocalculus.pdf
26. • CommentRowNumber26.
    • CommentAuthorGuest
    • CommentTimeJun 29th 2020
    • PermaLink
    Author: Guest
    Format: MarkdownItexWhoops. Clickable link: [http://lya.fciencias.unam.mx/favio/publ/cocalculus.pdf](http://lya.fciencias.unam.mx/favio/publ/cocalculus.pdf)

    Whoops. Clickable link:

    http://lya.fciencias.unam.mx/favio/publ/cocalculus.pdf

27. • CommentRowNumber27.
    • CommentAuthorTobyBartels
    • CommentTimeJul 21st 2021
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexExpound the example a little more. <a href="https://ncatlab.org/nlab/revision/diff/corecursion/10">diff</a>, <a href="https://ncatlab.org/nlab/revision/corecursion/10">v10</a>, <a href="https://ncatlab.org/nlab/show/corecursion">current</a>

    Expound the example a little more.

    diff, v10, current