[Haskell-beginners] Nested data types and bisimilarity

[Berlin Brown]

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/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20110308/d823e8bf/attachment-0001.htm>