[Haskell-beginners] Nested data types and bisimilarity

[Berlin Brown]

On Tue, Mar 8, 2011 at 3:11 AM, Berlin Brown <berlin.brown at gmail.com> wrote:

>
>
> On Mon, Mar 7, 2011 at 4:30 PM, Brent Yorgey <byorgey at 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 at 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.htm>