4 ms·

Am I misunderstanding this? reading all the examples, the difference between recursion and corecursion seems to be equivalent to the difference between tail rec

Am I misunderstanding this? reading all the examples, the difference between recursion and corecursion seems to be equivalent to the difference between tail recursion and stack recursion. Is that right? can anyone post an example of corecursion that is stack recursion? or is there something else that needs to happen to qualify something as corecursion?

Sharlin 12y ago
I believe the following is a corecursive analog for a stack recursive factorial implementation in Python: def factorial(i = 1): yield i for j in factorial(i + 1): yield j*i Not sure why anyone would want to implement it like that, though.
- deleted 12y ago
  [deleted]
deleted 12y ago
[deleted]
tel 12y ago
Those are just at different levels of meaning. I don't think there's a direct relationship between stack/tail recursion and recursion/corecursion. To get a brief feel for the difference consider the "type function": T x = 1 + x where 1 is the type with only one value and the type (X + Y) is the tagged union of types X and Y. We might decide to talk about the type "iterated T" as the type IT = T (T (T (T (T (T ...)))))) = 1 + (1 + (1 + (1 + (1 + ...)))))) If we tag "left" values with Inl and "right" values with Inr and take * to be the only value of type 1, then values of IT look like Inl * Inr (Inl *) Inr (Inr (Inr (Inr (Inl *)))) which looks a lot like the Peano Naturals. Now, a recursive definition on IT looks like cata : forall x . (T x -> x) -> IT -> x and a corecursive definition looks like ana : forall x . (x -> T x) -> x -> IT In other words, recursion occurs by constantly pulling "layers" of type T off of values of IT while corecursion occurs by adding "layers" of type T on to seed values to build an IT. We can convert IT to natural numbers by using cata cata (\tx -> case tx of { Inr * -> 0; Inl n -> 1 + n }) and we can invert that conversion with ana ana (\x -> case (x > 0) of { True -> Inl x; False -> Inr * }) and we can build the "infinite" structure omega with ana omega = ana (\x -> Inl x)
- crashandburn4 12y ago
  Wow, thank you so much for your answer. it definitely helped me understand better!
ww520 12y ago
They are different animals. Stack recursion/heap-based recursion or tail recursion are mechanism to implement recursion. Recursion and co-recursion are the usage of recursion with different way to manage the input data. Recursion tends to just process the input data one by one until there's no more. Co-recursion would add more to the input data along the way. Let's say I have a list of numbers. In each step of the recursion, a number is removed. If the number is odd, it's dropped. If the number is even, a randomly generated set of numbers is added to the input list, adding more to it. The recursion would take longer. Hopefully it will end if there's no more even number.
Dewie 12y ago
I guess an example of corecursion is an inductive definition of the natural numbers: Let N be a set. 1. zero is in N. 2. If an element e is in N, then s(e) is in N. You get: {zero, s(zero), s(s(zero)),...} (of course in any order, since sets are unordered). You start from zero and build the whole infinite set from that starting point. Bottom up.

Sharlin 12y ago

I believe the following is a corecursive analog for a stack recursive factorial implementation in Python: def factorial(i = 1): yield i for j in factorial(i + 1): yield j*i Not sure why anyone would want to implement it like that, though.

deleted 12y ago
[deleted]

deleted 12y ago

[deleted]

tel 12y ago

Those are just at different levels of meaning. I don't think there's a direct relationship between stack/tail recursion and recursion/corecursion. To get a brief feel for the difference consider the "type function": T x = 1 + x where 1 is the type with only one value and the type (X + Y) is the tagged union of types X and Y. We might decide to talk about the type "iterated T" as the type IT = T (T (T (T (T (T ...)))))) = 1 + (1 + (1 + (1 + (1 + ...)))))) If we tag "left" values with Inl and "right" values with Inr and take * to be the only value of type 1, then values of IT look like Inl * Inr (Inl *) Inr (Inr (Inr (Inr (Inl *)))) which looks a lot like the Peano Naturals. Now, a recursive definition on IT looks like cata : forall x . (T x -> x) -> IT -> x and a corecursive definition looks like ana : forall x . (x -> T x) -> x -> IT In other words, recursion occurs by constantly pulling "layers" of type T off of values of IT while corecursion occurs by adding "layers" of type T on to seed values to build an IT. We can convert IT to natural numbers by using cata cata (\tx -> case tx of { Inr * -> 0; Inl n -> 1 + n }) and we can invert that conversion with ana ana (\x -> case (x > 0) of { True -> Inl x; False -> Inr * }) and we can build the "infinite" structure omega with ana omega = ana (\x -> Inl x)

crashandburn4 12y ago
Wow, thank you so much for your answer. it definitely helped me understand better!

ww520 12y ago

They are different animals. Stack recursion/heap-based recursion or tail recursion are mechanism to implement recursion. Recursion and co-recursion are the usage of recursion with different way to manage the input data. Recursion tends to just process the input data one by one until there's no more. Co-recursion would add more to the input data along the way. Let's say I have a list of numbers. In each step of the recursion, a number is removed. If the number is odd, it's dropped. If the number is even, a randomly generated set of numbers is added to the input list, adding more to it. The recursion would take longer. Hopefully it will end if there's no more even number.

Dewie 12y ago

I guess an example of corecursion is an inductive definition of the natural numbers: Let N be a set. 1. zero is in N. 2. If an element e is in N, then s(e) is in N. You get: {zero, s(zero), s(s(zero)),...} (of course in any order, since sets are unordered). You start from zero and build the whole infinite set from that starting point. Bottom up.