foreign
[Music]
this will be a talk about
compositionality
uh it's probably a word that not all of
you know
and I'll try to explain what this is
about in the course of this Workshop
uh in the last months probably a year or
so we've been hearing a lot about
composable things composable blockchains
composable service
compositionality is basically just a
mathematical Structure Theory that tells
you how to do that in the most principle
way possible
uh
I'll start and if you have any question
just feel free to like raise your hand
and interrupt me and I'll try to answer
and or clarify
okay so first of all to introduce the
concept of compositionality we need to
introduce some basic building blocks
that are systems and processes
so compositionality is basically the
study of how systems compose to give
life to more complex systems
systems are basically things that can be
transformed enacted upon
and processes are exactly the things
that act on systems and transform them
uh a very interesting Insight from
Modern mathematics the mathematics
developed from 1950 onwards is that
often is way more fruitful to
understand something to describe it by
looking at how the thing composes and
behaves in a context so instead of
splitting things open and look how they
look on the inside we describe them by
saying how they behave
and how they interact
um okay so let's start with something
very very simple I will use a lot of
pictures in this talk and hopefully
close to zero mathematics
uh for people that love mathematics I
cannot that there is a soundness a
completeness theorem that says that
these pictures are formal which means by
doing pictures we're actually doing
mathematics it's just easier and more
beautiful in my opinion so in here we
have a very simple process that we
depict as a box it just takes a number
in input adds one and spits a number in
as output
I mean for I guess everyone acquainted
to with programming that's just like man
yeah okay
uh the point is that when we have a
process a process like that we can
compose it with other processes so for
instance
in here we take this process we notice
that it needs an input that is a number
and spits out an output that is a number
and we realize that oh we can actually
pipe this process with itself and if we
do that by just concatenating the boxes
you see that this will be equivalent to
the process that adds to to your input
now this seems very
naive but the nice thing about this
picture is that it goes both ways you
can start from the top row where you
have simple components and you actually
abstract away so add to uh is basically
just you know the dotted box
encompassing the two or you can do the
opposite you can start from a process up
to and open it up and further specify it
with a finer degree of accuracy and
since you have an equal sign you can
basically go both ways
now there are very peculiar processes
that that are called identity processes
these are the processes that don't do
anything in this case with the number
example we have a process that is at
zero that takes a number in input does
absolutely nothing with it and spits the
same number as output
the good thing about graphical reasoning
is that since this thing is not doing
absolutely anything we can just not draw
it
and indeed I'm drawing it as a dotted
box uh down here just to
highlight that there should be something
there
but you know with this very simple trick
we can already start proving some
equations
that are very simple so if I add one and
then I add 0 is like just adding one
right
if you know you adopt the convention of
not drawing identity processes then the
picture on the top row just looks like
the one in the bottom row while you have
stretched a wire a little bit more
similarly from I don't have it here on
on the slides but you can understand
that in this formalism the composition
is associative we don't use parentheses
if you concatenate three boxes one after
the other it doesn't matter in which
order you obstruct them
in the end you only have three boxes so
it doesn't matter how you group them
okay let's do another example
so
for this example I'm using gravitation
gravitation that has absolutely nothing
to do with crypto I admit uh at least I
I think I don't know maybe
uh so we have a system that is a sun
that is just sit there and you know does
nothing and raise the earth that is
orbiting around the Sun
so you know
during many centuries people thought a
lot about this and at some point
basically a guy called Newton found out
that there is a process that you can
call evolve
in which you can feed
a state of your system and then you can
say okay show me what happens one second
later
and this is a beautiful predictive power
of physics in this case of dynamical
systems that allows you to start from
some experimental evidence and predict
what is going to happen uh in the future
you see that in this example you also
have an identity process that is the
process that doesn't evolve evolve for
like zero time it's just taking the
input and is not looking in the future
or in the past it's just giving you the
state that is as it is now
and we see that we have a notion of
composition because if I let evolve the
process for I don't know one second I go
from the position Mark type t0 to the
position Mark T1 again I can feed T1 to
the system another time let it evolve
for another second and I go to T2
and that would be the same of evolving
the system for two seconds so again I
can combine These Bricks
now the important thing is that anything
that matters everything that matters in
this formalism is how things are
connected you can deform the wires no
problem what you can't do is you cannot
make new connections or splitting
connections if you do you are getting
something that has a different meaning
another important thing is that you can
only compose things with matching types
for instance senior I have the Hub one
process we saw that that spits out a
number
but the evolved thing wanted something
of type sun earth as an input so you see
that it doesn't really make sense to
compose these things because they are
apples and pears
Okay so
this tells us the types in this
formalism are very important the way you
type your processes changes what you can
and cannot compose
okay as an example imagine that you have
a car right you have
the wheel and the shaft and the gas tank
and you could see this as a process that
takes some inputs for instance I don't
know fuel or and Human Action and
produces heat and motion
but when you look very carefully you see
that you could pour any liquid in your
car right like
the gas tank won't complain if you fill
it with water
clearly the engine will though
and basically from this you can
you know infer that the problem here is
that the type of input of our process is
to General
and it allows you to fiddle with the
process in a way that produces
unintended Behavior another example that
I like is imagine a socket in the wall
you can put a plug into it
and you know use any electronic
Appliance but if you have a couple of
nails you can also stick the nails in
the socket and what you go what you get
is emerging behavior all over you and
very painful
so
the important thing here is this is the
main message of compositionality so when
you look at this process like the socket
and plug process
you can start asking what are the
properties that are preserved when I
compose these processes together
so physically sticking the nails in the
socket makes total sense because they
fit
but if you're looking at things through
the lens of safety regulations you see
that a nail can be safe can you know be
certified with whatever standard your
country has
same thing for the socket but when you
compose them suddenly you have a very
very unsafe system
compositionality is exactly the art of
choosing these types in a way that
emergent behavior is averted as much as
possible so that when you compose things
you know precisely what is going what we
are going to get
now under the hood
compositionality is based on a theory
called category Theory this was invented
in 1942 and had a monstrous impact on
Modern mathematics essentially you can
see it as a super glue of mathematics
that describes how different theories
compose and interact
basically all the main progress in you
know big areas of mathematics like
algebraic geometry or algebraic topology
come from here
and in the last year people started
realizing that this thing can be applied
also outside of mathematics because
again it embodies this perspective that
you can describe things but looking how
they behave in a context
so
when I show you those diagrams what I'm
really doing I'm always speaking a
category that defines the universe I'm
working on and working in
uh let me just dig a bit deeper into
this idea so
if you want to define a category if
you're a mathematician you want to
Define it formally basically you have to
specify various entities you have to
specify objects that correspond to
systems in the pictures I showed you
before so objects would be the wires
in the box and wire pictures you have to
specify morphisms that are the process
the boxes that transform objects into
objects
you are required to specify identities
so for each system you need to have a
process that doesn't do anything
to it and then you basically have to
specify a composition law uh a recipe
that tells you what happens when you
compose processes together
uh let me give you some examples of
categories that are probably familiar to
uh I hope as many people as possible
here there's a category called set where
your objects are sets and your morphisms
so your processes are functions between
sets there is always a function that
doesn't do anything and you can pipe
functions into each other
for programmers there is another
category called Data where your objects
are data types and your programs are
programs that turn data types into data
types
again you can compose programs this is
basically functional programming Style
programming you can pipe you know the
output of a program into the input of
another program if the data type matches
and you are also a program that just
Returns the input without doing anything
so what is the difference between these
two categories
well set offers an intention sorry an
extensional perspective what it means is
that for instance if I consider the set
of integer numbers I have exactly one
function that takes a number and adds n
to it
on the contrary in data I have multiple
ways of either specify what integer
numbers are and I have multiple programs
that sum n to your term in here I just
brought two of them but in general you
see that in the car in the category data
the formalization the implementation
matters
so these two categories offer very
different views on the same phenomenon
in one case you're saying I'm only
interested about behavior I'm not
interested about the inner workings of
these functions in the other one you say
no I do and I distinguish two processes
they could uh emit the same output on
the same input but I want to keep them
distinguished
now the cool thing about category theory
is that you can connect these different
perspectives there is a notion called
functor that turns a category into
another category in our framework this
would be a box that is sort of like
level two box that allows you to change
the universe you are working in
so
um basically what you do to define a
functor is you specify a mapping from
the object of the category C to the
objects of the category D so you have to
say where systems of C go in D you do
the same for the morphism so for each
process in C you have to map it to a
process in D and and this is the
important thing these mappings have to
map identities into identities and
compositions into compositions so what
it means is that if I compose two
processes in C and then I use the
functor is the same of using the
functions on the components and then
composing them in D
questions or sure
not necessarily you can have functors
that are called full and faithful that
allow you to yet basically be inverted
and go one direction to the other but no
in general these can you can lose
information or you can embed embed a
less expressive Universe into a more
expressive Universe if you want to
sure
it's like
sorry
factors as information so I don't
oh linear transformations
uh
maybe I don't know like there is this
very convenient thing that in category
Theory everything is everything else
like not going in depth into that but
you can describe a category as a factor
and a functor as a category and blah
blah blah so it it is possible maybe to
describe a function as a sort of linear
transformation in general what I can say
is that you can Define categories of
vector spaces for instance and in that
case your morphisms your systems will be
linear applications that respect the
linearity of the vector space uh yeah
you know
uh yeah yeah this is exactly what
happens because this thing is basically
mapping processes of C to processes of D
so you can see it as an higher level
function and indeed a factor is a
process in the category of categories so
you can do this kind of you know level
up
let me give you an example of functor
this is a function that actually
collapses information we saw two
categories data and set and we can
define a functor that sends a data type
into the set it implements and sends
every program to the function it
implements so this is exactly what I was
saying before
that you can start in the category data
and be you know very detailed about
distinguishing things and then you say
actually I don't care I want to collapse
all this information and I want to
forget about you know these different
details you apply this functor and
that's exactly what you get all your
process compositions now you know lose a
part of information
obviously there are very interesting
questions like how do I invert these
things can is there a procedure to
canonically invert a functor and
actually go for instance from just a
specification to sorry from a behavioral
extensional perspective to something
more complicated sometimes you can
sometimes you can
I don't think
yeah
so imagine that int is a data type that
you define I don't know inascal uh about
integers
that data type is basically modeling
the set of integers in a computer right
so conceptually you can say I can send
that to Z similarly if you have the data
type string you can have a set of all
the possible words on an alphabet and
again you can send string to that set
uh with this functor basically what
happens is that these two programs here
get mapped to the same function between
sets
so I have two different implementations
of the same program that maybe you know
I consider separate as programs like if
I for instance hash the one on the left
and the one on the right the hashes will
be different
uh but they correspond to the same
function they are implementing the same
function so when I go from data to set
i'm I deciding willingly to lose that
information
okay let's try to use what we got up to
now to do some process design that is
actually the interesting part of it
this is a very simple example imagine
that you have a grid and you want to
define the process of moving on this
grid so
imagine that you can only move of you
know a kind of fixed amount of things so
it's not like I cannot move like 0.1
steps but only one step at a time
in this case you'll see that wherever
you are there will be four fundamental
processes that are up down left right
that allow you to move one step and now
I can basically describe every path as a
concatenation of these processes so for
instance if I move three times right and
two times down I'm describing the L part
I have there if I feed to this process a
couple of coordinates that tell me where
I am then these coordinates will be
transformed as in the end of the path
basically
and we see that in this kind of theory
we also have some equations like if you
move right and then down does the same
of moving down and then right you are
describing a square you are just walking
in like different paths but you end up
in the same place
let's spice this up and let's do it
concurrently now we have multiple agents
uh wandering on this grid
and we want to model you know how they
move
intuitively what you do is well now we
want to consider processes that happen
in parallel like if I have two agents
for instance I can have this process
here that says agent one moves three
times on the right and agent two moves
down and then on the right and now we
see that new equations pop out so for
instance I have this equation here
called The Interchange law that
basically says these two threads are
separate
you can see the first are saying I move
somewhere internet do nothing the other
agent does nothing in which for you to
move and then moves
in this setup is the same if you just
you know swap the things and second
agent moves first and first agent moves
later
why because intuitively these two agents
are not causally interfering with each
other agent one doesn't care at all
about what agent 2 does and vice versa
and so in these formalization of moving
on a grid concurrently I have these
extra equations
mathematically we say that the Universe
we are relying upon is not just a
category but it's something called the
monoidal category that basically means a
category where you can do also things in
parallel
okay let's do uh more like programming
oriented example so let's consider a
very simple record uh let's call it
person uh This Record has two Fields
name and surname okay
um now
you can notice that in this record in
this example person is basically just a
couple of terms of type name and surname
now we want to be able to you know
functionally describe the procedure of
extracting a subfield of this record so
you give me a person I give you the name
for instance and we also want to be able
to replace the subfield of a given type
with a subfield of a different type this
is a bit more complicated but what it
really means
is that for instance imagine that I want
to edit this personal record I want to
strip surname out and put a new field in
called age
that is of different type so the point
is how can we do that
in a automated and more importantly
compositional way
uh so what I mean by compositional is
Imagine This example where I have the
record person but one of the fields is
itself a record it's a sub record
and now I say okay I want to replace the
city thing there Bogota with something
else intuitively I want to be able to
pipe the process for editing person with
the process for editing address and you
know feed these compose these two
processes in a way so that I don't have
to reinvent the wheel every time
the way you do this in a functional
programming and in compositionality is
with something called a lens that is a
particular example of something called
an optic
so what is the idea uh the idea is that
the lens is just a couple of processes
one called get and one could put
and basically get is taking your record
and is giving you the subfield
that in this case is s subfield of a
what put does instead put is taking your
record a is taking something of type T
and intuitively is replacing s with t
and now it's spitting out something of
type B you see the type of a could
change because you replace the type of a
subfield of this thing if a was a couple
of strings with this put I could
substitute a string type with a nint
type and then the overall type of the
record will change
the funny thing about this is that you
know there is an ask a library for
instance that allow you allows you to
automatically get these things for every
a s and t as soon as you define your
type A this thing will you know create
the Setters and Getters automatically
for you so it's a it's a procedure that
you can automate and that's the cool
thing you don't have to do it manually
the library does it for you
okay so I'll do these things compose
imagine that I have two lenses so the
first is taking the subfield s from a
and the second one is taking the sub
field V from s the get part is easy
because you see you can just
telescopically access the records you
can say I start from a I pull out s and
I pull out V from s
the part is a bit more complicated so
what happens here is that imagine that
in S I am replacing the subfield V with
a subfield W and I obtain something of
type t
and now I want to replace uh s with this
type B into a how do I compose these two
things well with this sort of like
monstrous awful thing here in in the
bottom where I basically take a I copy a
I get S from a now you see I can use
this put put V and basically substitute
uh V in s with W I get something of type
T and then I can use put on T and A to
get a B
I know that this sounds very cumbersome
and difficult to follow
but the good thing is that you can you
know topologically deform these diagrams
and basically Express them in a way that
makes way more sense so in here instead
of considering this funk these things
are two couple separate processes
I'm you know packaging them as a unique
thing
so as you can see this thing is a bit
strange because it has arrows going in
opposite directions so on the top row a
gets processed into an S so you are
extracting s from a on the bottom row
you are getting this t on the right and
you know you are writing s with t and
you're getting a B on the left
this is an example of a bimodular data
accepts accessor the way you can think
about it is as a process that says if
you give me an a I will read field s and
forward the output to you and if someone
else from the future will give me a t i
will replace S in a with it and return u
a b and the good thing about it is now
you can compose them exactly as you
composed the processes we sew up to now
and when you do this if you squint your
eyes a bit you see that we are doing
something that is basically equivalent
at that um to that cumbersome
composition we had before but now is
again graphical like you can just
compose these Lego bricks together
again and this is the art of
compositionality anything that really
changing is the point of view so you can
still deform this thing in another way
I'm just rewriting the top diagram as
the bottom diagram if you see the
interconnectivity of the diagram didn't
change
and I can shape it as a comb basically
and again it's the same like you get a
in you get an S out then you get a t in
and then you get a B out these is really
interesting because when you look at
this comp process it really looks like
something that wants to be a normal
function but it can't because it's
waiting for you to do something
intuitively if you have an automated way
to turn S into T that thing would just
be one of those naive building blocks we
saw in the beginning
and you know in this framework the
composition will be nested he would be
of this sort you are basically composing
comms by substituting a comb in the
whole of the bigger comp
and again this composition is exactly
the same when you follow the the
processes and the interconnections of
this one this one and this one are the
same thing we just deformed the way we
arrange the diagrams
now again as I said you can see a comb
as an incomplete process
that basically is waiting for you to do
something to turn a nest into a t and
that would be that F that you put there
and if you put it there this thing
basically closes up and just becomes a
normal process
but what is really interesting about
this
is that we found a pattern so we started
by modeling record rewriting but now we
found a new pattern of composition that
is this kind of nested composition and
indeed there are a lot of things that
compose in this way if you abstract from
details for a second
these two processes are basically
representing two different points of
view of the same thing that is
bi-directional transformations
now let me give you an example of how
you can use these things
an example would be estrus what is an
escrow trade an escrow trade is when I
want to give something to someone but I
don't trust that someone or that someone
doesn't trust me and so what I do is I
take my funds instead of giving them
directly I lock them up in a vault
and then basically you know my
counterparty will ship me some goods and
when I receive them I will confirm that
I received them and at that point my
funds are unlocked and forwarded and
that is exactly a calm looking thing
it's like I committed my funds I locked
them and now I'm waiting for
confirmation and as soon as you give me
confirmation and you put it in.com then
this looks like a standard transaction
from A to B
another example and this will be the
main
point of the second part that my
colleague Philip will do is Game Theory
so
we can model games in Game Theory as op
as open processes basically
in that case a game will be a process
that has again two inputs and two
outputs
it will take in input and observation so
it will observe the word it will spit
out an action According to some strategy
if we receive a payoff from the outside
world
and you will return a feedback
the feedback is probably the most
difficult part to get in this
composition method and you have to
imagine it one of the ways to imagine it
is is the portion of your payoff that
you have to return to someone else
stupid example if you take a depth you
place a bet you win you get a payoff
that you have to repay the debt and the
debt repayment would be the feedback
wire
in this system of compositional Game
Theory
we can recover traditional games as a
composition of processes
so this for instance is the prisoner
dilemma uh I guess a game most of you
are familiar with and normally we see it
as a payoff Matrix and you know like if
player R does this then this is what
happens if player B does that blah blah
blah in this case prisoner dilemma is
the composition of three different
processes
player one player two and payoff Matrix
these three things in isolations are
games
player one and player two are games that
do not observe anything because you
don't do any observation in the prisoner
dilemma they just act they just you know
Express a choice and they receive a
feedback for that choice the payoff
Matrix gain is a game that doesn't act
it doesn't have any strategic value but
it just observes
the players move and returns some
feedback and again you see that in this
setting
the players payoffs are the payoff
Matrix feedback and the player's actions
are the payoff Matrix observations
so yeah the cool thing about that is
that now we can quickly prototype games
by basically creating these blocks and
interconnecting them with each other one
thing we are currently working on uh and
Philip will show a demo of this
is for instance a way to lift evm byte
code to open games automatically in
doing that you know if you deploy a
smart contract we can take your smart
contract and put it into this framework
and then we can strategically probe it
your smart contract would become like
the payoff Matrix in the system and then
we can economically probe it with
players that can be honest or
untrustworthy and see you know which
strategies are actually winning
strategies or not and so if your
contract is economically sound
economically stable or not or in within
which bounds it operates financially in
the way you intended
so this is the theory part that is
concluded and I will leave for the
second part everything to Philip uh and
basically yeah in this short tutorial we
saw how we can use this compositionality
techniques to guide our intuition in
designing processes we started with
something very simple then we start we
did a bit more involved the
um examples and then we found out that
those examples were actually modeling
and more General pattern this
bi-directional composition
and we were able to basically recycle
that pattern to instantiate other things
like escrows or open games
and yeah that's everything for me and
I'll just pass it to Philip thank you
[Applause]
if you have any questions
if you have any questions we can in the
meantime that Philips up the computer
feel free to ask sure
uh the final
uh yeah uh
I I mean in here I kind of cheated
because I basically just defined an
optic as
you know this box obstructing the
details indeed mathematically you can uh
prove the I mean the definition of optic
is exactly something that embeds that
thing mathematically it's a bit
complicated to describe uh but
graphically that's exactly what it is an
optic is something that has this sort of
nested notion of composition basically
sure
yeah there are various ways to do that
uh Philip is the expert in this and I
don't know maybe you won't
yeah sorry um what's your question
whether you can also do repeated
ly
yeah
yeah you can do that
um so the game that for business short
is a one shot game but you can also
think about this as taking that let's
say you want to iterate it finally many
times you just stack it on each other
the only qualification you have to make
um if you looked at the slide they were
basically the
um the the wires were not coming in from
the outside you have the game with wires
and then you can stack it basically
alternative way to do is also you can
turn it into a Markov game which has a
state and then you can basically think
about it as approximating it to be run
infinitely
okay other questions to the first part
there is a question in the first part
um let me do the following I'm trying
I'm jumping on my slides ahead
um
to show you this
then I will go back
ah sorry could you guys sorry can you
switch on the okay
um let me go to the
so here
um you have to think about it as two
Dimensions right so time flows from left
to right and if you start from the left
there are two things P1 and P2 they are
not connected which means they happen in
parallel so this is simultaneously
happening then afterwards they output
the move which is y1 and Y2 that move is
consumed by U which is the payoff
function and in that sense you follow
sequentially after these two games right
you can also think about these two games
P1 and B2 being merged into one and then
it's just big two games being stacked on
top
okay so let me go back to the start
you can already see what is coming
okay
um so what we want to do in this in this
part in the second part by the way hi
I'm Philip thanks thank you all for
coming
um what we want to do in the second part
is basically take a deeper look look at
compositional Game Theory as one
specific instance of
um how you can think about
compositionality and what
compositionality possibly can give you
as value to
um as an approach to thinking about in
that specific context of strategic
interactions
okay compositional Game Theory what is
that actually so it's a at the beginning
actually this was a research project
which was focused on providing a new
formal language for game theoretic
reasoning yeah you probably have heard
about Game Theory many of you probably
have already seen it it's a mathematical
language to express the reasoning about
agents and what we provide is just
another language in some sense
now this language is as for pizza
already introduced based on the
categorical framework and this has
several consequences one is you give you
first of all you get a graphical way of
reasoning but most importantly you get a
way of compositionally approaching the
modeling problems
um that you that you face okay now if
you just do the diagrams and you you
know suppose you would be forced of you
know using diagrams for very large
systems like a staking protocol or other
complicated more complicated systems
that would be limiting it would not be
that much help it might be a cool new
Theory it might be of interest because
some academics but practically maybe not
so much relevant
what is up what however is a consequence
of what also for pizza already said dami
there is a very close connection to
Optics and Optics allow more or less
these things to be directly implemented
enabled us to also develop on the site a
software tool which basically takes the
language of category theory for modeling
games
and turns it into a software framework
that you can use that supports your
modeling process and that's the key
thing because if you would be forced to
doing things on pen and paper well yeah
would not be that practical once you
have this Tooling in the back then you
can actually leverage
um the basically the benefits of
compositionality and the purpose of that
basically second part is hopefully to
convince you that at least this might be
interesting and hopefully more that this
might be really useful
okay so a large chunk of the talk will
also focus on the implementation so what
does the implementation actually provide
um first and foremost it's just a
framework in which you can express and
represent strategic interactions like
the prison dilemma but obviously also
more complicated stuff
many times you're not only interested in
representing models but you naturally
are interested in you know what kind of
behavior may result from these models so
you want to you also want to analyze
them in various ways in the current
engine there are basically three ways to
do that one is interactively so you
basically run a session and then you can
query
um your model let's say I'm looking at a
stake staking protocol and I have some
idea what would constitute an honest
strategy of the participants and then I
can ask okay if I'm feeding in a
strategy this is actually an equilibrium
or do specifications have an incentive
to deviate and the way it works is a bit
like a proof assistant it will tell you
you know your proposition that these
strategies make sense either makes sense
and then it's good or it will they will
the compiler or the engine will tell you
wait at least one agent basically has an
incentive to deviate and here's the
incentive here's a specific action that
this player can take
um
now the interactive part is very useful
to explore parts of the model and for
the staking stuff we will also see an
extended example on this it's quite
useful to think about specific vectors
of attack and then you can verify does
this actually work or you know what two
specific agents actually react to If a
strategy of another player changes
you can also think about this for pizza
alluded to that
um that there is a system a which is
somehow represented as an open game or
several open games you make changes in
that system these changes propagate in
your open games and then in the back
you're running tests on what kind of
behavior would you expect from this kind
of system yeah so it might be that you
have an incentive mechanism and it works
but you make a change to the overall
protocol a how does that actually is
then this is translated into the open
games framework and in the back you're
running tests on the behavior of the
agents and then maybe things go through
or you get a warning something is not
working anymore as before
and lastly theoretically as well as from
a practical implementation perspective
there's a very close connection to
machine learning framework specifically
reinforcement learning I will say a bit
more at the end if I have time but the
idea basically is that you can either
leverage reinforcement learning
techniques and machine learning
techniques more generally for solving
and analyzing games solving of course
has limitations because it's very
complex but for some specific games it's
feasible and on the other hand you can
also turn it around you can also make
Learners basically part of the game so
that you have an interactive interaction
of learning agents basically
which is also quite useful because you
basically have to think about this as
you know institutional players
um updating or actually um Learners
themselves as part of the
um of the model for instance in pricing
settings
okay
um
what's the key Innovation well
compositionality obviously that's a key
point but what does it actually mean
here
if you think about the prisoner dilemma
what is already showed um is that you
can think about the prison dilemma at
least from what you have seen so far as
either one monolithic building block or
at the minimum you're splitting it up in
three components right now for a
prisoner dilemma that's not that
relevant but the more complex your
scenarios become the more helpful it
actually is to say look I'm taking that
part I'm zooming in I'm modeling it zoom
out take another part model that zoom
out and so on and so on and later on if
you do it right you have basically
systematic ways of composing these
things together into a bigger model
now
this doesn't end at that level you can
also for programming purposes or because
of convenience you can further
um modernize your code let's say there
is a specific thing a specific way you
want to approach it you can split this
up implement it in different ways and
the key thing about all of this
basically so far is that
all what you're doing will be guaranteed
to make game theoretic sense if you
follow basically the syntactic
descriptions or restrict restrictions of
the engine that means you start out
modeling if you use our language you end
up you can decompose things each of
these components will make sense from a
gametheory perspective and the composed
thing will also make game Authority
sense that's compositionality at action
why is this useful well you get an
overall few on the over on the on your
situation that you want to model and it
is sound and you can ask questions like
okay what's equilibrium of that or you
know if we repeat it um a Serial
deviation strategy if you think about
more um like a Markov strategy for
instance other ways of
um deviating that a profitable
profitable for specific players
another perspective basically is that
this turns the pro the modeling exercise
into a programming exercise so the idea
of zooming in and zooming out I'm sorry
and you know modeling Parts in isolation
is more or less just like divide and
conquer a typical pattern that you would
apply in any kind of or many programming
um problems
okay and the key thing again is you can
modulize your code further we will see
this later on we will you know we will
have regular High School functions that
we just lived into that and you can
change these components but as long as
you're staying inside of that system you
are guaranteed that these things make
um are kind of well-defined
no warning uh the fact that is uh this
is game 3D well designed well well
defined does of course not mean that
your model makes sense you can come you
know you can model complete garbage
um we can't help you with that if you're
you know really intended to do that but
what we can guarantee to you is or what
this kind of helps you is at least in
the process of modeling we have a
scaffold that you can use
all right so how is this useful
um
the main thing basically is I alluded to
that if you have you know if you can
apply divide and conquer you can easily
deal with complex scenarios
um it overall also speeds up the process
of modeling in several ways first you
know division of labor so in principle
the larger the systems you can actually
very easily collaborate with people
um secondly if you want to change a
component you can easily do that as long
as the rest stays intact and lastly
because everything is expressed as code
there is obvious reuse for components
and you know we have been said we have
had several projects in the past and we
can see that there are some patterns
that just emerge that you can use over
and over again which is useful because
it speeds up
um down the road how um you know and you
want to model something
foreign
you can also think about it as just
being part of a larger stack where
um it's just feeling a proper it's
fulfilling a certain um service
um like testing properties again on your
on the safeness of the system from an
economic perspective
okay this is kind of the introduction
very roughly what this engine is doing
why it's possibly useful why it's maybe
interesting what I want to do for the
rest of this Workshop
um and for basically the second part I
will give you an intuition about how to
model with this tool how to represent
games and again the focus will be on
showing that compositionality is
actually useful or hopefully useful
um secondly I will also give you an
intuition of you know how does an
analysis actually work what does it look
like
I will be shorter on that second part
the reason is in order to make sense of
the analysis you obviously have to have
a deep understanding of the model
um this is given the type constraints
not really feasible but I still will
give you an intuition of how does it
actually work how does this look like
okay and a leading example
um that we will converge to is basically
a staking protocol it's a simplified
model that illustrates
um these two components of
compositionality and also the kind of
analysis you want to run in this in this
system
good I start with not code but directly
coming back to what for pizza actually
namely um introducing a bit Theory this
will be partly repetition but it doesn't
hurt it will be mostly about diagrams so
not much mathematical content the reason
I do this is the theoretical approach is
more or less directly the way that
implementation works model is some kind
of difficulties in the back obviously if
you understand how the modeling on the
theoretical side works you basically
have a very good idea of how then the
syntax actually works and operates and
that means you also basically know how
to use that that
um
that engine basically
okay so you've seen this this is a
bi-directional information
transformation Transformer from both
sides so X is transformed into Y and
then there's something coming from R to
S both directions again convention is if
you want to think about this is that
time is from time is on the left so on
the side of X and S and the future is
basically the passes on the X side and
the future is on the Y side
okay now in some sense in the essence of
compositional game theory is that what
we showed is any kind of game that you
want to model has this shape and can be
put into this shape whether it's just a
single player making a decision which is
kind of a non-typical game or a very
large complex system many players moving
and interacting everything can be
modeled in that shape whether it's very
large or very small
now why is this good or why is this
useful well it's useful because you can
start out with small components like one
player maybe just also computation
something very trivial and you can plug
these things together and slowly from
the bottom up yeah like Lego blocks you
can build up a system that is quite
quite complex and of course because
you're programming you can also kind of
box things and say well this is a
pattern maybe two players interacting in
a certain way this is quite useful you
know I'm giving that a name and I'm
going to be reusing that component over
again
okay so everything is of that shape you
know so it's a bit like it's like a
closer closure property in some sense
you start out with a number you add a
number you end up with a number the same
here you started with one game compose
another game you end up in another game
and this is in some sense what I
referred to before as this guarantees
you that you stay in a formerly well
defined framework
okay let me come back a bit to the
concrete Implement concrete
interpretation of this specific box and
for the next few minutes think about
this box as just one player doing
something now one way to think about
this is essentially the player is just
doing some kind of information
transformation right so there is
something coming from the past a move
information whatever X the player
observes this and internally something
happens he's outputting a move why okay
now the question of course is what kind
of move will a player make this depends
on what what kind of moves he has
available but it also of course if it is
a game theoretic agent Let Me Assume for
now it's a rational agent who wants to
maximize something he needs to think
about what's my effect of choosing wire
on my utility
and you see that the wire is an open
wire so it doesn't really specify
exactly how it is interacting yet within
my with the environment
but what we can say is the player is
expecting an R back from the environment
and this openness between my action Y
and the payoff data or whatever actually
are is in fact what I receive from the
environment that openness makes it
possible to take it like a building
block put it in specific situations and
then sometimes I might be able to close
the loop
um in a certain way the most trivial way
of closing it would be I have one player
and I'm just bending the Y back into R
and then basically my why my action that
I take will be directly to think that I
observe and I affect I have full control
basically
most interesting scenarios from a game
theory perspective are obviously not
like that but my why will not solely
determine what my payoff actually is
like in a prison dilemma there's another
agent doing something and this will also
affect my payoff
and of course this is the idea that at
some point we will give a concrete
environment which determines how this y
actually spent back into a specific
payoff whatever or whatever result you
actually care about as an agent
okay so that's the basic structure
now I said before we are building up
from the bottom
what we want is we want to compose
larger games by composing simpler games
and what we need for this are
essentially two kind of things we want
some building blocks think a bit you
know again like Lego
um you have one specific thing and from
that if you have it and you have more of
them you can just build up a wall for
instance
so we need the building blocks the
atomic units if you like and then we
need operations how to compose stuff
on the buildings on the atomic building
blocks we have essentially two which is
a decision a single player making a
decision
and the computation computation means
just some input is observed some output
is basically the result
um
these these computations can have side
effects so it could be
um actually a deterministic input is
turned into a probability distribution
or a probability probability
distribution as an input is turned into
another probability distribution
good what are the composition operations
for those of you who already followed
for pizza you will already guess it it's
parallel and sequential composition
um parallel in the game 360 is maybe
more easier interpreted as simultaneous
and what this looks like essentially is
again repeating a bit of what we have
seen you have two games do you want a G2
if they are in parallel you can compose
them and then they again will have this
basic shape of input X cross the X2 X2
in that case turned into a certain
output and it's the same time expecting
a certain result and sending some
information back into the past
okay sequential composition we have G
first H following you can stack them on
each other
so that they look in the following way
now what is important so far I haven't
said anything about what these labels x
y and actually correspond to
um you can think about them as shapes
and only games that actually have the
right shape can be stacked on each other
and this is important because you know
if I say you know give me two games and
I can compose them you might wonder that
sounds weird how can this be possible in
generality right I can easily come up
with two games that are not so easy to
or maybe not at all composable
the Restriction that you have is that
these shapes the labels here actually
have to match up only then can you stack
games together
forbidity already set from a categorical
perspective and then of course also from
the programming perspectives perspective
these labels will be types so only if
the types match up can you actually
stack games together this is quite
useful
um and it's actually an important
restriction because you know if let's
say G is outputting a Boolean and H is
expecting a numerical value a numerical
type
you can't match them up basically right
what is even more important if you try
to do that the engine in that case the
Hustler compiler will loudly complain
that this is not feasible you can't do
that
what is more because you can't obviously
design your own types you have also
degrees of freedom of you know being
very specific about what kind of input
type is actually expected yeah so it's
basically also part of the modeling
effort that you can you have control
over
um how easy is it actually to
um stack these things
okay and full circle back to the
prisoner dilemma again I already alluded
to it just very briefly what is this
actually representing
um two compositions first parallel or
simultaneous between P1 and P2 and then
sequential
um the U and again if you go back to the
parallel composition you can basically
think I'm first composing the two
players in parallel into again this
shape and then I'm composing that one
sequentially with the utility function
of the payoff function
okay
questions so far
can you explain why the utility function
is applied sequentially
um
yes in a sense of
the the utility function essentially is
just a computation right so it's waiting
there for you and it's waiting for two
actions One Way player one and remember
player two so it has to wait until these
action these actions realize in that
sense it's sequential in the
implementation that I that I show you
will decide this directly as variable
output of P1 being fed into the U okay
other questions
okay
um implementation first a bit of an
overview
so what is actually what does the
implementation actually look like it's
uh the main specific language embedded
in Haskell
uh you might wonder why Haskell
um one of the reasons is that and
repeats are already status as well as
well the Optics and lenses are something
that exist and you can build
implementation basically on pre-existing
structures in Hesco which is nice
because
um your theory has a direct
correspondence to the elements that you
use for the implementation in other
words it makes it also easier to control
that your implementation actually is
correct
okay another thing which is quite useful
the typing system of Haskell is um
actually
um can be
well sometimes your enemy but sometimes
also your friend if you have larger
components larger operations and you
wonder what inputs if you want to query
games do I actually have to supply the
type system is quite useful because it
can it infers the types and they can
tell you your strategy that you have to
supply has the following type right it
has it's a tuple of double pool or maybe
something much more complicated
this sounds at the beginning kind of bit
you know why are you in beneath yet why
would you need that but the more complex
your scenarios are the more useful these
properties and these this functionality
actually is
okay this is under active development
it's under the active development from
two sides from the programming
perspective of things we you know we
feel like features that we want and we
want to implement but also the theory is
continuously developed right this is
something I will come back to
um at the end if I have time
okay we are using it for a couple of
things
um staking protocols an example a simple
example you will see today token design
and there are also applications outside
of crypto
good
the first thing we want to focus on how
does the engine actually work in the
sense of how do we represent games how
does this work
all right so on the left you can see
again the the game with the inputs and
outputs on the right hand right hand
side you basically see the syntactic
expression
um
which is basically this square bracket
open game and then what follows until
the the last square bracket that
internally is basically the DSL and
telling here is a game coming with a
certain shape
okay um there is what is called
internals of G between the dashed lines
I will say something about this in a
minute first what you should see is
there are four Fields inputs feedback
output returns and they exactly
correspond to the wires so you can see
this as basically a way of expressing a
two-dimensional element kind of language
into on the the language or the the
programming syntax in within Haskell
so the inputs are just the outside
system another way to think about this
box essentially is each open game is
almost like an interface right you have
something internally happen but to the
outside world is somehow it is um
connected or maybe not connected through
its interface that it offers
what happens internally internally is
where the place of credit information is
generated so insights of these dashed
lines there are what we call line blocks
these are five lines basically there
could be many of them
um they roughly correspond again or
mirror the outside wires so inputs
feedback output returns and then there
is an additional field which is the
operation field that is essentially
where information is created
now the first thing to observe is in a
simplest game if I'm just talking about
one single player making a decision the
input X could be exactly linked to the
outside wire X that I showed you before
and it's the wire going out or actually
coming in similarly the output y
um
is will be the result of the information
that is created and will be directly
pushed outside of the box
however this is not this is not
necessarily the case in the sense of
there could be more line blocks there
could be more complicated things and
some of these inputs and output fields
and so on could be just totally consumed
inside of that game without any exposure
to the outside world
okay the operation can be two things
like here this is the dependent decision
just means this is a decision operation
so one player makes a decision
or alternatively a computation these two
building blocks either you don't need
more if you have that you can basically
build the most complicated model you
want
okay here's the prisoner dilemma
um again the diagram from before
first you can see
um if you look at the left hand side the
outside Fields the outside interfaces
here are empty
this tells you two things first you
don't always need to supply information
sometimes the games don't have are not
connected to the outside world or only
partly connected
and internally what you can see is
um
there are three line blocks the first
one the second one and the first and the
second basically are player one and
player two
again for both of them they don't
observe anything from the past there is
no input
the output something which is the
decision player one and decision Player
Two And they also need something from
the environment back this is the payoff
player one payoff player 2 which are
only defined at the third line block
which is the payoffs PD this is the
utility function and here coming back to
connecting to your question before the
form this function is expecting
basically an input from above which
tells you this is a sequential
um a sequential composition right keep
in mind the diagrammatic language is
two-dimensional
hassle is not
okay
now the last element the pair of SPD is
also outputting the payoffs and these
payouts are then connected back to the
the players and you can see already
um you know certain elements of has to
also help because the order of where
these things are actually don't matter
and it helps in the evaluation later
yeah
okay
questions so far is the center roughly
clear at least
area
so so yeah you have a question I want to
ask about oh thank you I wanted to ask
about the inputs and feedback before and
after the uh internal
definitions like like are those the
inputs going into P1 you mean outside of
sorry on this slide yeah yes so the
first inputs and feedback the ones that
have a blank
um this okay I should have feel precise
thanks for the pointer so um what is
actually the inputs would correspond to
an ingoing wire into the overall game
um I could think about the overall game
as a box itself right so this this is
just one box with possible in-going
in-going and outgoing wires what it
essentially represents is an empty not
an empty box but a box which is not
connected at all to the outside world
right okay I'm cutting just away four of
these wires
and
um
why is this relevant actually if you
think about a prisoner dilemma a
One-Shot game it has no past and it has
also no future right it's one shot by
definition there is no need to send
information back or send information
into the future and topologically I can
kind of represent these features in a
sense that there are wires or they are
not wires it's also useful in the sense
that you know if you model more complex
games you can see that only when there
is a connection through a wire there is
actually an effect happening so
sometimes these diagrams can be
extremely helpful in kind of
understanding what actually dependencies
for sure thank you okay other questions
okay
so in the last part I want to look at a
staking model
this is you know a simple model still in
the sense that I can most mostly explain
all the components that are needed in
the in the scope of the workshop
the motivation comes actually
have said that part of the engine
um we're kind of funded by the ethereum
foundation and we were working with the
robust incentive group that was one of
the examples they prompted us to work on
um and that's basically what we did so
this is this is a simplified version of
that of that work
I will focus on compositionality we can
guess it already
um specifically now I want what I want
to show is how I'm basically not
composing things but I first will
actually decompose stuff I will look at
the overall problem and I will put it in
as small parts and bits as possible
I want to also illustrate
um what we sometimes refer to as a
zooming in operation
I said before all of the components are
making game theoretic sense which means
if I'm modeling something complicated
I can when I want to obviously look at
the overall complex thing and you know
analyze this but sometimes I might not
care about the overall thing but I might
just care
let's say the the validator is a
mistaken protocol what are they actually
doing for a specific input what I can do
then is if I have the model as a
specific component I can just zoom in
look at this specific thing analyze this
specific thing without regard of the
rest
it's a bit like unit testing of specific
units if you like which can be extremely
useful
given time there are obviously more
details that I can I cannot explain all
the details behind it but this is
explicitly based on a blog post that we
wrote which gives much more context also
on the relation to you know where the
idea for the model comes from and also
all of the components are explained in
detail
okay so what's the basic setup here
we have essentially
um
several periods possibly in each period
there is one proposal and there are two
validators
um what are they doing the proposal
basically observes a chain
I will say in a minute or give you a
picture of how this actually looks like
and the proposal basically observes
their chain and then decides
um yeah I want to extend the chain at
the chain and basically says okay there
are several blocks on which block am I
actually building again it's simplified
and what are the validators doing the
validators basically observe the Delta
between what was the chain before and
what was
um basically the result after the
proposal moved and then they can make it
they have to make a decision on a voting
decision on what do they think is the
legitimate head of that chain and
legitimate obviously in the sense if
they are trying to be honest and are not
malicious
okay so this would be one example of how
this looks like what is the underlying
data type
um it has we'll be using Haskell
obviously in Haskell this will be what
is called an algebraic graph it's just a
simple graph here
um each block has two information namely
an ID and then votes in that specific
example here this would be kind of the
ideal world we started with I'm block
one built on on that block two and so on
have a linear chain the votes are in
everything looks fine okay now if you
take that as a specific input for one
period let's say this system you know
now is period four coming what will be
the action of The Proposal The Proposal
will basically um say yeah I want to
build on that chain I'm choosing in that
case I'm choosing
um ID3 which is the legitimate hat
according to the protocol that we are
interested in at that moment he makes
the decision that block gets appended
but there are no no votes yet and then
the validators come in they observe the
ID which was proposed and then they can
cast their vote and in this case here
they will do everything is very nice
yeah this is the this is a really nice
World here
okay
um however sometimes things are not so
easy
um specifically if uh if you know
everything would be deterministic then
obviously all the problems will go away
but you have networks issue in reality
which means the staking Protocols are
hard you have to think about certain
problems one of the problems could be
that um what if there is time lag
between the proposal and the tester and
what happens if this is an example here
there was a proposal in period four and
he's actually malicious he's just
letting time pass by
at some point proposal from The Next
Period
observes the chain thinks okay the other
guy hasn't done anything I'm building on
the chain and legitimately you know he's
honest Builds on ID3 and that moment
before the validators come in I said the
first the four proposal from period four
actually sneaks in and places in all his
own his own
um
block on that check so it's
basically and now the question is what
happens this is one of the motivating
examples
okay do you have questions to the basic
setup more details to follow
okay
um if not let me jump to
um
that's not really looking nice
okay can you read this should I increase
the fund is it
okay
um left hand side is basically the model
right hand side will be just an
interactive session that I will be using
um
let me start with something first
um
in order to implement the model
you need a lot of background information
right I need to actually think about
what's the data type of the chain
if there is a new block being proposed
how do I actually edit
um this for instance this function here
at the chain
um it's just observing a chain it's
observing an ID which was proposed and
it's you know creating a new chain so I
lead them I need a lot of background
stuff in order to make this model work
which is just basically you know Haskell
in that sense Haskell functions and
computations another one would be for
instance determine head I'm clearly in
order for the protocol to work which has
a certain goal
um I need to be able to at each point
say what are the hat or the heads if
they are non-determinate and this is
basically the second function what it's
doing and there's a lot of other stuff
that I'm not showing you
um that comes in so you need for that in
order to kind of use this you need first
this um the structure in order to
basically I'll say that this is the
computational background to which I'm
working
now you might wonder okay for you know
it wouldn't it be nice if this would be
coming from the outside world and indeed
for some problems you just need to
create it but in other cases and this is
something we'll be working with in the
future or towards is can part of that
basic infrastructure that we are
interfacing with in the end and that is
actually not that interesting from your
modeling perspective it's just something
you want to take as given can you
somehow import it from the outside world
or can you connect this tooling to the
outside world
okay for this purpose here I'm just
recreating it
um what it actually does is not so
important just think about it for now
what the behavior is
um of air chain and so on and so some
functionality I will explain on the Fly
good these are all functions the first
thing we want to do we want to create
basic building blocks that we'll be
relying on yeah I said before we'll be
making it here really really kind of I'm
fine-grained in a sense we start at the
real bottom of
let's make add to chain actually an open
gate put it into a computational
framework so that we have a building
block that we can move around if we want
to similarly let's do that for
determined head maybe we needed a
different points
um and then we kind of have this billing
clock available as an open day also note
essentially for the whole system here
the protocol logic is exclusively in
determined head this is this function
that you can see here if you change that
all the rest stays intact and that's
another way of if you make it you know
if you try to approach the problem in
that way you will save a lot of redoing
um if you want to make changes to the
protocol
okay
um
let me jump here
foreign
okay so I showed you the the function
before
um
let me actually
put it next to each other so
add to Adblock basically is
doing nothing else it's just a
computation
um it observes the chain old and
observes an ID and then it you know puts
that into the inputs field inside
and it's basically this is the forward
function keyword remember we had the
decision and basically computation this
is one instance of the computation and
then it does just the add chain to
weight which is
uh similar to what we have on the
attitude chain
by the way I can explain in a minute
yeah but it's the same in principle it's
the same idea you just take a component
plug it in and lift it into an open gate
it's just a computation similarly
determine head of the chain um here as
you can see this input here
um is basically just a function from the
right hand side I'm lifting it into an
open game just a building block
good these are very boring building
blocks so let's move on
what do I need I have proposer and I
have validators so what makes probably
sense is to think about how does the
validator actually look like
okay let's model the validator
um if you think about what a validator
is doing I said before the action he
does is he observes the new chain he
observes the Delta which means he also
has an access to the oil chain
that's the input here
um that's also the input the line
element here and then there is a
decision and what you can see here in
that expression is just basically that's
telling internally the dependent
decision operator what is the action
space the where Cutters they actually
can choose from
um here this is basically just because
we start the IDS of the of the blocks
from one until the vertex count
basically how many vertex are there and
then this is basically the choice that
the validator can do
okay so we have basically a bit of
computational background adds adds a
block we have the determined head of
chain we have the validator
um
now we have the proposer
okay what is the proposal doing well the
proposal observes the chain
also internally he makes a decision
um
what decision does it do well you can
choose basically on which block to build
that is the outset this is the decision
proposer which is coming out here
and then you can see this is the first
game in that in that context where we
have another line block there's some
kind of additional functionality this is
just basically producing the new chain
this is taking two graphs this is as I
said this is a specific library from
Haskell which is algebraic you can just
plug things together and you get the new
the new chain
and the output so the wiring of that
game is basically chain old and chain
new this is my interface of what the
proposer is doing
okay now the thing
um I cheated you a bit
um on two places maybe already spotted
it
if you look at for the validator as well
as the proposer if you look at the
return type here a return field I'm
returning a constant zero which is kind
of weird right because I said before
isn't that where actually the Strategic
context come from the environment
telling me what to do blah blah blah
blah and now it's just saying it's zero
it doesn't look really strategic now
this is an instance and I will come back
to this this is an instance of where we
actually had exactly what I just blah
blah namely we had the inputs coming
from the outside world and blocked them
through but then realized that there is
actually a very neat useful pattern here
that we can abstract out and make it
much easier to compose later on the
payoffs in a different way yeah this is
in some sense a bit of Haskell
background that made it possible to kind
of split this up even further that is
what I meant initially when I said when
you start modeling in this chain you can
of course sometimes realize just
programming patterns drastically
abstract them out and replace them with
something else
why is this actually happening in a
sense keep in mind for the protocol to
work
in Period T the decisions of proposal as
well as validators are not rewarded they
are only rewarded in the future that
means their reward actually is
conditioning on what is coming from the
future
and this is a way and I will show you in
a minute how we actually can deal with
this
and the same is true for the validator
as well as the proposal
okay so here's an example
um of what you can see here but
basically how this is done this is what
is called up
update payoff validator
this is an auxiliary thing it's taking
in a boom
the bull is basically was the validation
correct according to the protocol
that is then determining the payoff
um payoff can also be negative so if the
pro and basically the protocol
determines what this validator did
actually in t in t plus one doesn't
actually look good so we will punish it
could be a negative value
okay that value is feed forward and then
there's this add payoffs construction
this is just another open game and what
internally is happening internally this
is associating the payoff to the player
which is parameterized spending so you
can you can put this component in
different places and it will
automatically add the payoff at that
point to your player do you have to do
it in that form no I said before you
could also kind of make it more with the
wires and so on but this is a pattern
which makes it extremely lightweight of
recomposing the pairs and again this is
useful for the following reason
if you think about and for here I'm
assuming the payoffs are evaluated just
in one period advanced
a proposal do something the validators
do something and then in the next period
it gets evaluated what they actually do
of course I could have a protocol which
actually takes more more episodes what
do I do then I can of course kind of
take the wires put them through which is
still okay but I can also just use it
and say well the information Flows In
Direction and I can compose this value
at payoffs with the same name with the
same identifier again at that point and
I'm done it's not something we planned
for but it's just something which
emerged out of working on this and there
are other examples like this
okay these are the components that we
need
um now we want to take the next step
first I'll be awesome
we have not only one validator
but we have several
what we do here we are grouping them
together right so we say well there's a
chain U chain old input and then there
is some kind of information this is just
information about past behavior from the
other validators from the period before
and then the thing is what this should
observe is the following here and here
validator this is the construct which is
on the right hand side so we take that
and block in the open game here and this
is basically the second step of nesting
we already have one for the proposal but
for the validator basically we bottle it
as an open game and then we plug it into
the group and now you can also see
um the the structure basically of that
component validator's group decision is
made that you can also extend the number
of players if you want you just
basically add one line here add
functionality but the overall
interfacing of that group of decision
making process is the same whether it's
100 or just two and there are also ways
I should say this you don't always have
to make this explicit if they are
symmetric in some sense there's also
convenience patterns such as you can say
here 10 players of the same type put
them there
good so this is the validated group
decision
we also need to make the payment for the
validators again it's not only one
validated but two and again you could
think about this as being extended to
more players
the thing to keep in mind
um is again is
um and I repeat myself but it's
important this validation step is in
time t for the behavior of T minus one
yes you have a question
okay
maybe you ask a question again and
everyone yeah he was asking uh I'd like
to know what's operation the operation
field basically the operation field okay
the operation field is from one
perspective basically what the where the
the um strategic information is created
if it's a function it will be just
saying
um let me give you the example
here
I'm filling the operation with basically
two keywords namely either
um forward function
or depend decision yeah what is the
forward function doing it's just lifting
a normal function a normal Haskell
function into an open gain which means
in the simplest case it's just a
deterministic function that determined
head
takes a chain and outputs ahead and then
I'm interfacing it with the outside
world
if you're talking about a decision it's
different look at the validator this is
the keyword dependent decision the
validator in this case the decision is
the following
the player observes this chain U chain
old that this observation is information
and then he makes a move he has to pick
an element and this element in that case
is an index to which of the block
elements do I believe to be the head or
I'm choosing to be the head yeah okay
then there'll be an operation between
returns and feedback
sorry second like so so this is doing
the like from left to right yeah
movement correct and what about the
other direction okay that's a good point
so first let's take one step back um if
you think about the prisoner dilemma
there was also the case where the agents
did not send information back into the
past yeah okay so that explains and the
reasoning is simply here I don't need to
send the information from these players
back into the past and the reason I
don't need to do that is
um there's basically the protocol is
moving forward and I don't need to send
this information back it's like I'm
creating a state and the state will
summarize what is going on why I'm doing
this in this form is the following the
following reason I will end up with one
episode
that episode will be basically a basic
game for Markov game and then I can
stack these again on it on each other
and repeat them if I want to
now you are right if you wanted let's
say you you're just explicitly wanted to
model two episodes you could say
um
parts of these elements for instance
what these guys expect here what the
return is is actually coming from this
returns field over here and I said
before you can do that the reason I'm
not doing it is here is exactly for if I
want to Stack more more episodes with
payoff still being created for players
in let's say T minus four I can easier
do that
okay
maybe it will become clearer when we
come to the rest if not you know feel
free to ask again
other questions
could you tell me the time
yeah
25 okay good
okay well it is payments um again this
looks like a bit more you know
convenient stuff but this is a I mean
the question we should ask if you model
it yourself is how can you how can you
model it in a way that it's actually
really a building block
um I said before one way of doing it is
that the interfaces are relatively
flexible so I'm just leading the fee
which is an outside outside parameter
um and then internally basically I just
need the payoffs I need to chain new and
the hat ID which was chosen and with
that basically I have the full picture
and that the protocol can evaluate once
the behavior actually correct
okay
and you can see this is actually
happening in a function that I didn't
show you this is a tested correct they
tested correct is basically just telling
according to the logic of the of on the
protocol the information I got yes made
sense or no and it's outputting a pool
it's just saying yes or no and it's
doing that for player one and it's doing
it for player two and these then
corrected a tests that are basically
input into this function pay or
validator here on the right which you
can also see here it's just taking was
the validator correct or not and then
it's basically updating
good
okay also what you should see and this
is kind of coming back to this
discussion on why is there no
information being sent back this is also
um there's also no information sent in
the future right if I would be doing
this again without my way of composing
this one player which just magically
updates I would have to explicitly
feedback that information
uh so here you have uh potentially
Boolean values that are that that
um the outputs which is the correct
attested one and two uh but then in a
different block you had an input and
output that was actually called boo so
I'm a little confused whether uh that's
this is supposed to be like a label or a
type
um okay this is basically the question
of the scope of the of the um of the
environment basically so the reason I
call this rule here is I'm just telling
now basically me for the reader I know
this is a pool and I basically know what
is happening why am I doing this here
differently I'm doing the correct to
test it because I'm giving it
information that I can easier pass it
right if I would be just saying Bull in
that specific context I might know what
it is but I don't know where the bull is
coming from right so it's it's like you
might disagree with my um basically with
my nominator or with the way I I label
things but for me internally it was just
like I understand what it actually means
and that's the reason basically yeah the
thing to keep in mind in a categorical
framework because you have these wires
going in basically bound variables come
in
um the outgoing wires are basically
binding new variables to the output
right so in case of the correct the test
that I'm binding a value that is the
outcome of that operation to that
specific
um character test which means if I'm
reusing it it's mounted
okay other questions
all right let's continue so we have to
validate us
payment
and now we have everything assembled for
a one period game one episode game
okay this is this Beast here just barely
makes it on
not completely
what it basically tells you is this is
one episode I'm now pulling everything
together there are certain
parametrizations ignore them for now
they're just details um of you know how
do I call the players what is the reward
and what is the fee and so on
you should really think about it again
as an as a diagram with in-going and
outgoing wires so the in-going wires are
basically chain old head of chain from
the period -2
um validators map this is just basically
summarizing the information of what the
validators have done before
and in principle you should think about
this I keep enough information so that
the protocol Works in a simple case here
just one episode if there would be more
episodes this would be it's just a
record type basically it would contain
more records
okay
um what we then have basically is the
proposal moves first he observes the
chain
he outputs a new chain keep in mind
this is this again
so he's observing the chain and then
internally is also at the same time
creating the new chain this is a
computation taking place here
okay proposal Moves new chain is created
then the validators move as a group
they observe the new chain they observed
the old chain there's also access to the
old information
validator smash validators hashmap old
and then they make a decision they
create new this is basically new map
containing the updated information how
did all of these validators actually
behave
and they also have the chain updated
because when they cast their votes
remember the shape of the of
um the blocks are basically an ID and a
voting value
all right the thing to remember and I'm
repeating myself I know but it's
important to understand what is
happening that the payments basically
that happen are happening not for the
decisions to that are made by the
players in that episode but from the
episode before or if I would be looking
at them more longer Horizon from the
episodes before
good after this this is the main things
the decisions are made by the proposal
by the validators now I'm basically
during bookkeeping
um I'm determining the head of the chain
I do the validators payment this is from
the past
I also check I didn't explain this but
this is basically also bookkeeping I'll
just look at what was the old proposal
actually doing did he actually do
something
and then I'm getting that as an input to
the proposal payment again for the
period before
now
the complicating thing here is that I'm
targeting a model which itself has a
structure that if you just look at the
output chain new updated head of chain
and so on validators hashmap and you
look above
you can see there's a pattern basically
the input types here chain old head of I
mean you can't see that but I'm telling
you
the input type Jane old head of chain
and that here are exactly the output
types
which means I now I can take the one
episode and just say okay maybe I want
to run it for three episodes I'm taking
the same element and I'm just connecting
them
or I'm not doing that here if I want to
run this as a Markov game and you know I
want to approximate it like I'm running
this for a long time I could just
basically use a specific operator we
developed that you can embed the stage
game and then I'm repeating it yeah so
you're starting you're initializing the
game you create a one-stage output that
is fed back into the next period And so
you go on
thank you
okay I'm not doing that here
um I want to jump
for the
last part basically a bit and looking
into how do you actually analyze these
games
I mentioned before on the slide what I
want to do is I want to
um illustrate a bit of what is the
zooming actually what is the zooming how
does the zooming work and you can
already see because I'm focusing on the
one episode I'm actually ignoring any
kind of repetition clearly if you care
about the overall protocol at some point
you have to think about the Dynamics and
also longer time period periods but for
some questions it might be relevant to
see
um is it actually working locally
to give you an example suppose you're
interested in honest Behavior by
proposal as well as validator
and I'm giving you you know I'm
initially initializing this with
specific inputs and I'm testing in that
one period do the players actually have
an incentive to work in that way
and if not if you find out basically
just by zooming in on that context it's
not well the info can you just can put
everything else aside you don't have to
think about the Dynamics that's enough
similarly if you care about let's say
vectors of attacks very often it's
enough to focus on specific Parts in
order to evaluate whether the attack is
actually working or not
question no yes
maybe
okay I said um in the context of like uh
you know modeling like the domain of
like a game and you know like a software
team working with like a program like
this you know if they have to Liaison
with like the product team which will
have an understanding of like the ux
wouldn't it be easier for them if they
want to model attack vectors to just
model what the agents could do and then
use a genetic algorithm for example
might well be depends on the context
right um the key thing is here you can
have you have both basically The Best of
Both Worlds you can just look at the one
component but if that is not the only
query you want to do but you also want
to look at the more complicated stuff
you have it as well right so nothing I
mean in principle what you could do is
actually you can take this component
interface it to the outside world runs a
learning algorithm on top and that's it
and it would be exactly the same thing
but it will be part of the overall
consistent framework and that's an
important thing if you care about the
design for instance you want to make
sure that everything is somehow
consistent obviously right and then it's
much easier to say I'm taking an element
which is consistent with the rest and
just interface it to the outside world
and then simulate it
clearly I mean you know this is also
ethical I'm not sure how many people
will be using it in that form right
that's another question that is I think
lurking in the yeah in the back so there
are I mean this is at the moment
actually to work with that you don't
need that much high school because you
need to understand the syntax of the
engine and most of what I showed you is
inside clearly you need some kind of
knowledge of Haskell to work with the
outside world but if that also goes away
it's easy to think of this as basically
working as you have a domain specific
language and that's all you need to know
and you have some operators on top then
parts of the pain hopefully go away
okay other questions
all right if not
slide one shall we start again
maybe maybe afterwards
okay
um
let's jump a bit into the um analysis
um
okay here's a bit more Haskell pain for
you
um and even more than average
namely I'm using something which is
um kind of what is called arrows
uh if you don't even know what it is for
now you just think about this as I'm
defining a strategy for proposal as well
as for the validator what is this
basically doing is the following is
creating a function and the function
tells me I'm observing a chain and what
you want me to do is I'm basically
sending an ID
remember the proposal observes the chain
and decides on which which element to
build what the rest is basically saying
is this is an honest strategy it does
the following determine head this is a
functionality from before
so I'm looking into the chain I'm
looking at what is the what is the what
is the head of the chain according to
the protocol if it is play that game
play that strategy if not if there are
multiple candidates randomize this is
happening here basically
and this is done uniformly and the
validator does exactly the same it's
basically a super honest as well he's
just looking at
um what's the head if the hat is a
single value play that if multiple
values randomized among them
good and then basically we kind of
encapsulate everything in this so
reminder this is basically
um
uh referring to the one episode game I'm
plugging in some variables or some
parameters which you can ignore for now
and then what is the thing that I'm
doing
let me actually open it differently
um so I'm analyzing
the scenario and then this is I should
have said this this is the interactive
way this is the right hand side is an
interactive session with the high school
compiler I'm querying that thing and
what I'm getting out basically is
simplistic information namely
um the output just tells me everything
is fine
um you don't have to worry go home or go
to the pub everything is working
now this is a specific thing what it
actually tells you and in fact this is
the protocol is inspired by you know by
one of the biggest
um by ethereum basically you can see
that the specific assumption is working
no incent no agent has an incentive to
deviate okay nice and nice and clean so
far but now we want to do the following
now we want to come back to this picture
here
I said before that let's suppose in the
past period there's a guy who's actually
not so nice and he's deciding not to
propose he's waiting at that moment at
some point after some time threshold the
next proposal which is
um the lower one here basically observes
the chain steps in he wants to be nice
he's honest proposes a new a new head
um and at that moment before the testers
can actually be active the old proposal
steps in and just basically proposes his
own his own head of the chain
okay there are various ways of doing
this I could just model explicitly the
attack game and it is actually Merit to
do that but here's an alternative way
you can do it and this is I'm referring
to the zooming in that I want to
illustrate
foreign
I've created another version here which
is doing this one episode attack which
is doing a simple trick namely I'm
introducing an additional variable
because I'm just focused on this one
period I can do that it's easy I just
add which is a chain manipulated
um all the rest is the same
the proposer observes the old change so
he's basically still operating under the
information from the past
and then what happens is this line block
is added
I'm merging the two proposed heads into
one chain so then I have really a fork
and then what is happening the
validators are observing the forked
version so they have to deal with the
problem basically right
now is this the only way to do it no you
have multiple ways of doing it but this
is you know this is part of the what the
model has to decide how can this be done
in an easy and accessible way another
way to another way to do this and on one
branch we actually do this is explicitly
keeping time of the um keeping track of
time and basically look at the timing
game right so that time passes and then
the proposal from the first period can
until a certain point act the problem is
that until a certain threshold the all
the other players don't know whether the
other guy moved or just they haven't
received a signal yet but this is much
more involved here I'm just cutting into
this thing and I'm just focusing on that
one aspect that I care about namely what
do the validators actually do
foreign
okay let's jump to this
um
attack
okay um strategy proposal is the same
then we have what I call the strategy
validator random it's also the same from
before I add two new strategies for
validators one is strategy validator
four and validator five this is
something very
um very simple namely in case of a tie
when there are multiple things I'm just
taking here by hand I'm just taking the
fourth element
and you know for that specific example
I'm just specializing it for that
specific thing because it's enough but
you could also easily extend it to a
more General version
in other words when there are multiple
candidates I'm just deterministically
choosing one of the elements right and
I'm doing the same for five but just on
the other on the other element
okay now I have several scenarios
um I have scenario four and five which
is just the same proposal strategy as
before honest
in the manipulator chain and then the
validators are just deterministically
both um voting for id4 in case of a type
or alternatively five
and lastly the random is basically I'm
just taking the element so the honest
behavior from before namely if there is
a tie I'm just randomizing
which obviously is also debatable
whether this is a good idea but for
illustration purposes
that's enough okay let me run through
four you can see this is nice this is
also not nice this isn't this is an
equilibrium and five as well okay so far
this looks like pretty useless because
everything is in equilibrium but in fact
what it tells you is that
suddenly we have two equilibrium at the
same time and both are kind of either we
go with the honors proposal and the one
who proposed the four or we actually go
with the five which tells you
um this is not in the interest of the
protocol this one of them should not be
in equilibrium
and you'll see even more if I'm sticking
to the actual Behavior of introducing
the possibility of random basically just
honestly saying I don't know when I'm
randomizing
you can you get different information
um and this is the alternative namely
the system recognizes one of the agents
has a deviation
the formatting is horrible but
um for basically focus on the first part
the player with the name a21 has a
deviating property it's optimal payoff
is two current payoff is one what's the
optimal action you just he should choose
is move one why is this the case you can
easily imagine because basically these
players tried to coordinate and if they
are diverging the protocol will punish
them so they actually are better off
voting for both coordinating on the
wrong or the manipulated head of the
chain instead of sticking to their honor
strategy so at that moment you see
Things Fall Apart
because that's very very relatively
simple model and again this kind of it's
a simple illustration here but that kind
of structure was actually motivation
from a unrealistic attack
good let me close with one more thing
and this is then more or less the end
with kind of some remarks
this is the interactive version I said
before you can also think about this as
being part of a system so you can
um
um basically also run the testing in
parallel
or as an alternative so if you do this
basically what will happen is you have
some kind of specification test this
includes the equilibrium but it can also
be the parts you know is the staking
protocol working in the right way
um and then hesper is actually quite
nice in that end because it can create a
lot of very well structured arbitrary
examples that you care about and then
you will see at the end hopefully
something green like this which
generated in that case I think 100
different starting points for the chain
evaluated them and you get some result
yeah and can you can see this is
basically you can you can extend this in
all kinds of versions it can be either
on the behavioral level really thinking
about equilibrium that would be the
first test or if you go down really just
the components
okay questions before I conclude
let me conclude
um on two levels first a bit more
concretely what is the end of the next
steps for this engine
and then circling back to where we
actually started so this is connected
the rest of category Theory or maybe
more precisely black category Theory
so one of the things and some of
actually formal verification people are
here we are one project that we have is
I mentioned this we want to have more
pipeline from let's say starting from
evm code into actual open games
representation a lot of work has already
been done that we can dock on and one
project is basically to kind of extend
this towards the open games framework so
that if you can start with some um smart
contracts you basically get an open
games representation and then you can
start querying them
um either automatically or with your
manual maybe you have some ideas of what
you want to query in a manual in a
manual way or you have some more bigger
and analyst tools on top
thank you
uh you know the analytics we have so far
we're extending them permanently we're
also you know going into different
applications and thinking about how they
you know what specific analytics are
relevant there
um it's outside of staking
and
I should mention this before which is an
actually important thing the engine
itself the end the version that you see
here is basically built on Theory
version
outdated time -3 or so there have been
three more iterations and one of the
tasks in the next weeks a month will be
basically an update of the engine the
theory itself is also continuously
developed
okay lastly compositionality that was
the starting point you've seen one
instance of why compositionality might
be useful in the context of open games
what is interesting about this specific
example is that when we started
um
out there is this basic question that
probably raised in the initial slide
mean or in the initial beginning of his
presentation then how the systems
compose in the game theory are in the
game City setting we have a relatively
clear answer and what was interesting
was in the beginning the implementation
and the way we did it categorically is
not at all doesn't resemble at all the
way it looks right now because at the
beginning we had a very different way
what we realized actually is the
connection to lenses in a categorical
framework what we also realized
um was actually realizing that the the
existing deterministic lenses are not
enough and this is quite obvious because
games need Randomness right you need to
deal with
um non-deterministic moves
that actually LED also to Innovations on
the on the side of the um Optics
implementation and that itself profits
alluded to that is itself now kind of a
you know in an area which is almost
exploding in all kinds of directions and
making connections and extending this
framework this is one of the things
which is quite nice actually about all
of this work that it's tightly it's
tying back into other fields within the
categorical framework and examples of
that are control theory reinforcement
learning active inference others to be
developed and the abstraction here
really enables you to see that these
patterns are or that these different
instances are actually related to Common
patterns and lastly what is more you can
also make cross cross combinations one
of the interesting ones is actually
thinking about games and learning right
which is not new itself but if you see
it in that form and you have this new
pattern it's quite info I find it quite
insightful and quite useful actually to
see it in that form
good
thank you very much
[Applause]
questions
yeah
or to me or to repeat soon
maybe you wanna
so I'm wondering if we can talk about
like uh real world attack example and
how that would
um come into such a system and in
particular I guess on my mind is the
mango attack from a couple days ago
where it was essentially an oracle
exploit and the
um it seems to me like an orca would be
inherently outside of a system that
you're modeling this way or is that is
that an incorrect assumption
um
sorry let me go back go back here just
if you think about no here if you think
about this
um
X doesn't have to come from the in from
the world it's from the game itself
right it can be something from the
outside perspective so I can interface
this that system with something which is
drawn from an outset could be from a
database or whatever it actually is
where it's coming from depending on how
I deployed this it could be continuously
updated and I'm running that basically
on a permanent basis so this is this is
clearly possible
um
you can also parameterize games
um I'm not sure you maybe remember this
part I just
go there
um if you look something like this one
episode editor attack there are a couple
of parameters which are actually
exogenous they are not part of the
internal structure I can make them
endogenous querying them but I can also
just say they're coming from the outside
and I'm fixing them like the names of
the players of feedbacks or sorry fees
and Rewards
uh can you establish bounds on those
parameters
um it depends on what you mean with
bounce first of all keep in mind that I
mean they're structured it because they
have to be typed right so if they have
the wrong time they will not will not
work
um then I mean what exactly do you mean
by by bounds in the sense of values or
so yeah I don't mean like a type bound I
mean uh value bounce
um well again I mean you have
limitations in a sense if you're working
with an escrow world you clearly have
boundaries for certain types that you
can use
um there are also of course the question
of the computational complexity at some
point right
um I haven't talked about this because
this is also part of active research
um so far I'm using compositionality
exclusively on the level of composing
the representation
there are results that show that you
know Computing equilibrium is very hard
um and we will not break these results
but in the practice of actually
Computing concrete concrete games
um you might be able to leverage also
the compositionality right because
some components here might be computed
but it might be independent of that and
then you can compute or
um some compute some component here
might compute but it will only affect
another component
another thing to keep in mind is that as
Philip said
um you can have that a game can you know
just have a function as internals or it
can have you know strategies
so in the case of an oracle you can
either treat it as a parameter that
basically comes from the outside world
or you can model it as a stupid function
that has no agency whatsoever or you can
model it as I don't know a protocol that
has its own set of economic incentives
to work in the right way I guess that
would be the case of like the
centralized oracles where you know
people are incentivated to not to lie
and whatever the cool thing about this
is that then you can start from a
scenario where the Oracle is honest the
the very cool thing that practice
teaches us is that usually when people
design a protocol they have already an
intuitive notion of what is the
equilibrium where everyone is honest so
you say okay you test that you have an
equilibrium and now you can basically
start bribing the Oracle so you can
start basically you know adding
incentives to the Oracle to lie
and one thing that you can do very
efficiently computationally is finding a
bound that is basically the cost of
breaking your equilibrium so say how
much do I have to bribe the Oracle to
break the equilibrium and then this is
super useful because now you can find
parameters
and and you know since you are starting
from equilibrium that you already knew
you don't have to do equilibrium search
it's just equilibrium checking you just
like linearly increment this parameter
and it's okay this is how much we are
protected and and then yeah that that
would be a sort of bound between your
model how expensive would be to it
up basically
oh hi um I have a few questions because
I've been really listening so intently
and I've written some things down so
it's okay
um the first one was um you know could
you perhaps optimize the compiler by
modeling like modeling it with category
Theory and with your tools
oh sorry was that kind of hard to
understand
um
could you perhaps Model A compiler and
optimize a compiler using your tools and
with category Theory
okay um they're actually doing people
doing this here uh I think at least at
least trying but honestly this is
definitely the outset of my expertise I
can't say that
you rechecked the research of uh these
professors called dangika that is using
category Theory to do compiler
optimization uh so yeah that would be
probably the closest thing okay and
that's exactly where my knowledge of it
and it's
thanks um and then another question and
I'm going to speed run it so nobody gets
offended that we're taking a long time
um could you model uh perhaps an
iterated prisoners dilemma with a
variable number of agents and rounds
yeah beautiful
very cool and um will you ever release
uh like a function annotated sort of
preprocessor language that's maybe
syntax agnostic or something that you
could add into other code bases that
aren't quite High School based in the
future
maybe very cool okay
thanks for coming