Start of esap buffer: Wed Sep 13 21:22:17 2006

Session Ident: esap (n=esap@a81-197-156-147.elisa-laajakaista.fi)
<bourbaki> hidiho sry that i query 
<bourbaki> you
<bourbaki> would you maybe interested in participating to release a paper for the new ifl07 next year?
<bourbaki> i have an idea and would send you the stuff via mail if you are interested i try to get dons 
  on board and he seems to be interested
<bourbaki> hidiho sry that i query 
<bourbaki> you
<bourbaki> would you maybe interested in participating to release a paper for the new ifl07 next year?
<bourbaki> i have an idea and would send you the stuff via mail if you are interested i try to get dons 
  on board and he seems to be interested
<esap> what kind of paper?
<esap> what's the topic?
<esap> I have quite busy schedule, so I can't do much work for a paper.
<bourbaki> the topic is extending the arrow stuff to petri net like programs
<bourbaki> if you want ill send you the 4 small files and you can have a look at it
<esap> I'm interested in reading it
<bourbaki> from what i remember of talking to you some time back you might be interested
<bourbaki> ok cool what addy should i send it to?
<bourbaki> its just a super small sample 
<esap> esa.pulkkinen@kotiposti.net
<bourbaki> ok sec
<bourbaki> ok the mail is send
<bourbaki> maybe you can contribute some ideas on the category side i think that these will form a week 
  topos and cartesian closed category though i have no idea if that is something good or thing that 
  needs to be mentioned
<esap> it's not clear to me whether your pictures are at the level of values or at the level of types.
<bourbaki> its at both i think
<bourbaki> if you have cyclic programs/graphs
<bourbaki> you need an interpreter cause you cant use the arrow operations to fold it to a single arrow
<bourbaki> so the interpreter is at the value level and for debugging issues and such
<bourbaki> once you 
<bourbaki> "compile" the program to a single arrow its at type level i think
<bourbaki> i hope that makes sense :)
<esap> no I mean, consider the 'joining of processes' picture. If the rightmost node represents a 
  product, then compared to normal "type-level" stuff, your arrows point to the wrong direction.
<esap> but if it's the value level, then I don't understand your description of it.
<bourbaki> well if its one of these choice arrows its the right direction isn tit?
<bourbaki> i guess its rather on the value level though cause its quite inspired by perti nets and data 
  flow
<esap> ok let me think a sec about this.
<bourbaki> sure take all the time you need
<esap> how do you distinguish products and coproducts?
<bourbaki> what do you mean by coproducts?
<esap> Either a b
<bourbaki> ah ok
<bourbaki> well you would need to tag the node for that
<bourbaki> but basically it will be sufficient to use the right type at the target node
<bourbaki> that is if its a cartesian product its simple what you mean and if its just the type of both 
  codomains then its also sufficient i think
<bourbaki> and since i dont want to allow to mix that this should surfice
<esap> I'm wondering about the 'parallel processes' picture, which represents (***), I was wondering how 
  your pictures could represent (+++). Is it the same picture as (***)?
<bourbaki> whats the exact notion of +++ again?
<bourbaki> a b c -> a b d -> b (c ,d) ?
<bourbaki> er
<esap> (+++) :: (ArrowChoice a) => a b c -> a b' c' -> a (Either b b') (Either c c')
<bourbaki> ah ok well for the either stuff i have to do it a bit different i think but this is the 
  result in the end i guess
<bourbaki> that is if its deterministic and you can just choose one of the other path in the graph then 
  its +++
<bourbaki> but if you cant garante that youll have to use the a (b b') (c c') notation
<bourbaki> the same accounts for the split of two processes for a if then else structure
<bourbaki> id really split that and then join them again 
<esap> ok I think I see what you're trying to do
<bourbaki> do you think that it is worth writeing a paper for that stuff?
<bourbaki> i think that especially the topological stuff over these graphs is interesting like the 
  quotient spaces and such
<bourbaki> and also you can unlike in usual automaton theory connect programs in other places then the 
  first and last node
<esap> that's the part that I don't understand well, perhaps because I don't really know topological 
  spaces very well
<bourbaki> well its pretty easy
<bourbaki> if you have the usual graph notation
<bourbaki> G = {E, V}
<bourbaki> V = ExE
<bourbaki> then the gluing thingy i do there is just 
<bourbaki> G1 + G2 = {E1 + E2, V1 + V2}
<esap> what's the '+' there? coproduct?
<bourbaki> and the ~ operator the quotient space just make elements in E1 and E2 equal and thus the ... 
  er sec
<bourbaki> E = VxV :)
<bourbaki> yes + is the coproduct
<bourbaki> just adding up the two lists in this case
<bourbaki> a small example
<bourbaki> G1 just consists of two nodes and one edge
<bourbaki> and G2 also
<bourbaki> G1 = { {v1,v2}, {v1 x v2} }
<bourbaki> G2 = { {v1_2,v2_2}, {v1_2 x v2_2} }
<bourbaki> now we want to append G2 to G1
<bourbaki> then you do G1 + G2 / ~
<bourbaki> and ~ is
<bourbaki> well it makes v2 and v1_2 equal and all other elements not equal
<bourbaki> and thus you end up with
<bourbaki> G3 = { {v1, v2, v2_2}, {v1 x v2, v2 x v2_2}}
<esap> is the equivalence relation used for the glue part of input to the glueing mechanism?
<bourbaki> yes
<bourbaki> all you would need to do in the graphical interface is connecting the nodes that are equal in 
  the new program
<bourbaki> and with graph matching you can do the following
<bourbaki> programX / subprogramY
<bourbaki> that is you make a subprogram a single arrow which is what you do when you "compile"
<esap> ok that's some kind of abstraction mechanism?
<bourbaki> so if you have two arrow in a program you can do this to make it use the >>> operator
<bourbaki> yes
<bourbaki> you can zoom out that way of your program
<bourbaki> ok make some parts of the program look like black boxes
<bourbaki> and the idea is that you just build up your complex programs by successively glue together 
  "simpletons" these arrow constructs
<bourbaki> this is just like in CW constructions
<esap> CW?
<bourbaki> http://en.wikipedia.org/wiki/CW_complex
<bourbaki> c = closure finite and w = weak topology
<esap> ok, I haven't heard of CW_complexes before :-)
<bourbaki> np :) but you more or less get the big picture of the idea?
<esap> yes. I'm wondering if the programs can really be represented as graphs.
<bourbaki> well because on the execution level they are like petri nets they can
<bourbaki> and you can mix different concepts
<bourbaki> ie you can use a neural net just as a graph and mix it with a usual program
<bourbaki> thats why i thought about that initially
<esap> well ok, but consider one link in a graph. Does it have some structure?
<bourbaki> a link beeing an edge?
<esap> yes
<bourbaki> ok all structure it has is the function its representing that is domain codomain and the 
  function body itself
<esap> other than the trivial structure of the pair of vertices
<bourbaki> the structure is just the same as in usual arrow notation i think
<bourbaki> the only real problem i have come by is recursion cause it expands the graph and thus needs 
  an interpreter
<bourbaki> i thought about a (co)+algebra way
<bourbaki> thus you have something like TxT -> T as in monads but also a T -> TxT to decompose it again
<bourbaki> that is something that generate graphs from byte code or so
<bourbaki> i hope im not eating too much of your time with that stuff
<esap> I'm thinking that due to the structure on the edges of the graph, you might actually find that 
  your graph is a category, with objects the data types and arrows the functions.
<bourbaki> yes that was one of the concepts i had in mind also
<bourbaki> also i think it canonically forms a CCC
<bourbaki> and maybe a topos if you allow partial application
<esap> but in that model, the gluing is interesting
<bourbaki> yes i think thats one of the strongest points and the quotent spaces
<bourbaki> so would you be interested in helping us at least if you are not able to write stuff?
<esap> is the gluing operation's equality relation a pair of arrows in that category [so you might get a 
  coequalizer maybe? actually I'm not sure, might be equalizer even...]
<esap> because what you are comparing is clearly the vertices of the graph.
<bourbaki> no i dont think so the ~ operator makes nodes equal but you can use it if you make edges 
  equal maybe that way
<bourbaki> that is if you have a graph X and there are two edges in there
<bourbaki> then X / ~ with ~ beeing an operator that makes the two edges equal might be interpreted as 
  useing >>> on the two edges
<bourbaki> if you use that on a subgraph its like applying whatever is needed to get a single edge which 
  might not be a single output if its not unambigous
<bourbaki> though if the compilation is propper all the outcomes should be equivalent under bisimulation 
  that is have the same results
<esap> I don't understand how ~ making two edges equal can be interpreted as composing the edges.
<bourbaki> ~ makes several elements in X one element in the resulting space
<esap> wouldn't such edges be parallel to each other
<bourbaki> that is if i plug in the two arrows in ~ then the result will be that the two edges are the 
  same in the result
<bourbaki> thats a matter of interpretation i think
<bourbaki> if the edges dont share a domain or codomain
<bourbaki> then its paralell 
<bourbaki> if they do its >>>
<esap> I thought if the edges are equal, they should have same domain *and*
<esap> I thought if the edges are equal, they should have same domain *and* same codomain
<bourbaki> i think i was to sloppy there
<bourbaki> ~ doesnt make edges equal thats false sry
<bourbaki> in the topology book i have its known as
<bourbaki> zusammenschlagen
<bourbaki> in english thats like ... beating together
<bourbaki> ie you have a surface X
<bourbaki> and you have a lake on that surface for example and you want to make the lake accassable as a 
  single element
<bourbaki> then you can do the following
<bourbaki> X / lake
<bourbaki> then youd have all the grass elements in X and one single lake element
<bourbaki> i hope thats not too trivially expressed for you :( but im bad at explaining
<esap> I think I see what you mean, it's in the context of gluing. You want to join the vertices of the 
  two glued graphs.
<bourbaki> in the same way i want to make a chain of edges availabe as a single edge
<bourbaki> right
<bourbaki> and if you want to build the quotient space of a single graph then ~ is something else
<bourbaki> then ~ is a subgraph
<bourbaki> let me see if i can find the stuff on the inet
<esap> ok. I think I see the idea.
<bourbaki> http://en.wikipedia.org/wiki/Quotient_space_%28topology%29
<bourbaki> the examples have gluing
<bourbaki> in topology you can use the ~ also to build cells on your surface
<bourbaki> and cell is here interchangeable with "chains" of edges
<esap> The glue operation is quite different than using the quotient on subgraphs.
<bourbaki> the glue that i use is also useing points (vertices)
<bourbaki> the other quotient space thingy is just aplicable on a single graph
<bourbaki> the latter tells you which edges form a "cell"
<bourbaki> let me get the book from the shelf for that sec
<bourbaki> the problem is that its a german book
<bourbaki> ill try to translate it
<bourbaki> let X be a topological space
<bourbaki> A is a subspace of X
<bourbaki> and non empty
<bourbaki> then X / A describes a quotientspace
<bourbaki> X / ~_A
<bourbaki> where
<bourbaki> x ~_A y :<=> x = y or x and y are both in A
<bourbaki> this is called beating together in german
<esap> hmm.. interesting. the definition of ~_A is opposite of what I thought.
<bourbaki> so if A is a subgraph you make that graph a single edge
<esap> ah, no, that's wrong.
<bourbaki> the text says further that in the new space A is a single point ...
<esap> you actually mean, that x = y is real equality, and ~_A is equality that combines all elements of 
  A.
<esap> ok I see, it's now clear.
<bourbaki> right so it would be a vertex but youd have to have to define ~ then over the edges of the 
  graphs and not the vertices
<bourbaki> so G / ~ is not precise enough here you are right there
<esap> A is a set of vertices there, right?
<bourbaki> no its edges in this case
<bourbaki> casue ie if you have two nodes of different type they cant be beaten together
<bourbaki> the gluing together of two programs it then explicitly
<bourbaki> program1 = { vertices, edges }
<bourbaki> program2 = { vertices, edges }
<bourbaki> and newprogram = { vertices1 + vertices2 / ~, edges1 + edges2 }
<bourbaki> where the subgraph thingy would rather be
<bourbaki> newprogram = { vertices, edges / A }
<bourbaki> where A is a subset of edges
<esap> but then you don't get that a subgraph described by A would be reduced to a point, it would be 
  reduced to an edge.
<bourbaki> and the cells formed that way are interpreted in the way that you get a single element(edge) 
  of the A
<bourbaki> righht its reduced to a point where a point in this case is a single function/edge/arrow
<bourbaki> so if you do this you zoom out/ abstract your program
<bourbaki> that is just lets pretend for a while we can explicitly find while loops in our program graph
<bourbaki> and you arent interested in looking at the while loops anymore then you can fold them buy
<bourbaki> program / while_loop
<bourbaki> thats a bit like the folding in modern ides just that its not reversable anymore so its like 
  compileing 
<bourbaki> and the compileing is dependant on the language you use
<esap> is there some concept that represents a "collection of edges from A to B"? like a Hom-set in 
  category theory?
<bourbaki> i think so ... but im not 100% sure
<bourbaki> you could just have a category of arrows
<bourbaki> which is better then the edges form A to B just say
<esap> it would be an exponential object in the category of data types and functions.
<bourbaki> Arrow A B
<bourbaki> right and if i have those its a topos
<bourbaki> which is why i need partial application to get these at least from what i think with my not 
  too deep insight in CT
<esap> the thing is, since you start from a graph, and the operations attempt to keep edges as points, 
  the category is in one sense degenerated.
<bourbaki> at least i think of exp opbjets as partial application
<esap> but that may be unavoidable when you're talking about concurrency.
<bourbaki> yes its sloppy at a lot of places i think but would you care to invest some work in it and 
  think about it a bit more? that is of course if you think its worth the time
<esap> exp objects are like haskell's "A -> B" type.
<bourbaki> even if you dont can write anything if you prove read and help us a bit id place your name on 
  the paper because thats all i can ask for really (reading and helping that is)
<bourbaki> but A -> B ~ arrow A B isnt it?
<esap> yes.
<esap> but at the level of *types*, not *values*
<bourbaki> ah ok
<bourbaki> its not that easy though to just operate on the type level
<bourbaki> do you think that the idea gains anything if i include CT?
<esap> you might get some easier-to-work with formalisms.
<bourbaki> i thought id gain something if i was able to say its a topos
<esap> but one problem is that concurrency requires some advanced concepts to model with category 
  theory. It's not easy.
<bourbaki> but personally i totally like the topological approach but thats maybe because im familair 
  with topology
<bourbaki> the idea for concurency was that you have an interpreter
<bourbaki> and an intperreter is nothing but a functor
<bourbaki> this it maps vertices (typed containters) to other vertices in the new graph
<esap> hmm. how do you make an interpreter as a functor. I thought interpreter is an arrow of type  F A 
  -> A.
<bourbaki> the updated graph that is
<esap> and the functor F represents the language being interpreted.
<bourbaki> and the edges just id to the edges in the other graph
<bourbaki> yes in my case a petri net
<bourbaki> do you know petri nets otherwise ill just explain it its really simple
<esap> I know the basic notations, but if there is some deep theory, I might not know those.
<bourbaki> no just the basics
<esap> ok, I do know basics of petri nets.
<bourbaki> so the functor would have to look if all the predecessing nodes are fillend and then execute 
  the edges
<bourbaki> and also the functor needs to behave like the io monad in a way because you need to be able 
  to add delete and modify edges
<bourbaki> er state monad
<esap> I'm not sure how that's a functor.
<bourbaki> hm ... why?
<bourbaki> a functor just maps vertices on vertices and edges on edges
<bourbaki> so theres a functor for each state the graph can be in that translates it to the updated state
<esap> oh I thought in a different category.
<esap> Is it some kind of forgetful functor then?
<bourbaki> and since you have the graph state as an element of the functor input you can choose the 
  right functor
<esap> forgetful functor F : C -> C , where C is the category that represents your graph
<bourbaki> i have heared that before
<bourbaki> yes more or less
<bourbaki> it needs to be something like 
<bourbaki> F: CxState -> C though
<bourbaki> cause the functor F depends on the state the graph is in
<bourbaki> othewise you would have a set of functors and you dont know which one should be applied
<bourbaki> since the functor just can "see" the single vertex
<esap> I thought of a category where objects are the graphs, and arrows are functions that preserve the 
  semantics of the graph.
<bourbaki> ah yes thats another possiblility
<bourbaki> then you have that scope thingy already in it
<bourbaki> sure you can do that as well
<bourbaki> then yes its a forgetful functor
<esap> no I mean, in that case, the arrows of the category could represent evaluation
<bourbaki> oh is see my idea also was that the functor follows the same notion as the program we just 
  developed
<bourbaki> also we need to have a notion of adding, deleteing and modifying arrows/edges in the graphs
<bourbaki> if we have this we are almost done then you can execute programs and if not cyclic you can 
  crunch/compile them to a single edge
<esap> btw, have you read Crolard's paper on coroutines and his 'subtractive logic' paper? I think those 
  are interesting in this context.
<bourbaki> no i havent but i might do so got an url at hand?
<esap> hold on
<esap> http://citeseer.ist.psu.edu/crolard99subtractive.html
<bourbaki> whats the cup and cap again in english?
<bourbaki> union and ... ?
<esap> intersection
<bourbaki> ah dang rgiht
<bourbaki> this whole notation also allows you to do intersection of programs
<bourbaki> and also because i think you can construct the usual c++ object stuff in there
<bourbaki> you can do the oposit of deriveing classes 
<bourbaki> that is you can intersect classes and come up with a propper interface of the classes you can 
  derive from
<bourbaki> if you dont mind btw id like to send our discussion to dons in the end so he can read what we 
  talked about
<esap> the other paper is: http://www.univ-paris12.fr/lacl/crolard/publications/jlc.pdf
<bourbaki> thanks ill read these papers
<bourbaki> but do you think that a paper on this idea will have a chance to get accepted at ifl?
<esap> I don't know what kind of criteria they have.
<bourbaki> http://www.inf.elte.hu/rendezvenyek/ifl/callforpapers.html
<esap> I think most of it is fairly basic stuff.
<bourbaki> hm yes but there is no good visual editor for arrows and such yet
<bourbaki> and also its all founded on nice notations in topology
<esap> but papers and visual editors are not quite the same thing :-) It's nice to have an 
  implementation, but paper needs more...
<esap> you need to have a solid theory and be able to express it clearly and in simple way.
<bourbaki> i dont want the actual implementation really but the math notion
<bourbaki> i think that the / operator is quite simple and strong and its extending the automaton theory 
  a lot
<esap> have you seen the stuff that was part of the ICFP programming contest where they had a 
  two-dimensional programming language?
<bourbaki> i dont think so 
<esap> for the competition, they had actually implemented a parser for two-dimensional ASCII diagrams
<bourbaki> and the interpreter would have a propper definition with functors and such
<esap> then had people write programs on top of that...
<bourbaki> damn....
<bourbaki> got an url for that as well?
<bourbaki> so you think that its not worth to start this paper?
<esap> http://icfpcontest.org/
<esap> well I think it might be possible to write a paper about this, but it would be lots of work.
<bourbaki> but you think it would be worth the work?
<esap> I'm not sure. I think the basic ideas have been around for some time. It would be worth it if the 
  concepts can be written in sufficiently clear way in the paper, so you could connect all the details 
  regarding topology in a coherent thing.
<esap> the problem as I see it is that there is lots of details you need to be able to describe in a 
  clear way.
<bourbaki> would you be interested in proof reading the paper? i guess from what you said so far that 
  you wont have the time to participate in any other way
<esap> sure, I can proof read the paper, if you have time to write it.
<bourbaki> yes thats what id need help with and im a bit clumsy and dont see the necessary details in 
  some points
<bourbaki> i hope that dons will participate cause i dont feel competent enough to do it all alone
<bourbaki> i wanted to make this my thesis but i dropped out but i feel that i need to finish this 
  somehow :)
<bourbaki> ok anyway thank you for all your help ill post the discussion to dons and hope that he will 
  get a little more insight in what its all about
End of esap buffer    Wed Sep 13 21:22:17 2006