Mailing list for all users of the OCaml language and system.
 help / color / mirror / Atom feed
From: Hendrik Tews <tews@tcs.inf.tu-dresden.de>
To: caml-list@inria.fr
Subject: Re: [Caml-list] Coinductive semantics
Date: Fri, 13 Jan 2006 11:23:43 +0100	[thread overview]
Message-ID: <rlu0c8xw7k.fsf@ithif59.inf.tu-dresden.de> (raw)
In-Reply-To: <1137102848.3681.268.camel@rosella>

Dear skaller,

please read some of the relevant paper, for instance the tutorial
on (Co)Algebras and (Co)Induction.

   First, you agree the ideas are dual .. and that's a formal
   mathematical statement that the very definitions are obtainable
   from each other by a mechanical application of the duality
   principle -- provided the definitions are stated formally
   enough of course.
   
Please read the relevant definitions. Coalgebras are the duals of
algebras _but_ coalgebra morphisms are not the duals of algebra
morphisms. Otherwise the theory of coalgebras would be void.
Because most interesting properties/definitions are connected
with the morphisms you get that the theory of algebras is _not_
dual to the theory of coalgebras.

   To take a simpler example, I simply say in some category X
   with products, and perhaps some extra structure,
   you can dualise any set of theorems to obtain another theory.
   
   The same clearly applies to initial and final algebras,
   and ALL other dual concepts -- that's the whole POINT of duality.
   
This is completely wrong. If you dualize an initial algebra you
get a final coalgebra, _but in Set^op, (ie, dualized Set)_.
Nobody is interested in final coalgebras in Set^op. People are
interested in finial coalgebras in _Set_, which are the same as
initial algebras in Set^op.

Take for instance the (set-) functor F(X) = (X x nat) + 1, where
x is product, + is disjoint union, 1 is a one-element set. The
initial algebras for it are the finite lists over nat. The final
coalgebra for it are sequences over nat, that is finite and
infinite list over nat. Do you see the difference? This
difference makes coalgebras interesting.

   dual -- they are, necessarily. The problem is that before
   duality was considered bodies of theories arose from different
   considerations that were not in fact dual i the literature, 

Sorry, you make yourself a fool here. Go out, read the papers on
the Co-Birkhoff theorem! Then you'll see that duality was always
considered by all authors on that subject. The point is that when
you dualize the Birkhoff theorem you don't get a theorem on
coalgebras!

Bye,

Hendrik

PS. Sorry if I missed some of your points, I did not read all of
your prose.


  reply	other threads:[~2006-01-13 10:23 UTC|newest]

Thread overview: 30+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2006-01-05 18:23 Alessandro Baretta
2006-01-05 19:48 ` [Caml-list] " David Baelde
2006-01-06 13:12 ` Andrej Bauer
2006-01-10 11:10   ` Francisco J. Valverde Albacete
2006-01-11  8:34     ` Hendrik Tews
2006-01-11 12:19       ` skaller
2006-01-11 14:54         ` Andrej Bauer
2006-01-12  2:10           ` skaller
2006-01-12 14:03             ` Andrej Bauer
2006-01-12 21:54               ` skaller
2006-01-13 10:23                 ` Hendrik Tews [this message]
2006-01-13 14:42                   ` skaller
2006-01-18 12:58                     ` Hendrik Tews
2006-01-18 14:22                       ` skaller
2006-01-20  0:49                         ` William Lovas
2006-01-20  9:57                           ` Andrej Bauer
2006-01-20 18:59                             ` William Lovas
2006-01-20 20:59                               ` skaller
2006-01-21 18:36                                 ` Andrej Bauer
2006-01-22  3:16                                   ` skaller
2006-01-22 12:23                                     ` Andrej Bauer
2006-01-22 15:35                                       ` skaller
2006-01-22 17:26                                       ` Kenn Knowles
2006-01-22 21:52                                         ` Andrej Bauer
2006-01-21 19:06                               ` Andrej Bauer
2006-01-13 10:40                 ` Andrej Bauer
     [not found]                   ` <43C7B17A.1070503@barettadeit.com>
2006-01-14 16:53                     ` Andrej Bauer
2006-01-05 20:38 Don Syme
2006-01-06 15:33 ` Alessandro Baretta
2006-01-08 10:02   ` Andrej Bauer

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=rlu0c8xw7k.fsf@ithif59.inf.tu-dresden.de \
    --to=tews@tcs.inf.tu-dresden.de \
    --cc=caml-list@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox