Start of esap buffer: Wed Sep 13 21:22:17 2006
Session Ident: esap (n=esap@a81-197-156-147.elisa-laajakaista.fi)
hidiho sry that i query
you
would you maybe interested in participating to release a paper for the new ifl07 next year?
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
hidiho sry that i query
you
would you maybe interested in participating to release a paper for the new ifl07 next year?
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
what kind of paper?
what's the topic?
I have quite busy schedule, so I can't do much work for a paper.
the topic is extending the arrow stuff to petri net like programs
if you want ill send you the 4 small files and you can have a look at it
I'm interested in reading it
from what i remember of talking to you some time back you might be interested
ok cool what addy should i send it to?
its just a super small sample
esa.pulkkinen@kotiposti.net
ok sec
ok the mail is send
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
it's not clear to me whether your pictures are at the level of values or at the level of types.
its at both i think
if you have cyclic programs/graphs
you need an interpreter cause you cant use the arrow operations to fold it to a single arrow
so the interpreter is at the value level and for debugging issues and such
once you
"compile" the program to a single arrow its at type level i think
i hope that makes sense :)
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.
but if it's the value level, then I don't understand your description of it.
well if its one of these choice arrows its the right direction isn tit?
i guess its rather on the value level though cause its quite inspired by perti nets and data
flow
ok let me think a sec about this.
sure take all the time you need
how do you distinguish products and coproducts?
what do you mean by coproducts?
Either a b
ah ok
well you would need to tag the node for that
but basically it will be sufficient to use the right type at the target node
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
and since i dont want to allow to mix that this should surfice
I'm wondering about the 'parallel processes' picture, which represents (***), I was wondering how
your pictures could represent (+++). Is it the same picture as (***)?
whats the exact notion of +++ again?
a b c -> a b d -> b (c ,d) ?
er
(+++) :: (ArrowChoice a) => a b c -> a b' c' -> a (Either b b') (Either c c')
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
that is if its deterministic and you can just choose one of the other path in the graph then
its +++
but if you cant garante that youll have to use the a (b b') (c c') notation
the same accounts for the split of two processes for a if then else structure
id really split that and then join them again
ok I think I see what you're trying to do
do you think that it is worth writeing a paper for that stuff?
i think that especially the topological stuff over these graphs is interesting like the
quotient spaces and such
and also you can unlike in usual automaton theory connect programs in other places then the
first and last node
that's the part that I don't understand well, perhaps because I don't really know topological
spaces very well
well its pretty easy
if you have the usual graph notation
G = {E, V}
V = ExE
then the gluing thingy i do there is just
G1 + G2 = {E1 + E2, V1 + V2}
what's the '+' there? coproduct?
and the ~ operator the quotient space just make elements in E1 and E2 equal and thus the ...
er sec
E = VxV :)
yes + is the coproduct
just adding up the two lists in this case
a small example
G1 just consists of two nodes and one edge
and G2 also
G1 = { {v1,v2}, {v1 x v2} }
G2 = { {v1_2,v2_2}, {v1_2 x v2_2} }
now we want to append G2 to G1
then you do G1 + G2 / ~
and ~ is
well it makes v2 and v1_2 equal and all other elements not equal
and thus you end up with
G3 = { {v1, v2, v2_2}, {v1 x v2, v2 x v2_2}}
is the equivalence relation used for the glue part of input to the glueing mechanism?
yes
all you would need to do in the graphical interface is connecting the nodes that are equal in
the new program
and with graph matching you can do the following
programX / subprogramY
that is you make a subprogram a single arrow which is what you do when you "compile"
ok that's some kind of abstraction mechanism?
so if you have two arrow in a program you can do this to make it use the >>> operator
yes
you can zoom out that way of your program
ok make some parts of the program look like black boxes
and the idea is that you just build up your complex programs by successively glue together
"simpletons" these arrow constructs
this is just like in CW constructions
CW?
http://en.wikipedia.org/wiki/CW_complex
c = closure finite and w = weak topology
ok, I haven't heard of CW_complexes before :-)
np :) but you more or less get the big picture of the idea?
yes. I'm wondering if the programs can really be represented as graphs.
well because on the execution level they are like petri nets they can
and you can mix different concepts
ie you can use a neural net just as a graph and mix it with a usual program
thats why i thought about that initially
well ok, but consider one link in a graph. Does it have some structure?
a link beeing an edge?
yes
ok all structure it has is the function its representing that is domain codomain and the
function body itself
other than the trivial structure of the pair of vertices
the structure is just the same as in usual arrow notation i think
the only real problem i have come by is recursion cause it expands the graph and thus needs
an interpreter
i thought about a (co)+algebra way
thus you have something like TxT -> T as in monads but also a T -> TxT to decompose it again
that is something that generate graphs from byte code or so
i hope im not eating too much of your time with that stuff
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.
yes that was one of the concepts i had in mind also
also i think it canonically forms a CCC
and maybe a topos if you allow partial application
but in that model, the gluing is interesting
yes i think thats one of the strongest points and the quotent spaces
so would you be interested in helping us at least if you are not able to write stuff?
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...]
because what you are comparing is clearly the vertices of the graph.
no i dont think so the ~ operator makes nodes equal but you can use it if you make edges
equal maybe that way
that is if you have a graph X and there are two edges in there
then X / ~ with ~ beeing an operator that makes the two edges equal might be interpreted as
useing >>> on the two edges
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
though if the compilation is propper all the outcomes should be equivalent under bisimulation
that is have the same results
I don't understand how ~ making two edges equal can be interpreted as composing the edges.
~ makes several elements in X one element in the resulting space
wouldn't such edges be parallel to each other
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
thats a matter of interpretation i think
if the edges dont share a domain or codomain
then its paralell
if they do its >>>
I thought if the edges are equal, they should have same domain *and*
I thought if the edges are equal, they should have same domain *and* same codomain
i think i was to sloppy there
~ doesnt make edges equal thats false sry
in the topology book i have its known as
zusammenschlagen
in english thats like ... beating together
ie you have a surface X
and you have a lake on that surface for example and you want to make the lake accassable as a
single element
then you can do the following
X / lake
then youd have all the grass elements in X and one single lake element
i hope thats not too trivially expressed for you :( but im bad at explaining
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.
in the same way i want to make a chain of edges availabe as a single edge
right
and if you want to build the quotient space of a single graph then ~ is something else
then ~ is a subgraph
let me see if i can find the stuff on the inet
ok. I think I see the idea.
http://en.wikipedia.org/wiki/Quotient_space_%28topology%29
the examples have gluing
in topology you can use the ~ also to build cells on your surface
and cell is here interchangeable with "chains" of edges
The glue operation is quite different than using the quotient on subgraphs.
the glue that i use is also useing points (vertices)
the other quotient space thingy is just aplicable on a single graph
the latter tells you which edges form a "cell"
let me get the book from the shelf for that sec
the problem is that its a german book
ill try to translate it
let X be a topological space
A is a subspace of X
and non empty
then X / A describes a quotientspace
X / ~_A
where
x ~_A y :<=> x = y or x and y are both in A
this is called beating together in german
hmm.. interesting. the definition of ~_A is opposite of what I thought.
so if A is a subgraph you make that graph a single edge
ah, no, that's wrong.
the text says further that in the new space A is a single point ...
you actually mean, that x = y is real equality, and ~_A is equality that combines all elements of
A.
ok I see, it's now clear.
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
so G / ~ is not precise enough here you are right there
A is a set of vertices there, right?
no its edges in this case
casue ie if you have two nodes of different type they cant be beaten together
the gluing together of two programs it then explicitly
program1 = { vertices, edges }
program2 = { vertices, edges }
and newprogram = { vertices1 + vertices2 / ~, edges1 + edges2 }
where the subgraph thingy would rather be
newprogram = { vertices, edges / A }
where A is a subset of edges
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.
and the cells formed that way are interpreted in the way that you get a single element(edge)
of the A
righht its reduced to a point where a point in this case is a single function/edge/arrow
so if you do this you zoom out/ abstract your program
that is just lets pretend for a while we can explicitly find while loops in our program graph
and you arent interested in looking at the while loops anymore then you can fold them buy
program / while_loop
thats a bit like the folding in modern ides just that its not reversable anymore so its like
compileing
and the compileing is dependant on the language you use
is there some concept that represents a "collection of edges from A to B"? like a Hom-set in
category theory?
i think so ... but im not 100% sure
you could just have a category of arrows
which is better then the edges form A to B just say
it would be an exponential object in the category of data types and functions.
Arrow A B
right and if i have those its a topos
which is why i need partial application to get these at least from what i think with my not
too deep insight in CT
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.
at least i think of exp opbjets as partial application
but that may be unavoidable when you're talking about concurrency.
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
exp objects are like haskell's "A -> B" type.
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)
but A -> B ~ arrow A B isnt it?
yes.
but at the level of *types*, not *values*
ah ok
its not that easy though to just operate on the type level
do you think that the idea gains anything if i include CT?
you might get some easier-to-work with formalisms.
i thought id gain something if i was able to say its a topos
but one problem is that concurrency requires some advanced concepts to model with category
theory. It's not easy.
but personally i totally like the topological approach but thats maybe because im familair
with topology
the idea for concurency was that you have an interpreter
and an intperreter is nothing but a functor
this it maps vertices (typed containters) to other vertices in the new graph
hmm. how do you make an interpreter as a functor. I thought interpreter is an arrow of type F A
-> A.
the updated graph that is
and the functor F represents the language being interpreted.
and the edges just id to the edges in the other graph
yes in my case a petri net
do you know petri nets otherwise ill just explain it its really simple
I know the basic notations, but if there is some deep theory, I might not know those.
no just the basics
ok, I do know basics of petri nets.
so the functor would have to look if all the predecessing nodes are fillend and then execute
the edges
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
er state monad
I'm not sure how that's a functor.
hm ... why?
a functor just maps vertices on vertices and edges on edges
so theres a functor for each state the graph can be in that translates it to the updated state
oh I thought in a different category.
Is it some kind of forgetful functor then?
and since you have the graph state as an element of the functor input you can choose the
right functor
forgetful functor F : C -> C , where C is the category that represents your graph
i have heared that before
yes more or less
it needs to be something like
F: CxState -> C though
cause the functor F depends on the state the graph is in
othewise you would have a set of functors and you dont know which one should be applied