On Tue, Mar 8, 2011 at 3:11 AM, Berlin Brown <span dir="ltr">&lt;<a href="mailto:berlin.brown@gmail.com">berlin.brown@gmail.com</a>&gt;</span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div><div></div><div class="h5"><br><br><div class="gmail_quote">On Mon, Mar 7, 2011 at 4:30 PM, Brent Yorgey <span dir="ltr">&lt;<a href="mailto:byorgey@seas.upenn.edu" target="_blank">byorgey@seas.upenn.edu</a>&gt;</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>On Sat, Mar 05, 2011 at 03:17:57AM -0800, dan portin wrote:<br>
&gt; &gt; Actually, you are missing the point. ;)  The point of bisimulations is<br>
&gt; &gt; that they are defined *coinductively*, so they let you work with<br>
&gt; &gt; potentially infinite data structures.  In your example, proving that<br>
&gt; &gt; xs and ys are in the relation R really is that simple -- 1 = 1, and<br>
&gt; &gt; then to complete the proof we are allowed to use the coinduction<br>
&gt; &gt; hypothesis that xs and ys are in the relation R, since they are<br>
&gt; &gt; guarded by a constructor (:).<br>
&gt; &gt;<br>
&gt; &gt; Dan, does this help answer your original question?  If not I can try<br>
&gt; &gt; to give a more detailed answer in the morning.<br>
&gt; &gt;<br>
&gt;<br>
&gt; I understand the coinduction principle for data structures like streams<br>
&gt; (e.g., Felipe&#39;s example) and finitely branching trees (from papers like &quot;A<br>
&gt; calculus of binary trees&quot;). In general, for lists and types constructed from<br>
&gt; arrow, product, and so on, it&#39;s easy to define conditions for a relation to<br>
&gt; be a bisimulation. For instance, I know that a relation *R* is a<br>
&gt; bisimulation over *n*-branching trees *t1 *and *t2* (for some *n*) if their<br>
&gt; roots are equal and each of their subtrees are in *R*. My problem is,<br>
&gt; specifically, with the case of infinitely branching trees. In Haskell, these<br>
&gt; are modeled by the data type<br>
&gt;<br>
&gt; T a = T a [T a]<br>
&gt;<br>
&gt; and the possibility arises, of course, that the list [T a] is a stream.<br>
&gt; Clearly, we can&#39;t just say that a relation *R* is a bisimulation on trees *<br>
&gt; t1* and *t2* of type T a if their root values are equal and their *lists* of<br>
&gt; subtrees are equal. Because if the lists are infinite, we have to prove that<br>
&gt; they are bisimilar. And the coinduction principle for lists requires us to<br>
&gt; have established that the head of each list is equal. But this is what we&#39;re<br>
&gt; trying to prove!<br>
<br>
</div></div>I don&#39;t actually see a problem here, as long as we generalize the<br>
notion of &quot;equality&quot; to &quot;bisimilarity&quot; (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&#39;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><br>
-Brent<br>
<br>
_______________________________________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org" target="_blank">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></div><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&gt;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&gt;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&gt;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&gt;pkg-config.exe --modversion gtk+-2.0</div><div>2.16.2</div><div><br></div><div>C:\Documents and Settings\Usr Berlin&gt;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&gt;cabal update</div><div>Downloading the latest package list from <a href="http://hackage.haskell.org" target="_blank">hackage.haskell.org</a></div>
<div><br>
</div><div><br></div><div>C:\Documents and Settings\Usr Berlin&gt;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 &#39;cabal&#39; 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 &quot;-dev&quot; 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 &#39;cabal&#39; 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 &quot;-dev&quot; 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><font color="#888888"><div><br><div>
<br clear="all"><br>-- <br>
Berlin Brown (berlin dot brown at <a href="http://gmail.com" target="_blank">gmail.com</a>)<br><a href="http://botnode.com" target="_blank">http://botnode.com</a><br><a href="http://berlinbrowndev.blogspot.com/" target="_blank">http://berlinbrowndev.blogspot.com/</a><br>


</div></div>
</font></blockquote></div><br><br><div>I might have figured it out. </div><div><br></div><div>The default install for gtk installed in &quot;Program Files&quot;.   I moved it to just c:\gtk without the + and the program files space and that seem to have corrected the problem.</div>
<div><br></div><div>Weird.  It is 2011 and that is still an issue apparently.<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>