Send Beginners mailing list submissions to beginners@haskell.org To subscribe or unsubscribe via the World Wide Web, visit http://www.haskell.org/mailman/listinfo/beginners or, via email, send a message with subject or body 'help' to beginners-requ...@haskell.org
You can reach the person managing the list at beginners-ow...@haskell.org When replying, please edit your Subject line so it is more specific than "Re: Contents of Beginners digest..." Today's Topics: 1. Re: Nested data types and bisimilarity (Berlin Brown) ---------------------------------------------------------------------- Message: 1 Date: Tue, 8 Mar 2011 03:47:58 -0500 From: Berlin Brown <berlin.br...@gmail.com> Subject: Re: [Haskell-beginners] Nested data types and bisimilarity To: Brent Yorgey <byor...@seas.upenn.edu> Cc: beginners@haskell.org Message-ID: <aanlktinwfocfor4m_hm0kraipff42pwfaxflbto8e...@mail.gmail.com> Content-Type: text/plain; charset="iso-8859-1" On Tue, Mar 8, 2011 at 3:11 AM, Berlin Brown <berlin.br...@gmail.com> wrote: > > > On Mon, Mar 7, 2011 at 4:30 PM, Brent Yorgey <byor...@seas.upenn.edu>wrote: > >> On Sat, Mar 05, 2011 at 03:17:57AM -0800, dan portin wrote: >> > > Actually, you are missing the point. ;) The point of bisimulations is >> > > that they are defined *coinductively*, so they let you work with >> > > potentially infinite data structures. In your example, proving that >> > > xs and ys are in the relation R really is that simple -- 1 = 1, and >> > > then to complete the proof we are allowed to use the coinduction >> > > hypothesis that xs and ys are in the relation R, since they are >> > > guarded by a constructor (:). >> > > >> > > Dan, does this help answer your original question? If not I can try >> > > to give a more detailed answer in the morning. >> > > >> > >> > I understand the coinduction principle for data structures like streams >> > (e.g., Felipe's example) and finitely branching trees (from papers like >> "A >> > calculus of binary trees"). In general, for lists and types constructed >> from >> > arrow, product, and so on, it's easy to define conditions for a relation >> to >> > be a bisimulation. For instance, I know that a relation *R* is a >> > bisimulation over *n*-branching trees *t1 *and *t2* (for some *n*) if >> their >> > roots are equal and each of their subtrees are in *R*. My problem is, >> > specifically, with the case of infinitely branching trees. In Haskell, >> these >> > are modeled by the data type >> > >> > T a = T a [T a] >> > >> > and the possibility arises, of course, that the list [T a] is a stream. >> > Clearly, we can't just say that a relation *R* is a bisimulation on >> trees * >> > t1* and *t2* of type T a if their root values are equal and their >> *lists* of >> > subtrees are equal. Because if the lists are infinite, we have to prove >> that >> > they are bisimilar. And the coinduction principle for lists requires us >> to >> > have established that the head of each list is equal. But this is what >> we're >> > trying to prove! >> >> I don't actually see a problem here, as long as we generalize the >> notion of "equality" to "bisimilarity" (which is of course the point >> of bisimilarity). We say that two trees are bisimilar if there is a >> relation R, for which >> >> * if the roots of the two trees are equal >> * and their forest-streams are bisimilar >> >> then the trees are in relation R. >> >> It's perfectly fine that the notion of bisimilarity for the >> forest-streams is defined in terms of bisimilarity of trees. Perhaps >> to be completely rigorous we should say that we define the notions of >> bisimilarity for trees and for streams of trees by simultaneous >> coinduction. >> >> -Brent >> >> _______________________________________________ >> Beginners mailing list >> Beginners@haskell.org >> http://www.haskell.org/mailman/listinfo/beginners >> > > > I tried, nothing seems to work. But, here is my configuration for the > other poor souls. > > C:\Documents and Settings\Usr Berlin>echo %PATH% > C:\Program Files\Gtk+\bin;C:\Program Files\Haskell\bin;C:\Program > Files\Haskell > Platform\2010.2.0.0\lib\extralibs\bin;C:\Program Files\Haskell > Platform\2010.2.0 > .0\bin; ... and other stuff > > C:\Documents and Settings\Usr Berlin>echo %PKG_CONFIG_PATH% > C:\Program Files\Gtk+\lib\pkgconfig;C:\Program > Files\Gtk+\include\libglade-2.0;C > :\Program Files\libxml2\libxml2-dev_2.7.7-1_win32\lib\pkgconfig > > > C:\Documents and Settings\Usr Berlin>echo %INCLUDE% > C:\Program Files\Gtk+\include;C:\Program > Files\libxml2\libxml2-dev_2.7.7-1_win32 > \include;C:\Program Files\Gtk+\include\libglade-2.0;C:\Program > Files\Gtk+\includ > e > > C:\Documents and Settings\Usr Berlin>pkg-config.exe --modversion gtk+-2.0 > 2.16.2 > > C:\Documents and Settings\Usr Berlin>pkg-config --cflags gtk+-2.0 > Files/Gtk+/include/gtk-2.0 -mms-bitfields Files/Gtk+/lib/gtk-2.0/include > Files/G > tk+/include/atk-1.0 Files/Gtk+/include/cairo Files/Gtk+/include/pango-1.0 > Files/ > Gtk+/include/glib-2.0 Files/Gtk+/lib/glib-2.0/include > Files/Gtk+/include/libpng1 > 2 -IC:/Program > > C:\Documents and Settings\Usr Berlin>cabal update > Downloading the latest package list from hackage.haskell.org > > > C:\Documents and Settings\Usr Berlin>cabal install gtk > Resolving dependencies... > > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cairo-0.12.043564\cairo-0.12.0\Gtk2HsSetup.h > :25: warning: #warning Setup.hs is guessing the version of Cabal. If > compilatio > of Setup.hs fails use -DCABAL_VERSION_MINOR=x for Cabal version 1.x.0 when > bui > ding (prefixed by --ghc-option= when using the 'cabal' command) > [1 of 2] Compiling Gtk2HsSetup ( > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cairo- > .12.043564\cairo-0.12.0\Gtk2HsSetup.hs, > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cair > -0.12.043564\cairo-0.12.0\dist\setup\Gtk2HsSetup.o ) > [2 of 2] Compiling Main ( > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cairo- > .12.043564\cairo-0.12.0\Setup.hs, > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cairo-0.12 > 043564\cairo-0.12.0\dist\setup\Main.o ) > Linking > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\cairo-0.12.043564\cairo-0.12.0\dist\ > etup\setup.exe ... > Configuring cairo-0.12.0... > setup.exe: Missing dependencies on foreign libraries: > * Missing C libraries: z, cairo > This problem can usually be solved by installing the system packages that > provide these libraries (you may need the "-dev" versions). If the > libraries > are already installed but in a non-standard location then you can use the > flags --extra-include-dirs= and --extra-lib-dirs= to specify where they > are. > > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0.12.043564\glib-0.12.0\Gtk2HsSetup.hs: > 5: warning: #warning Setup.hs is guessing the version of Cabal. If > compilation > f Setup.hs fails use -DCABAL_VERSION_MINOR=x for Cabal version 1.x.0 when > build > ng (prefixed by --ghc-option= when using the 'cabal' command) > [1 of 2] Compiling Gtk2HsSetup ( > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0 > 12.043564\glib-0.12.0\Gtk2HsSetup.hs, > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0 > 12.043564\glib-0.12.0\dist\setup\Gtk2HsSetup.o ) > [2 of 2] Compiling Main ( > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0 > 12.043564\glib-0.12.0\Setup.hs, > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0.12.04 > 564\glib-0.12.0\dist\setup\Main.o ) > Linking > C:\DOCUME~1\UsrBER~1\LOCALS~1\Temp\glib-0.12.043564\glib-0.12.0\dist\se > up\setup.exe ... > Configuring glib-0.12.0... > setup.exe: Missing dependencies on foreign libraries: > * Missing C libraries: gobject-2.0, glib-2.0, intl > This problem can usually be solved by installing the system packages that > provide these libraries (you may need the "-dev" versions). If the > libraries > are already installed but in a non-standard location then you can use the > flags --extra-include-dirs= and --extra-lib-dirs= to specify where they > are. > cabal: Error: some packages failed to install: > cairo-0.12.0 failed during the configure step. The exception was: > ExitFailure 1 > gio-0.12.0 depends on glib-0.12.0 which failed to install. > glib-0.12.0 failed during the configure step. The exception was: > ExitFailure 1 > gtk-0.12.0 depends on glib-0.12.0 which failed to install. > pango-0.12.0 depends on glib-0.12.0 which failed to install. > > > > > -- > Berlin Brown (berlin dot brown at gmail.com) > http://botnode.com > http://berlinbrowndev.blogspot.com/ > I might have figured it out. The default install for gtk installed in "Program Files". I moved it to just c:\gtk without the + and the program files space and that seem to have corrected the problem. Weird. It is 2011 and that is still an issue apparently. -- Berlin Brown (berlin dot brown at gmail.com) http://botnode.com http://berlinbrowndev.blogspot.com/ -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/beginners/attachments/20110308/e011ce50/attachment-0001.htm> ------------------------------ _______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners End of Beginners Digest, Vol 33, Issue 10 *****************************************