On Sat, Mar 5, 2011 at 2:32 AM, dan portin wrote:

Actually, let me rephrase the question. I know that a relation R over streams is a bisimulation if, for all lists l1 and l2, (a) their heads are equal and their tails are in the relation R, or (b) both l1 and l2 are empty. Similarly, I know that a relation R over in binary trees is a bisimulation if, for all trees t1 and t2, the values at the root node of t1 and t2 are equal, and the left and right subtrees of t1 and t2 are in the relation R. From the definition of a bisimulation, the conditions for a relation R over types constructed from arrow, cross, and so on, is easy to derive.

However, suppose I have a data type

data N a = N a [N a]

By analogy, I might suppose that a relation R over trees t1 and t2 of type N a is a bisimulation if (a) the values at their root node are equal, and (b) their forests are equal. However, proving equality using this definition can lead to a circular proof. For instance, it might be the case that the values at the roots of t1 and t2 are equal, but that the head of the forests of t1 and t2 are, again, t1 and t2! (that is, assume T(t1,t2), and if their root values are equal, show that their forests are equal; if each is an infinite list, show that their heads are equal, but perhaps their heads are t1 and t2!). So I am slightly confused as to how equality of such types can be proved by the bisimulation method. In fact, I'm confused as to what the appropriate conditions are!

I don't really know much about bisimulations, so I may be missing the point or going into the wrong direction. So read this e-mail with a grain of salt =). Your N data type isn't the only one that may have some weird infinite recursion. Consider let xs = 1 : ys ys = 1 : xs To prove that xs and ys are on a relation R, you have to proove that ys and xs are on a relation R. Oops! As I said, I don't know much about bisimulations. However, you don't seem to think that there is a problem with xs/ys defined as above. So I am tempted to read your definition of a bisimulation on lists as some form of induction. Being explicit, let's define R_0 = { ([], []) } as the relation with only the empty list and R_{n+1} = R_n ∪ { (x:s, x:t) | s, t ∈ R_n, x ∈ ℕ } Now, (xs, ys) ∉ R_n for all n ∈ ℕ, as R_n contains lists of at most length n, and xs/ys have infinite length. However, (xs, ys) ∈ R_ω, where ω = |ℕ| is the first ordinal. In a real machine we only have finite time, so we can't (in general) know for sure that (xs, ys) ∈ R. Well, the same thing happens when you consider your N data type. If you have let t1 = N 1 [t1, t2] t2 = N 1 [t2, t1] then you can't know for sure in finite time in a machine in general that (t1, t2) ∈ R, however you can given infinite countable time ω. I hope that helps you to answer at least a little bit of your question =). -- Felipe.

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! So my questions is: what must be established to show that a relation is a bisimulation on an infinitely branching tree of type T a? This question arises because I'm having trouble "combining" the individual principles for trees and lists.

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

...

roots are equal and each of their subtrees are in *R*. My problem is, specifically, with the case of infinitely branching trees. In Haskell,

...

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

On Sat, Mar 05, 2011 at 03:17:57AM -0800, dan portin wrote: their these * 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/