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