Couple of formal questions
|
View:
New views
9 Messages
—
Rating Filter:
Alert me
|
 |
Couple of formal questions
by Creighton Hogg-4
::
Rate this Message:
Hello Haskell,
So there's two questions that have been bothering me lately & while they are, as usual, a little off topic I figured this might be a good forum: Where could I find a good treatment on data vs. codata & the difference between well-founded recursion & well-founded(?) corecursion? Where could I find a proof that the initial algebras & final coalgebras of CPO coincide? I saw this referenced in the "Bananas.." paper as a fact, but am not sure where this comes from. Thanks, Creighton Hogg _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@... http://www.haskell.org/mailman/listinfo/haskell-cafe |
|
|
Re: Couple of formal questions
by Wouter Swierstra
::
Rate this Message:
Hi Creighton,
> Where could I find a good treatment on data vs. codata & the > difference between well-founded recursion & well-founded(?) > corecursion? Bart Jacobs has some good papers on the subject. I found the draft of his book "Introduction to Coalgebra" quite good: http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf > Where could I find a proof that the initial algebras & final > coalgebras of CPO coincide? I saw this referenced in the > "Bananas.." paper as a fact, but am not sure where this comes from. I couldn't find the statement you are referring to in "Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire" - but I'm not sure if this holds for every CPO. Having data and codata coincide is quite a curious property (I think it's sometimes called "algebraic compactness" - but don't quote me on this). Hope this helps, Wouter _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@... http://www.haskell.org/mailman/listinfo/haskell-cafe |
|
|
Re: Couple of formal questions
by Matt Hellige
::
Rate this Message:
On Thu, May 1, 2008 at 9:54 AM, Wouter Swierstra <wss@...> wrote:
> > > Where could I find a good treatment on data vs. codata & the difference > between well-founded recursion & well-founded(?) corecursion? > > > > Bart Jacobs has some good papers on the subject. I found the draft of his > book "Introduction to Coalgebra" quite good: > > http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf > Indeed. I'd also recommend Varmo Vene's thesis, Categorical Programming with Inductive and Coinductive Types: http://www.cs.ut.ee/~varmo/papers/thesis.pdf Matt -- Matt Hellige / matt@... http://matt.immute.net _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@... http://www.haskell.org/mailman/listinfo/haskell-cafe |
|
|
Re: Couple of formal questions
by Michael Karcher-7
::
Rate this Message:
Wouter Swierstra <wss@...> wrote:
> Hi Creighton, > > Where could I find a proof that the initial algebras & final > > coalgebras of CPO coincide? I saw this referenced in the > > "Bananas.." paper as a fact, but am not sure where this comes from. > I couldn't find the statement you are referring to in "Functional > Programming with Bananas, Lenses, Envelopes, and Barbed Wire" - but > I'm not sure if this holds for every CPO. Probably he was referring to the last paragraph of the introduction: Working in CPO has the advantage that the carriers of intial algebras and final co-algebras coincide, thus there is a single data type that comprises both finite and infinite elements. Regards, Michael Karcher _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@... http://www.haskell.org/mailman/listinfo/haskell-cafe |
|
|
Re: Couple of formal questions
by Kim-Ee Yeoh
::
Rate this Message:
I'm not sure there's a proof as such, more like a definitional absence
of distinction between initiality and finality. In other words, the CPO framework is orthogonal to such extremality considerations. Perhaps someone here knows about work enriching CPOs in that direction. -- Kim-Ee
|
|
|
Re: Re: Couple of formal questions
by Wouter Swierstra
::
Rate this Message:
On 1 May 2008, at 16:58, Michael Karcher wrote: > Wouter Swierstra <wss@...> wrote: >> Hi Creighton, >>> Where could I find a proof that the initial algebras & final >>> coalgebras of CPO coincide? I saw this referenced in the >>> "Bananas.." paper as a fact, but am not sure where this comes from. >> I couldn't find the statement you are referring to in "Functional >> Programming with Bananas, Lenses, Envelopes, and Barbed Wire" - but >> I'm not sure if this holds for every CPO. > > Probably he was referring to the last paragraph of the introduction: > > Working in CPO has the advantage that the carriers of intial algebras > and final co-algebras coincide, thus there is a single data type that > comprises both finite and infinite elements. Ah - thanks for pointing that out. According to my more categorically inclined office mates, Marcelo Fiore's thesis is a good reference: https://www.lfcs.inf.ed.ac.uk/reports/94/ECS-LFCS-94-307/ Hope that answers your question, Wouter _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@... http://www.haskell.org/mailman/listinfo/haskell-cafe |
|
|
Re: Re: Couple of formal questions
by Creighton Hogg-4
::
Rate this Message:
On Mon, May 5, 2008 at 9:53 AM, Wouter Swierstra <wss@...> wrote:
I've had a lot of good reading material from this thread, and I greatly appreciate it: As a more background reading on this, I think Meijer & Fokkinga's "Program Calculation Properties of Continuous Algebras" is good, though the notation is a little idiosyncratic. http://citeseer.ist.psu.edu/717129.html I've also liked Baez et al's Rosetta Stone paper as food for thought http://math.ucr.edu/home/baez/rosetta.pdf Creighton Hogg _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@... http://www.haskell.org/mailman/listinfo/haskell-cafe |
|
|
Re: Couple of formal questions
by Dominic Steinitz
::
Rate this Message:
Creighton Hogg <wchogg <at> gmail.com> writes:
between well-founded recursion & well-founded(?) corecursion?Where could I find a proof that the initial algebras & final coalgebras of CPO coincide? I Creighton, I started putting something together here. I'm not sure if it's what you are after and in any event it will now have to wait until the weekend. Dominic. http://idontgetoutmuch.wordpress.com/2008/05/12/isomorphic-types/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@... http://www.haskell.org/mailman/listinfo/haskell-cafe |
|
|
Re: Couple of formal questions
by Dominic Steinitz
::
Rate this Message:
Creighton Hogg <wchogg <at> gmail.com> writes:
> Where could I find a proof that the initial algebras & final coalgebras of CPO > coincide? I saw this referenced in the "Bananas.." paper as a fact, but am not > sure where this comes from Creighton, As promised and I hope this is what you were after. Dominic. http://idontgetoutmuch.wordpress.com/2008/05/12/isomorphic-types/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@... http://www.haskell.org/mailman/listinfo/haskell-cafe |
| Free Forum Powered by Nabble | Forum Help |