This page contains an argument over whether Recursion needs to be adjusted to properly account for corecursion.

Corecursion edit

Corecursion currently redirects to Recursion, but there is no mention of corecursion here. Can I request that someone either add one (it's not my area), or remove the redirect? --Malcohol 14:11, 2 Jun 2005 (UTC) In fact, now that I've read the Recursion article, this may be an important distinction that is being overlooked. The humorous "definition of recursion" is described as "an erroneous recursive definition of an object, the error being the absence of the termination condition...". Yet the "recursive acronym GNU" has no such termination condition. I think some of the examples described as recursive may acually be corecursive. As I said, this isn't my area, but I think an example of a corecursive definition is the following: "The first element of the sequence s is 1 and the rest of it is equal to s". This is a valid definition of an object (the infinite list of ones) yet there is no base case. Of course, you may not believe in the existance of infinite objects, but let's leave that until later in the pub;).--Malcohol 14:41, 2 Jun 2005 (UTC)

What you are calling co-recursive is simply recursive. There is indeed a base case in the definition of that infinite list of ones:
  • The first element of the list is 1. (the base case)
  • Each element after the first is equal to the previous element. (the recursive case)
Note that if you remove the supposedly unnecessary base case, you don't have much of a definition anymore; it could be a list of 1s, of 2s, of 5s, of -32568s, of anything.
A co-recursive definition, to my knowledge, would be something like the following:
  • Alpha-sorting a set of strings means sorting them first in ascending order by their first characters, then beta-sorting within those sets by the remainder of the strings.
  • Beta-sorting a set of strings means sorting them first in descending order by their first characters, then alpha-sorting within those sets by the remainder of the strings.
Alpha-sorting never directly calls alpha-sorting, nor does beta-sorting directly call beta-sorting, but unless the strings are unusually short or sparse, they will call themselves, indirectly through the other. The two routines are thus co-recursive. -- Antaeus Feldspar 23:00, 25 Jun 2005 (UTC)
Your sorting example is an example of what I think is called mutual recursion, not corecursion. Such definitions can be dealt with like standard recursion. There is a problem with your analysis of the infinite list of ones. The statement "the first element of the list is 1" cannot qualify as a base case since it does not uniquely define a list. However, your analysis is not completely wrong: very many corecursive definitions can be converted to recursive definitions by a reformulation of some kind. So, for example, you could define a function which returns the nth element of the infinite list of ones using a standard recursive definition similar to your analysis. This, however, is not a list; it is a function. Anyway, I'm not the right person to add the notion of corecursion to the article, but I reiterate my request for someone to add it. --Malcohol 28 June 2005 09:46 (UTC)
I think there is a problem with your analysis of my analysis. =D No one ever said that a "base case" had to uniquely define a list, or any other complete object, in order to qualify as a base case. In order to qualify as a base case, a base case only needs to return some partial result without calling itself directly or indirectly. As well, I detect some problems with your idea that when we have created a function that exactly specifies without ambiguity or error exactly what each element of an infinite list must be, we have not "defined" that list. What, exactly, does it take to "define" a list in your view? If we state "every element in this infinite list is 1", have we not defined it? And yet that too is 'just a function', the function "f(n) = 1". -- Antaeus Feldspar 30 June 2005 00:06 (UTC)

I see we have a different idea of what constitutes a list. I fully accept that lists can be modelled as a function from Naturals to Naturals (although, to model finite lists, the codomain needs some undefined value and there must be an invariant constraining the functions to those which correctly model lists). With this model, a standard recursive definition can define the infinite list of ones.

On the other hand, I think a more natural model of a list is a the nested pair idea. Using Functional programming/Datatype notation, lists can be modelled as "Emptylist + (Natural * List)". This has a corresponding set theoretic definition, but I'm not that familiar with set theory. Non-well-founded set theory would probably be required for infinite lists. Viewing lists in this way, I think the definition of the infinite lists of ones must be a corecursion.

No one ever said that a "base case" had to uniquely define a list, or any other complete object, in order to qualify as a base case.

Actually, I think that a base case would have to do this and I disagree that a partial result will do as the result of any call of a function. But perhaps we are just disagreeing on models again: in your model of a list, the function which models it returns a natural number, thus 1 is an acceptable return value. In mine, the definition is required to return a list, so "some list whose first element is 1" is not an acceptable result.--Malcohol 4 July 2005 15:03 (UTC)

If I'm following you, you're saying that the infinite list of ones can be defined as "x = {1,x}", and you're saying that there is no "base case" involved in this definition. If this is so, then what list is uniquely defined by "x = {x,x}"? It sure looks like a base case and a recursive case vs. two recursive cases to me... -- Antaeus Feldspar 4 July 2005 17:09 (UTC)

Okay, I could argue further, but I think I'm going beyond what I know here. I've found what looks like a useful reference: On the Foundations of Corecursion by Moss and Danner. If I get some time, I'll give it a read and see if I can make my point more effectively. A book which looks good is Vicious Circles by Barwise and Moss.--Malcohol 7 July 2005 09:02 (UTC)