<br><br><div class="gmail_quote">On Mon, Mar 7, 2011 at 4:30 PM, Brent Yorgey <span dir="ltr"><<a href="mailto:byorgey@seas.upenn.edu">byorgey@seas.upenn.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div><div></div><div class="h5">On Sat, Mar 05, 2011 at 03:17:57AM -0800, dan portin wrote:<br>
> > Actually, you are missing the point. ;) The point of bisimulations is<br>
> > that they are defined *coinductively*, so they let you work with<br>
> > potentially infinite data structures. In your example, proving that<br>
> > xs and ys are in the relation R really is that simple -- 1 = 1, and<br>
> > then to complete the proof we are allowed to use the coinduction<br>
> > hypothesis that xs and ys are in the relation R, since they are<br>
> > guarded by a constructor (:).<br>
> ><br>
> > Dan, does this help answer your original question? If not I can try<br>
> > to give a more detailed answer in the morning.<br>
> ><br>
><br>
> I understand the coinduction principle for data structures like streams<br>
> (e.g., Felipe's example) and finitely branching trees (from papers like "A<br>
> calculus of binary trees"). In general, for lists and types constructed from<br>
> arrow, product, and so on, it's easy to define conditions for a relation to<br>
> be a bisimulation. For instance, I know that a relation *R* is a<br>
> bisimulation over *n*-branching trees *t1 *and *t2* (for some *n*) if their<br>
> roots are equal and each of their subtrees are in *R*. My problem is,<br>
> specifically, with the case of infinitely branching trees. In Haskell, these<br>
> are modeled by the data type<br>
><br>
> T a = T a [T a]<br>
><br>
> and the possibility arises, of course, that the list [T a] is a stream.<br>
> Clearly, we can't just say that a relation *R* is a bisimulation on trees *<br>
> t1* and *t2* of type T a if their root values are equal and their *lists* of<br>
> subtrees are equal. Because if the lists are infinite, we have to prove that<br>
> they are bisimilar. And the coinduction principle for lists requires us to<br>
> have established that the head of each list is equal. But this is what we're<br>
> trying to prove!<br>
<br>
</div></div>I don't actually see a problem here, as long as we generalize the<br>
notion of "equality" to "bisimilarity" (which is of course the point<br>
of bisimilarity). We say that two trees are bisimilar if there is a<br>
relation R, for which<br>
<br>
* if the roots of the two trees are equal<br>
* and their forest-streams are bisimilar<br>
<br>
then the trees are in relation R.<br>
<br>
It's perfectly fine that the notion of bisimilarity for the<br>
forest-streams is defined in terms of bisimilarity of trees. Perhaps<br>
to be completely rigorous we should say that we define the notions of<br>
bisimilarity for trees and for streams of trees by simultaneous<br>
coinduction.<br>
<div><div></div><div class="h5"><br>
-Brent<br>
<br>
_______________________________________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org">Beginners@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/beginners" target="_blank">http://www.haskell.org/mailman/listinfo/beginners</a><br>
</div></div></blockquote></div><br><br><div>I tried, nothing seems to work. But, here is my configuration for the other poor souls.</div><div><br></div><div><div>C:\Documents and Settings\Usr Berlin>echo %PATH%</div>
<div>C:\Program Files\Gtk+\bin;C:\Program Files\Haskell\bin;C:\Program Files\Haskell</div><div>Platform\2010.2.0.0\lib\extralibs\bin;C:\Program Files\Haskell Platform\2010.2.0</div><div>.0\bin; ... and other stuff</div><div>
<br></div><div>C:\Documents and Settings\Usr Berlin>echo %PKG_CONFIG_PATH%</div><div>C:\Program Files\Gtk+\lib\pkgconfig;C:\Program Files\Gtk+\include\libglade-2.0;C</div><div>:\Program Files\libxml2\libxml2-dev_2.7.7-1_win32\lib\pkgconfig</div>
<div><br></div><div><br></div><div>C:\Documents and Settings\Usr Berlin>echo %INCLUDE%</div><div>C:\Program Files\Gtk+\include;C:\Program Files\libxml2\libxml2-dev_2.7.7-1_win32</div><div>\include;C:\Program Files\Gtk+\include\libglade-2.0;C:\Program Files\Gtk+\includ</div>
<div>e</div><div><br></div><div>C:\Documents and Settings\Usr Berlin>pkg-config.exe --modversion gtk+-2.0</div><div>2.16.2</div><div><br></div><div>C:\Documents and Settings\Usr Berlin>pkg-config --cflags gtk+-2.0</div>
<div>Files/Gtk+/include/gtk-2.0 -mms-bitfields Files/Gtk+/lib/gtk-2.0/include Files/G</div><div>tk+/include/atk-1.0 Files/Gtk+/include/cairo Files/Gtk+/include/pango-1.0 Files/</div><div>Gtk+/include/glib-2.0 Files/Gtk+/lib/glib-2.0/include Files/Gtk+/include/libpng1</div>
<div>2 -IC:/Program</div><div><br></div><div>C:\Documents and Settings\Usr Berlin>cabal update</div><div>Downloading the latest package list from <a href="http://hackage.haskell.org">hackage.haskell.org</a></div><div><br>
</div><div><br></div><div>C:\Documents and Settings\Usr Berlin>cabal install gtk</div><div>Resolving dependencies...</div><div>C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cairo-0.12.043564\cairo-0.12.0\Gtk2HsSetup.h</div><div>:25: warning: #warning Setup.hs is guessing the version of Cabal. If compilatio</div>
<div> of Setup.hs fails use -DCABAL_VERSION_MINOR=x for Cabal version 1.x.0 when bui</div><div>ding (prefixed by --ghc-option= when using the 'cabal' command)</div><div>[1 of 2] Compiling Gtk2HsSetup ( C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cairo-</div>
<div>.12.043564\cairo-0.12.0\Gtk2HsSetup.hs, C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cair</div><div>-0.12.043564\cairo-0.12.0\dist\setup\Gtk2HsSetup.o )</div><div>[2 of 2] Compiling Main ( C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cairo-</div>
<div>.12.043564\cairo-0.12.0\Setup.hs, C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cairo-0.12</div><div>043564\cairo-0.12.0\dist\setup\Main.o )</div><div>Linking C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cairo-0.12.043564\cairo-0.12.0\dist\</div>
<div>etup\setup.exe ...</div><div>Configuring cairo-0.12.0...</div><div>setup.exe: Missing dependencies on foreign libraries:</div><div>* Missing C libraries: z, cairo</div><div>This problem can usually be solved by installing the system packages that</div>
<div>provide these libraries (you may need the "-dev" versions). If the libraries</div><div>are already installed but in a non-standard location then you can use the</div><div>flags --extra-include-dirs= and --extra-lib-dirs= to specify where they are.</div>
<div>C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0.12.043564\glib-0.12.0\Gtk2HsSetup.hs:</div><div>5: warning: #warning Setup.hs is guessing the version of Cabal. If compilation</div><div>f Setup.hs fails use -DCABAL_VERSION_MINOR=x for Cabal version 1.x.0 when build</div>
<div>ng (prefixed by --ghc-option= when using the 'cabal' command)</div><div>[1 of 2] Compiling Gtk2HsSetup ( C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0</div><div>12.043564\glib-0.12.0\Gtk2HsSetup.hs, C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0</div>
<div>12.043564\glib-0.12.0\dist\setup\Gtk2HsSetup.o )</div><div>[2 of 2] Compiling Main ( C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0</div><div>12.043564\glib-0.12.0\Setup.hs, C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0.12.04</div>
<div>564\glib-0.12.0\dist\setup\Main.o )</div><div>Linking C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0.12.043564\glib-0.12.0\dist\se</div><div>up\setup.exe ...</div><div>Configuring glib-0.12.0...</div><div>setup.exe: Missing dependencies on foreign libraries:</div>
<div>* Missing C libraries: gobject-2.0, glib-2.0, intl</div><div>This problem can usually be solved by installing the system packages that</div><div>provide these libraries (you may need the "-dev" versions). If the libraries</div>
<div>are already installed but in a non-standard location then you can use the</div><div>flags --extra-include-dirs= and --extra-lib-dirs= to specify where they are.</div><div>cabal: Error: some packages failed to install:</div>
<div>cairo-0.12.0 failed during the configure step. The exception was:</div><div>ExitFailure 1</div><div>gio-0.12.0 depends on glib-0.12.0 which failed to install.</div><div>glib-0.12.0 failed during the configure step. The exception was:</div>
<div>ExitFailure 1</div><div>gtk-0.12.0 depends on glib-0.12.0 which failed to install.</div><div>pango-0.12.0 depends on glib-0.12.0 which failed to install.</div></div><div><br></div><div><br><div><br clear="all"><br>-- <br>
Berlin Brown (berlin dot brown at <a href="http://gmail.com">gmail.com</a>)<br><a href="http://botnode.com">http://botnode.com</a><br><a href="http://berlinbrowndev.blogspot.com/">http://berlinbrowndev.blogspot.com/</a><br>
</div></div>