1
00:00:00,000 --> 00:00:22,300
*ChaosWest TV intro music*
2
00:00:25,628 --> 00:00:30,031
Herald: Good afternoon, everybody, and
welcome back to Chaos TV West.
3
00:00:31,267 --> 00:00:36,614
We are going to see a prerecorded
talk by Michael Sperber
4
00:00:36,614 --> 00:00:39,620
about mathematics for hackers.
5
00:00:39,620 --> 00:00:45,313
Michael is… once was a mathematics
student, but never finished his degree
6
00:00:45,313 --> 00:00:48,256
and is in the process of
revisiting this old love of his.
7
00:00:49,615 --> 00:00:52,975
Dieser Vortrag wird auch
simultan übersetzt in Deutsch.
8
00:00:53,355 --> 00:00:55,588
And, well, enjoy.
9
00:00:55,898 --> 00:00:57,359
Michael Sperber: Welcome!
10
00:00:57,359 --> 00:01:00,322
Well, I'm here to get you all
excited about math for hackers.
11
00:01:00,322 --> 00:01:03,980
Now, you can have an entire hacker's
life without having encountered
12
00:01:03,980 --> 00:01:08,520
much of mathematics. After all, this
conference and this community to a large
13
00:01:08,520 --> 00:01:13,142
degree really is about finding unexpected
behavior in software such as Heartbleed.
14
00:01:13,142 --> 00:01:17,797
I mean, there's zillions of examples, but
Heartbleed is an example where, you know,
15
00:01:17,797 --> 00:01:22,164
the OpenSSL API exposed secret memory
through a regular API call. That was
16
00:01:22,164 --> 00:01:27,710
certainly unexpected. Now, you might
consider this unexpected behavior to be
17
00:01:27,710 --> 00:01:31,430
just an inevitable part of software
development because it's so complex,
18
00:01:31,430 --> 00:01:35,270
right? Things that you didn't expect
happen due to all the complications and
19
00:01:35,270 --> 00:01:40,090
the complexity. On the other hand, with
critical infrastructure, such as OpenSSL,
20
00:01:40,090 --> 00:01:45,660
you really want certain aspects of that to
really run reliably, correctly. And so
21
00:01:45,660 --> 00:01:49,497
really, that unexpected behavior comes
down to a correctness issue. And,
22
00:01:49,497 --> 00:01:53,747
of course, that's where mathematics might
come in because mathematics deals in
23
00:01:53,747 --> 00:01:59,369
correctness a lot of the time in the form
of proofs. Now, you can certainly apply
24
00:01:59,369 --> 00:02:06,049
proofs to software systems to great
benefit. But of course, proofs are often
25
00:02:06,049 --> 00:02:10,678
tedious and a lot of work. They involve a
great deal of mathematical intuition.
26
00:02:10,678 --> 00:02:14,292
You might not feel like that today, and
you don't have to, because I will talk
27
00:02:14,292 --> 00:02:19,640
about something else today. I will instead
talk about mathematics as a language.
28
00:02:19,640 --> 00:02:23,005
Right. This is not a new idea,
it's hundreds of years old.
29
00:02:23,005 --> 00:02:26,397
Here's a quote from Galileo
that said, well,
30
00:02:26,397 --> 00:02:31,731
the world really can only be understood
in terms of the language of mathematics.
31
00:02:31,731 --> 00:02:35,320
And, you know, a lot of
mathematics concerns itself with finding
32
00:02:35,320 --> 00:02:39,980
formal methods for the world around us.
Now I want to emphasize the fact that
33
00:02:39,980 --> 00:02:44,666
really mathematics doesn't really model
the world around us directly. It really
34
00:02:44,666 --> 00:02:47,091
does that through the detour through our
perception, right?
35
00:02:47,091 --> 00:02:51,045
Mathematics really is
a fundamentally human construct
36
00:02:51,045 --> 00:02:55,000
that our mind uses to understand
the world around us.
37
00:02:55,000 --> 00:02:59,270
And in that way, it's also a social
construct because, well, we don't really
38
00:02:59,270 --> 00:03:03,885
need mathematics, if not for communication
between different people.
39
00:03:03,885 --> 00:03:09,584
And that's really where, you know, the
value of mathematics for software comes in
40
00:03:09,584 --> 00:03:14,510
because software also is an image, sort of.
Our perceptions perceptions of the world
41
00:03:14,510 --> 00:03:19,510
around us, a lot of the time. At least
useful software is. So, one particularly
42
00:03:19,510 --> 00:03:24,250
useful part of mathematics for hackers,
for software construction, is, well, first
43
00:03:24,250 --> 00:03:29,234
of all, the language of equations. And
here's a couple of equations, right?
44
00:03:29,234 --> 00:03:33,378
x plus two equals six, that's very simple,
specifies the value for x.
45
00:03:33,378 --> 00:03:37,451
This next equation, well, it has...
so x is a variable
46
00:03:37,451 --> 00:03:40,186
and the next equation has two variables,
has x and y.
47
00:03:40,186 --> 00:03:44,190
So it has two x squared plus
two y minus two equals zero.
48
00:03:44,190 --> 00:03:49,322
That's a quadratic equation. Might even
have, you know, several solutions. And
49
00:03:49,322 --> 00:03:53,887
finally, there's an equation that involves
a function whose definition is unknown.
50
00:03:53,887 --> 00:03:58,231
It just says, well,
f(5) plus f(7) equals 70.
51
00:03:58,231 --> 00:04:01,026
Now, you know,
when it comes to functions,
52
00:04:01,026 --> 00:04:04,060
well, those are things that also
exist in software. So we might
53
00:04:04,060 --> 00:04:09,440
conceivably use the language of equations
involving functions to describe functions
54
00:04:09,440 --> 00:04:13,500
in our software. So we might take that
equation to describe that piece of
55
00:04:13,500 --> 00:04:17,651
software written over on the right-hand
side. And, well, you know, we could try to
56
00:04:17,651 --> 00:04:22,250
kind of work through it. Right? You can
see there's a function, there's a variable
57
00:04:22,250 --> 00:04:27,479
that's external to that function. So it
goes across several invocations of it,
58
00:04:27,479 --> 00:04:29,860
called y. And it's initialized to 7.
59
00:04:29,860 --> 00:04:34,163
And maybe if we call f(5),
x is going to be five.
60
00:04:34,163 --> 00:04:36,740
Y'know, try to go through it in your mind.
61
00:04:36,740 --> 00:04:41,140
z is going to stash
the old value of y, which is seven,
62
00:04:41,140 --> 00:04:43,720
and then y is going to be set to x.
63
00:04:43,720 --> 00:04:48,030
So it's not going to be five. And then we
multiply x with the old value of y, so we
64
00:04:48,030 --> 00:04:53,175
multiply 5 with 7 getting 35.
So f(5) might return 35.
65
00:04:53,175 --> 00:04:59,058
And with f(7), we then after that call f(7)
y is now 5,
66
00:04:59,058 --> 00:05:03,661
we stash the old value
in z, so it's now 5
67
00:05:03,661 --> 00:05:06,359
x is 7,
and it returns 35 again.
68
00:05:06,359 --> 00:05:09,825
Only the product, the multiplication,
works in the other order.
69
00:05:09,825 --> 00:05:13,773
And the sum of that is 70, so you might
say, well, that equation describes that
70
00:05:13,773 --> 00:05:19,720
function over there. But really, we had to
go through a lot of detail and sort of
71
00:05:19,720 --> 00:05:24,160
tracing through the program to figure that
out. And also, it only works with that
72
00:05:24,160 --> 00:05:30,069
initial value of y and it only works if we
call those functions from left to right.
73
00:05:30,069 --> 00:05:34,067
But the language of equation doesn't say
anything like that, that we really need to
74
00:05:34,067 --> 00:05:38,430
respect order or something like that.
Really, f(5), in mathematics, should
75
00:05:38,430 --> 00:05:43,040
always return the same value. Otherwise,
you know, it becomes much harder to really
76
00:05:43,040 --> 00:05:47,840
consistently apply the language of
equations to programs. Therefore,
77
00:05:47,840 --> 00:05:51,870
Really, that's I guess the first hint
that mathematics gives you,
78
00:05:51,870 --> 00:05:55,750
is that you should write functions that
always return the same value given the
79
00:05:55,750 --> 00:06:02,832
same input. But, I digress.
Another aspect of the language of
80
00:06:02,832 --> 00:06:06,833
equations is a concept called
substitution, that you probably know. So
81
00:06:06,833 --> 00:06:12,740
imagine that first equation says x equals
to 7. And then there's a formula that
82
00:06:12,740 --> 00:06:16,890
has that variable occurring. And in the
context of that first equation, what we
83
00:06:16,890 --> 00:06:22,040
can do is you can kind of plug in that
equation, we can substitute every
84
00:06:22,040 --> 00:06:29,248
occurrence of x with the number 7 in
this case and then use that to figure out
85
00:06:29,248 --> 00:06:33,480
the final result of that formula. That's
also something that fundamentally only
86
00:06:33,480 --> 00:06:39,990
works, you know, if x doesn't change over
time. If your functions really return the
87
00:06:39,990 --> 00:06:44,440
same value every time you call them with
the same input. Now, the substitution
88
00:06:44,440 --> 00:06:50,228
principle is not just for equations of the
form where you say x is a certain number.
89
00:06:50,228 --> 00:06:54,350
You might also have an equation that
expresses x in terms of another variable,
90
00:06:54,350 --> 00:06:59,430
such as z in this case. And you know, that
first equation means, well, I can plug in
91
00:06:59,430 --> 00:07:06,980
2z every time x occurs in that formula and
use that to do further evaluation or
92
00:07:06,980 --> 00:07:11,550
simplification of that formula. And what's
more, it also works the other way around,
93
00:07:11,550 --> 00:07:17,299
right? I can work. I can sort of read that
equation in the second line, also from
94
00:07:17,299 --> 00:07:22,930
right to left. So order does not matter.
So that's a fundamental principle of a
95
00:07:22,930 --> 00:07:27,370
branch of mathematical algebra, right,
that we have variables and that we have
96
00:07:27,370 --> 00:07:32,510
that substitution principle and that we
have equations. So well, here's a well
97
00:07:32,510 --> 00:07:37,724
known algebraic formula, the binomial
formula, or one of them, at least.
98
00:07:39,688 --> 00:07:44,310
You might've learned that at high school.
But today I want to look at a couple of
99
00:07:44,310 --> 00:07:50,831
more slightly more fundamental equations
that might be part might have been part of
100
00:07:50,831 --> 00:07:55,879
your school algebra class. So I want to
point out that all of these equations have
101
00:07:55,879 --> 00:07:59,457
names, and you might try to think of them
right now, but I'll try to go through them.
102
00:07:59,457 --> 00:08:04,480
You might think of the names and
then I'll resolve when I'm done. So the
103
00:08:04,480 --> 00:08:08,460
first equation says when you multiply
three numbers, it doesn't matter whether
104
00:08:08,460 --> 00:08:12,120
you will first multiply the first and the
second one and then the result with the
105
00:08:12,120 --> 00:08:17,652
third one, or whether you first multiply
the second and the third one and then
106
00:08:17,652 --> 00:08:22,360
multiply with the first (I'm going from
right to left here). The second equation
107
00:08:22,360 --> 00:08:27,210
says you can swap the two arguments of a
multiplication, and the third one says
108
00:08:27,210 --> 00:08:30,950
that you can kind of multiply out a sum in
the sense that,
109
00:08:30,950 --> 00:08:35,779
when you have
a times the sum of b and c,
110
00:08:35,779 --> 00:08:41,779
you can multiply a individually,
with each of the of the sums there.
111
00:08:41,779 --> 00:08:45,560
Now here are the names:
The first one says, well, it doesn't
112
00:08:45,560 --> 00:08:52,240
matter which way we associate the
multiplication with these three numbers,
113
00:08:52,240 --> 00:08:54,319
so it's called "associativity".
114
00:08:54,319 --> 00:09:00,122
The second one? Well, it comes
from a verb that says "to swap".
115
00:09:00,122 --> 00:09:02,229
So it's called "commutativity".
116
00:09:02,229 --> 00:09:06,557
And the third one is about distributing
a multiplication over an addition.
117
00:09:06,557 --> 00:09:09,149
So it's called "distributivity".
118
00:09:09,149 --> 00:09:14,130
And so these are all very valuable
and useful equations, but
119
00:09:14,130 --> 00:09:17,015
really the most useful one is the first
one, associativity.
120
00:09:17,015 --> 00:09:21,272
And associativity is something that
works not just for plus.
121
00:09:21,272 --> 00:09:25,861
It also works for multiplication,
for example.
122
00:09:25,861 --> 00:09:30,450
So really, when you talk about
associativity, you don't talk about it in
123
00:09:30,450 --> 00:09:35,770
isolation. You have to say what operation
you mean is associative or is not
124
00:09:35,770 --> 00:09:41,050
associative; in this case, "plus" or
"times". Moreover, associativity is
125
00:09:41,050 --> 00:09:45,440
something that's not restricted to
numbers. So, for example, here are two
126
00:09:45,440 --> 00:09:51,260
Boolean equations that specify
associativity for a Boolean "or" or "and",
127
00:09:51,260 --> 00:09:55,860
so with the "or" operation you can take
three Boolean values, it doesn't matter
128
00:09:55,860 --> 00:09:59,160
which way you "or" them up,
you always get the same result.
129
00:09:59,160 --> 00:10:02,991
And the same works for
the Boolean "and" operation.
130
00:10:02,991 --> 00:10:05,389
While these are kind of primitive values,
131
00:10:05,389 --> 00:10:07,757
but you can also have
values that have structure.
132
00:10:07,757 --> 00:10:11,352
So, for example, you might
program with a list data structure.
133
00:10:11,352 --> 00:10:16,456
So you have a list with elements,
a1, a2, and so on, until aN.
134
00:10:16,456 --> 00:10:22,973
And you might take two lists, where the
second one has elements b1, b2, ..., bm
135
00:10:22,973 --> 00:10:27,611
and you concatenate them together. I
wrote this with that funny bow tie symbol
136
00:10:27,611 --> 00:10:32,917
there, concatenation. So you concatenate
these two lists, and that operation,
137
00:10:32,917 --> 00:10:38,805
that concatenates any two lists is,
if you think about it, also associative.
138
00:10:38,805 --> 00:10:43,620
Now, what value does it have
to know that an operation is associative?
139
00:10:43,620 --> 00:10:48,080
So here's a classic example where that's
valuable. One way to think about,
140
00:10:48,080 --> 00:10:53,180
associativity as well: you can move the
parentheses around, right? And if you can
141
00:10:53,180 --> 00:10:59,990
move the parentheses around, it doesn't
matter where they are. And that means that
142
00:10:59,990 --> 00:11:04,080
you can leave them out entirely if you
have sort of a chain of the same kind of
143
00:11:04,080 --> 00:11:09,670
operation. So imagine you have a large
parallel computation that's structured in
144
00:11:09,670 --> 00:11:14,680
the following way: you have individual
computations a, b, c, d and so on until z,
145
00:11:14,680 --> 00:11:18,490
and they're all independent of one
another. And to get the result of your
146
00:11:18,490 --> 00:11:23,210
overall computation, you all combine them
with that operation that's written as that
147
00:11:23,210 --> 00:11:28,250
black rhomboid. I'm just going to say
diamond from now. So the diamond
148
00:11:28,250 --> 00:11:34,690
operation. And so the combination works
with a diamond operation. But if you know
149
00:11:34,690 --> 00:11:39,010
that the diamond operation is associative,
it means you can sort of bunch up your
150
00:11:39,010 --> 00:11:45,730
"abc"s any way that you like. And so, for
example, you might say, Well, if I've got
151
00:11:45,730 --> 00:11:50,710
four machines working on this computation,
I can split my individual computations in
152
00:11:50,710 --> 00:11:56,040
four bunches. Combine, you know, diamond,
the first bunch, the second bunch, the
153
00:11:56,040 --> 00:12:00,150
third bunch and the fourth bunch, and then
combine the results of those and I get the
154
00:12:00,150 --> 00:12:05,570
same results. It doesn't really matter if
it's five bunches or six or seven, or even
155
00:12:05,570 --> 00:12:10,200
if it's irregular, right? And so that's
the freedom that associativity gives you
156
00:12:10,200 --> 00:12:16,779
in distributing your computation. And
this, what what I just told you, this is a
157
00:12:16,779 --> 00:12:21,130
classic big data abstraction for large
scale parallel computations called
158
00:12:21,130 --> 00:12:28,279
MapReduce. But I really want to talk about
something more fundamental today, which is
159
00:12:28,279 --> 00:12:32,970
how we think about the things that happen
in our software. So here is an excerpt
160
00:12:32,970 --> 00:12:37,529
from the Java API documentation and ir
draws an oval, so it has to do with
161
00:12:37,529 --> 00:12:44,481
graphics, with images. And you notice,
right the draw over operation, it has
162
00:12:44,481 --> 00:12:50,540
returned type void and the documentation
there talks about it in terms of pixels.
163
00:12:50,540 --> 00:12:58,149
Now, really, we think of an oval as this
thing, right, as an object or a shape or
164
00:12:58,149 --> 00:13:02,310
something like that, right, as an entity
in its own right. But if you look at the
165
00:13:02,310 --> 00:13:05,540
documentation there, you can see that
drawOval doesn't create an object that
166
00:13:05,540 --> 00:13:11,779
corresponds to the notion or mind has of
an oval, right? It just flips the colors
167
00:13:11,779 --> 00:13:18,300
of a bunch of pixels in some imagined
canvas that drawOval paints on. So that's
168
00:13:18,300 --> 00:13:22,060
very different, right? And then the notion
of having a thing that's an oval is really
169
00:13:22,060 --> 00:13:27,339
something that our mind reconstructs from
those pixels. But that gives us a very
170
00:13:27,339 --> 00:13:32,920
limited sort of API for dealing with
images. And you can do that differently in
171
00:13:32,920 --> 00:13:37,339
a way that that is amenable to algebra and
mathematics. And well, you can find that
172
00:13:37,339 --> 00:13:42,730
in several places. One that's particularly
accessible is the Racket Image Teachpack
173
00:13:42,730 --> 00:13:46,490
library that comes with the racket system.
So I put a download link down there,
174
00:13:46,490 --> 00:13:51,871
generally a great system to play with. And
so this is how it works: Well, Racket is a
175
00:13:51,871 --> 00:13:57,140
lisp like language, so the syntax works of
a different from Java or C in that when
176
00:13:57,140 --> 00:14:02,560
you call a function, the parentheses go,
around the function call and the arguments
177
00:14:02,560 --> 00:14:07,820
and the arguments are separated by white
space rather than commas. So first thing
178
00:14:07,820 --> 00:14:12,010
is you call a function called circle, you
pass it three arguments: 50, solid, and
179
00:14:12,010 --> 00:14:17,240
red, and it returns a red circle. Well, as
you might imagine. But really, I want you
180
00:14:17,240 --> 00:14:23,380
to understand that it doesn't flip pixels
or something like that. It really returns
181
00:14:23,380 --> 00:14:30,209
an object representing the circle. And
it's only the racket API that then
182
00:14:30,209 --> 00:14:35,740
displays that object as an actual picture
that we can view. But it could also do
183
00:14:35,740 --> 00:14:40,540
something else with that picture: save it
to a file, send it to somebody over the
184
00:14:40,540 --> 00:14:47,310
network or something like that. So well,
first function returns a circle. Second
185
00:14:47,310 --> 00:14:51,970
function is also square function that
returns a square. You can see I can put
186
00:14:51,970 --> 00:14:56,350
something, I can put outline instead of
solid to say that I want just the outline
187
00:14:56,350 --> 00:15:00,760
of a square or there's this blue star at
the bottom returned by the star function.
188
00:15:00,760 --> 00:15:04,269
So these three functions are kind of
primitive in the way that they create
189
00:15:04,269 --> 00:15:09,149
images out of thin air from a bunch of
numbers and strings. And here's another
190
00:15:09,149 --> 00:15:15,740
such function called right triangle that
creates a triangle out of thin air. Now
191
00:15:15,740 --> 00:15:20,540
there's three more operations here that
don't create something out of thin air. So
192
00:15:20,540 --> 00:15:24,041
there's the rotate function, for example:
it takes an image. An existing image - it
193
00:15:24,041 --> 00:15:28,200
has to exist before you call "rotate" and
rotates it, in this case by 10 degrees,
194
00:15:28,200 --> 00:15:32,600
just a little bit. And then there's two
other functions, flip-vertical, which
195
00:15:32,600 --> 00:15:36,730
flips an image vertically and flip-
horizontal, which flips it horizontally,
196
00:15:36,730 --> 00:15:43,380
so creates a mirror image, if you will.
Now, these two functions, they transform
197
00:15:43,380 --> 00:15:47,980
an image in some way. And what's important
to understand is an image object goes in
198
00:15:47,980 --> 00:15:53,620
and they returned an image object also.
And that image object that's returned, you
199
00:15:53,620 --> 00:15:59,300
can pass it to other operations. So, for
example, that's what happens here. You
200
00:15:59,300 --> 00:16:04,460
can, for example, rotate that triangle
again, as we did on the slide before. And
201
00:16:04,460 --> 00:16:07,940
you can pass that result, you can stick it
into flip-vertical to then flip the
202
00:16:07,940 --> 00:16:14,220
rotated image. Now what you see here is
particular examples. So "what happens to
203
00:16:14,220 --> 00:16:20,450
the triangle when you first rotate and
then flip?" But some of these things can
204
00:16:20,450 --> 00:16:25,730
be generalized to general equations that
hold for all images. So here's two very
205
00:16:25,730 --> 00:16:30,150
simple examples. The first one says, Well,
if I flip an image and I flip it again, I
206
00:16:30,150 --> 00:16:35,579
get the same image out again. And then I
think hopefully plays to your visual
207
00:16:35,579 --> 00:16:39,660
imagination or intuition. The second
equation says, Well, if you flip
208
00:16:39,660 --> 00:16:43,529
horizontally and then vertically or you do
it the other way around your first flip
209
00:16:43,529 --> 00:16:47,260
vertically and then horizontally, you get
the same result. And again that should
210
00:16:47,260 --> 00:16:52,589
conform to your visual intuition. So those
are traditional equations that
211
00:16:52,589 --> 00:17:00,170
characterize how images work and how image
construction works. And we can get some
212
00:17:00,170 --> 00:17:05,750
particularly useful equations from these
three operations that are on this slide
213
00:17:05,750 --> 00:17:10,750
here. Now what they do is, they don't just
take one image and output one image the
214
00:17:10,750 --> 00:17:16,620
way that rotate and the flips do, but they
take two images each and return one image
215
00:17:16,620 --> 00:17:21,120
that results from combining them. So the
first function, "beside", takes two images
216
00:17:21,120 --> 00:17:26,709
and sticks them together horizontally,
gives you the resulting image. "above"
217
00:17:26,709 --> 00:17:30,350
puts them above each other. Gives you the
result. An "overlay" puts them on top of
218
00:17:30,350 --> 00:17:36,840
each other. And these are operations. You
know, they have the same form as "plus" or
219
00:17:36,840 --> 00:17:42,970
list concatenation or multiplication or
"or" or "and" in the sense that "or" takes
220
00:17:42,970 --> 00:17:46,799
two Booleans and returns a Boolean. "plus"
takes two numbers, returns a number.
221
00:17:46,799 --> 00:17:51,320
"beside" takes two images, returns an
image. Same thing for "above" and
222
00:17:51,320 --> 00:17:54,550
"overlay". And whenever you have that, you
have a function that takes two things and
223
00:17:54,550 --> 00:17:59,220
returns one thing, you can think about
associativity and you should. And in fact,
224
00:17:59,220 --> 00:18:04,160
these functions, if you kind of work again
for your visual intuition, you figure out
225
00:18:04,160 --> 00:18:09,099
that "beside", "above" and "overlay" are
all associative operations. So, with
226
00:18:09,099 --> 00:18:12,780
"overlay", for example, should be
especially intuitive and that if you have
227
00:18:12,780 --> 00:18:16,190
three images on top of each other, it
should not matter whether you first kind
228
00:18:16,190 --> 00:18:20,659
of staple the top ones together and then
the bottom one to the bottom, or whether
229
00:18:20,659 --> 00:18:24,290
you first staple together the bottom two
and then put the top one on top. In each
230
00:18:24,290 --> 00:18:33,739
case, you have layers in the same
sequence. Now what can you do knowing that
231
00:18:33,739 --> 00:18:37,330
you have an associative operation? We
already talked about parallelization.
232
00:18:37,330 --> 00:18:43,489
Generally, you can do optimizations based
on some of the other equations, for
233
00:18:43,489 --> 00:18:47,109
example, the equation that says, "flip-
horizontal twice doesn't do anything". You
234
00:18:47,109 --> 00:18:51,710
can use that to optimize, right? When you
see somebody doing a flip twice, you just
235
00:18:51,710 --> 00:18:57,500
throw out those operations. You don't have
to compute the actual flip. You can also
236
00:18:57,500 --> 00:19:01,940
imagine computations where you can cache
intermediate results in the same way that
237
00:19:01,940 --> 00:19:07,369
you kind of process that parallel
computation in a tree-shape, and it gives
238
00:19:07,369 --> 00:19:13,309
you great flexibility in that caching and
recombining the cached values. So you can
239
00:19:13,309 --> 00:19:17,999
generally just use that for performance.
You could also turn those equations into
240
00:19:17,999 --> 00:19:22,049
what's called property based testing.
Right. You could stick in random values
241
00:19:22,049 --> 00:19:27,309
for the variables and test whether
equations are actually fulfilled. And that
242
00:19:27,309 --> 00:19:31,360
might help you debug or ensure the
correctness of your library. And finally,
243
00:19:31,360 --> 00:19:35,559
if you really need something to be
correct, then you could provide for the
244
00:19:35,559 --> 00:19:40,559
proofs giving you added assurance using a
technique called induction, because you
245
00:19:40,559 --> 00:19:45,220
combine two things into a thing that you
kind of have to walk that construction
246
00:19:45,220 --> 00:19:50,590
backwards. But again, this talk is not
really concerned with proof so much. But
247
00:19:50,590 --> 00:19:56,340
again, I mentioned that earlier, I really
want to talk about the modeling aspect
248
00:19:56,340 --> 00:20:01,389
that this mathematical way of thinking
about it suggests, right? Again, remember
249
00:20:01,389 --> 00:20:06,690
of the Java drawOval function that just
flips the color of a bunch of pixels. And
250
00:20:06,690 --> 00:20:10,570
here is the picture. But really, we view
this picture - our minds views this
251
00:20:10,570 --> 00:20:17,429
picture as a bunch of concentric circles,
and each circle is a thing in its own
252
00:20:17,429 --> 00:20:25,059
right. Now, I don't know what's intuitive
to you, but apparently it was intuitive to
253
00:20:25,059 --> 00:20:32,510
some people to create that first function
drawOval. And that mathematical intuition
254
00:20:32,510 --> 00:20:37,159
really tells you, well, make pictures,
make images into objects and then create
255
00:20:37,159 --> 00:20:44,429
abstractions based upon them. So we can
use mathematics to kind of create you
256
00:20:44,429 --> 00:20:48,240
create equations after the fact. But
really, mathematics gives us great
257
00:20:48,240 --> 00:20:52,940
suggestions as what the library, what the
API should look like in the first place
258
00:20:52,940 --> 00:20:58,340
that. Well, I often see people doing
something else, so that intuition might
259
00:20:58,340 --> 00:21:02,609
have something to do with that
mathematical understanding. So let me talk
260
00:21:02,609 --> 00:21:06,859
a little bit more about that language of
mathematics. Now that we figured out the
261
00:21:06,859 --> 00:21:12,720
importance of associativity or equations
in general. So, people working in algebra,
262
00:21:12,720 --> 00:21:19,179
they always talk about structures that
have three pieces, right? One piece is a
263
00:21:19,179 --> 00:21:25,619
mathematical set. So just a collection of
a bunch of things, of objects. Then they
264
00:21:25,619 --> 00:21:29,570
have operations on those sets and then
they have equations involving those
265
00:21:29,570 --> 00:21:33,279
operations. On the right hand side, you
can see what we know already. So we have
266
00:21:33,279 --> 00:21:37,460
some set "M"; it could be anything, could
be Booleans, could be numbers, could be
267
00:21:37,460 --> 00:21:41,580
images. And then you have an Operation
Diamond that combines two of those M's
268
00:21:41,580 --> 00:21:47,039
into one M. We here's a little bit funny
notation, right? With a cross there. What
269
00:21:47,039 --> 00:21:51,899
it says is there's two inputs right cross,
cross, cross for each input. And so the
270
00:21:51,899 --> 00:21:56,450
diamond operation has one M as an input,
another M as an input. And then there's
271
00:21:56,450 --> 00:22:02,259
the arrow and that says that there's also
an M as the output. And then finally,
272
00:22:02,259 --> 00:22:06,360
there's that associativity equation that
we've already seen quite a few times
273
00:22:06,360 --> 00:22:10,840
today. And those three things packaged up
together, the set and the operation on
274
00:22:10,840 --> 00:22:16,299
that set (in this case just a single
operation) and equations (in this case,
275
00:22:16,299 --> 00:22:20,289
associativity), this is all called a semi
group. There are other algebraic
276
00:22:20,289 --> 00:22:25,679
structures that we'll see. Now this
translates directly to programing. Your
277
00:22:25,679 --> 00:22:31,600
set "M" in mathematics might just be a type
in your program. And these semi groups, they
278
00:22:31,600 --> 00:22:34,460
occur in lots of places. So all of those
things that we've already seen with
279
00:22:34,460 --> 00:22:37,820
associativity, you could just kind of
shorten your language and say, all of
280
00:22:37,820 --> 00:22:42,580
those things are semi groups. So, for
example, at the top, it says: if you take
281
00:22:42,580 --> 00:22:47,140
the mathematical set of real numbers,
(that's that funny "R", that hollow "R"),
282
00:22:47,140 --> 00:22:53,690
the real numbers, with the plus operation,
(it takes two numbers from the "R" set and
283
00:22:53,690 --> 00:22:57,860
produces one number), of course, has
associativity and therefore it's a semi
284
00:22:57,860 --> 00:23:04,220
group. Lists, with concatenation, fulfill
the associativity equation. Therefore,
285
00:23:04,220 --> 00:23:08,899
they form a semi group. And, for example,
the "overlay" operation from the images,
286
00:23:08,899 --> 00:23:14,489
just as "beside" and "above" do, has that
same shape, right? Combines two images
287
00:23:14,489 --> 00:23:19,570
into one image and fulfills associativity,
Therefore, images and "overlay" form a
288
00:23:19,570 --> 00:23:25,549
semi group. Now, a semi group is not the
only algebraic structure, but it's a
289
00:23:25,549 --> 00:23:30,070
fairly humble one. It can't do a whole lot
and therefore kind of mathematicians build
290
00:23:30,070 --> 00:23:34,979
up from them. They take a simple algebraic
structure and they add more operations or
291
00:23:34,979 --> 00:23:38,929
something else to it. So, for example, the
next step up from a semi group is
292
00:23:38,929 --> 00:23:46,429
something called a monoid. So you take a
semi group and you add something, and I'll
293
00:23:46,429 --> 00:23:50,100
try to explain what that is. So again, you
have to set you have a binary operation,
294
00:23:50,100 --> 00:23:55,261
that diamond operation. And you also say
that in that system, there has to be a
295
00:23:55,261 --> 00:24:00,700
special element. And you have to know what
it is. And that element is called
296
00:24:00,700 --> 00:24:05,509
"bottom". That's what that line says, you
know, that upside-down tee, that's what I
297
00:24:05,509 --> 00:24:10,950
call "bottom". And it also has to be part
of that set M. And now, as usual because
298
00:24:10,950 --> 00:24:15,700
every monoid is a semi group, the
associativity equation holds. And the
299
00:24:15,700 --> 00:24:19,989
bottom line explains about the identity
element about the bottom element, where it
300
00:24:19,989 --> 00:24:25,590
says, Well, if you use the diamond
operator to combine "a" with the identity
301
00:24:25,590 --> 00:24:31,159
or identity with "a", you get back "a". In
German, you often use the word "neutral
302
00:24:31,159 --> 00:24:37,529
element". So it's neutral with with
respect to the binary operation that you
303
00:24:37,529 --> 00:24:42,429
have in your semi group. And hopefully
that appeals to your intuition as it does
304
00:24:42,429 --> 00:24:47,690
to mine. And if you take an algebra class
at the university level, you might learn
305
00:24:47,690 --> 00:24:52,669
about more involved algebraic structures,
such as groups and rings and fields. And
306
00:24:52,669 --> 00:24:56,789
every time you go a step up, right, a
monoid is a semi group plus a neutral
307
00:24:56,789 --> 00:25:02,820
element. A group is a monoid with even
more operations and more equations. A Ring
308
00:25:02,820 --> 00:25:10,529
even involves a another operation and more
laws. Same thing for a field. So, you just
309
00:25:10,529 --> 00:25:14,809
add a bunch of stuff as you go up the
ladder. But for hacking, really? For
310
00:25:14,809 --> 00:25:19,580
computing, for writing software, the two
most important ones from that stack here
311
00:25:19,580 --> 00:25:23,229
are semi group and monoid and you don't
really have to worry about the rest unless
312
00:25:23,229 --> 00:25:28,509
you really write mathematically inclined
software that involves those algebraic
313
00:25:28,509 --> 00:25:32,889
instructions. So we've seen a bunch of
semi groups. Have we seen a bunch of
314
00:25:32,889 --> 00:25:36,210
monoids? Yeah. Well, essentially all the
semi groups that we've already seen are
315
00:25:36,210 --> 00:25:42,729
also monoids. So for example, the plus
operation on the numbers; zero is the
316
00:25:42,729 --> 00:25:46,410
identity there: you add zero to a number,
you get back that same number. With
317
00:25:46,410 --> 00:25:51,580
multiplication, well you multiply a number
by one, you get back that same number. If
318
00:25:51,580 --> 00:25:54,739
you have a list you concatenate with it
the empty list, doesn't matter whether
319
00:25:54,739 --> 00:26:00,649
it's left or right, well, sure enough, you
get the same list. Now the bottom three
320
00:26:00,649 --> 00:26:04,720
examples might look a little bit funny
because they suggest that there's an
321
00:26:04,720 --> 00:26:09,999
identity for this those operations, but
they all are the empty image, so they're
322
00:26:09,999 --> 00:26:16,009
invisible. And so that points that out to
you. And monoids - I can't really over
323
00:26:16,009 --> 00:26:22,059
emphasize this - monoids are everywhere
around us. So, a well-known software
324
00:26:22,059 --> 00:26:26,600
engineer asked me a while ago and said:
Well, your mathematical structure is all
325
00:26:26,600 --> 00:26:32,019
good and well, but what about really
concrete software things? You know, we use
326
00:26:32,019 --> 00:26:35,240
shopping carts. How could you possibly use
mathematical structure for a shopping
327
00:26:35,240 --> 00:26:40,970
cart? Therefore as well, a shopping cart -
you might have a shopping cart associated
328
00:26:40,970 --> 00:26:46,140
with your account at some shop. Right? But
on another day you might go shopping, you
329
00:26:46,140 --> 00:26:51,889
forget to log into your account. But you
can usually still fill a shopping cart.
330
00:26:51,889 --> 00:26:57,760
Now, once you checkout that shopping cart,
you buy the stuff in it, it will usually
331
00:26:57,760 --> 00:27:01,210
ask you to log in. Now there's two
shopping carts, one inside your account
332
00:27:01,210 --> 00:27:06,929
and the one that you just filled. They
have to be combined into one. And really,
333
00:27:06,929 --> 00:27:10,229
it's worthwhile to think about what
properties that combination operation
334
00:27:10,229 --> 00:27:15,539
should have. But there's many other
examplesfor monoids. I have some concrete
335
00:27:15,539 --> 00:27:21,000
examples from applications that I've
worked on. A famous paper in functional
336
00:27:21,000 --> 00:27:23,230
programing, for example, is about
financial contracts - sure ehough, they
337
00:27:23,230 --> 00:27:29,260
form a monoid. Recently, I talked to a
company that makes configurable flower
338
00:27:29,260 --> 00:27:33,109
bouquets, so you might have well, you
might combine two flowers, two sets of
339
00:27:33,109 --> 00:27:37,589
flowers into one to form a bouquet. You
know, all kinds of things. Monoliths
340
00:27:37,589 --> 00:27:43,940
really are everywhere around us. So much
that, my friend Conal Elliott has elevated
341
00:27:43,940 --> 00:27:48,240
this to a general design principle,
whenever you write software for a
342
00:27:48,240 --> 00:27:53,559
particular domain, you should look for
mathematical algebraic structure. And
343
00:27:53,559 --> 00:27:56,940
because monoids are so common, one thing
that you can always try is look for binary
344
00:27:56,940 --> 00:28:01,750
operation on your objects. Check of the
associative law holds. Look for an
345
00:28:01,750 --> 00:28:08,419
identity. And if you don't find that
binary operation, OK, but it's not
346
00:28:08,419 --> 00:28:12,960
associative, you know, that's maybe a sign
that you should try to make it
347
00:28:12,960 --> 00:28:17,210
associative. Doesn't always work, but
frequently does. And and usually gives you
348
00:28:17,210 --> 00:28:20,130
some improvement in the process. Same
thing for identity: If there isn't one,
349
00:28:20,130 --> 00:28:25,469
you might make one up, trusting that you
might need it later. Conal calles this the
350
00:28:25,469 --> 00:28:29,759
Tao check. Something that I really like.
It's whether the software model that
351
00:28:29,759 --> 00:28:35,059
you're creating aligns with mathematics.
And that means, with the deeper structure
352
00:28:35,059 --> 00:28:38,999
of the universe that humanity has
discovered in the hundreds of years that
353
00:28:38,999 --> 00:28:44,070
were there before computing. Monoids are
also useful in differentiation from things
354
00:28:44,070 --> 00:28:47,399
that are not monoids. So, for example, the
maximum operation that gives you the
355
00:28:47,399 --> 00:28:51,509
bigger of two numbers does not form a
monoid. It gives you a semi group. It's
356
00:28:51,509 --> 00:28:57,710
associative, but well, there's no
identity, right? Thinking about it, you
357
00:28:57,710 --> 00:29:02,149
might think, well, but can't I take minus
infinity or something like that? But of
358
00:29:02,149 --> 00:29:06,960
course, that's not a real number. But it
maybe gives you a hint as to how you could
359
00:29:06,960 --> 00:29:11,869
complete that structure if you really need
a monoid. I'll get back to that in a
360
00:29:11,869 --> 00:29:17,200
second, but first I want to talk about a
general principle in that, it's not just
361
00:29:17,200 --> 00:29:22,229
discovering monoids in the domain of
objects around you, you can also construct
362
00:29:22,229 --> 00:29:27,509
monoids systematically. Specifically, you
can create larger monoids out of smaller
363
00:29:27,509 --> 00:29:31,539
ones. So this is probably the most
complicated slide that I have. So don't
364
00:29:31,539 --> 00:29:35,249
worry, it'll be over in the second, but
we'll try to go through it line by line.
365
00:29:35,249 --> 00:29:40,080
So imagine you have two momoids. The first
one is called M1, the second one is called
366
00:29:40,080 --> 00:29:44,929
M2, and each has their own diamond
combination operation. The first one is
367
00:29:44,929 --> 00:29:50,389
called Diamond 1, the second one is called
Diamond 2. The first one takes two M1s,
368
00:29:50,389 --> 00:29:56,559
gives you back an M1. The second one takes
two M2s and gives you back an M2. Now,
369
00:29:56,559 --> 00:30:03,169
using those two momoids, you can create a
larger monoid by taking pairs of elements
370
00:30:03,169 --> 00:30:08,100
from M1 and M2. That's what those funny
cross means. It's something called the
371
00:30:08,100 --> 00:30:13,969
Cartesian product; out of two sets, it
forms the set of pairs where there's one
372
00:30:13,969 --> 00:30:19,430
from each of those two sets in there. And
in order to make that a monoid, we have to
373
00:30:19,430 --> 00:30:23,649
define the binary operation. I'm just
going to call it diamond. You can see the
374
00:30:23,649 --> 00:30:28,210
diamond is defined in such a way that one
pair out of M1 and M2 goes in, another pair
375
00:30:28,210 --> 00:30:34,460
out of M1 and M2 goes in and it returns
another pair out of M1 and M2. And the way
376
00:30:34,460 --> 00:30:39,940
it's defined is, you take two pairs and
you combine the first elements from both
377
00:30:39,940 --> 00:30:45,239
pairs using the M1 monoid and the Diamond
one operation. And you combine the second
378
00:30:45,239 --> 00:30:51,239
elements of both pairs using the diamond
operation from the M2 monoid. And sure
379
00:30:51,239 --> 00:30:55,850
enough, that gives you an operation that's
associative. I didn't put that on the
380
00:30:55,850 --> 00:30:59,479
slide, but it also gives you an identity
with a pair that consists of the
381
00:30:59,479 --> 00:31:07,659
individual identities from M1 and M2. You
know, that works. Also, sometimes you have
382
00:31:07,659 --> 00:31:12,860
a semi group lying around, but you really
need a monoid. I mean, a semi group that's
383
00:31:12,860 --> 00:31:15,970
not a momoid, but you really need a
monoid. Here's a little construction that
384
00:31:15,970 --> 00:31:21,330
will build a monoid from a semi group. So
again, we start with the set. We start
385
00:31:21,330 --> 00:31:25,809
with a binary operation on that set called
diamond, and then we create another set
386
00:31:25,809 --> 00:31:30,110
that I call M-bottom (again, that funny
upside-down tee that you see there). And
387
00:31:30,110 --> 00:31:35,009
we create it by adding artificially one
new element to it, right? It can be in
388
00:31:35,009 --> 00:31:44,659
there before. And then we define a new
operation, Diamond-bottom, that operates
389
00:31:44,659 --> 00:31:50,409
on that set. And and we just define it in
such a way that,if either side of that
390
00:31:50,409 --> 00:31:54,859
operation is the identity, the bottom
element, we just have it return the other
391
00:31:54,859 --> 00:32:01,259
side. So, "a, Diamond-bottom, bottom"
returns, you "a", and the same thing the
392
00:32:01,259 --> 00:32:07,370
other way around. And whenever that
operation is called on two things that are
393
00:32:07,370 --> 00:32:12,529
not bottom, we just call the original
operation. And sure enough, that gives you
394
00:32:12,529 --> 00:32:16,470
a monoid. [glitch] that the thing before,
the M before, was just a semi group, and
395
00:32:16,470 --> 00:32:20,200
you might have seen that construction when
programing. So, for example, the Java
396
00:32:20,200 --> 00:32:25,320
library has something called an option,
and that is exactly that. And again, when
397
00:32:25,320 --> 00:32:29,249
you're defining abstractions like that,
the mathematical notion of the
398
00:32:29,249 --> 00:32:34,169
mathematical equations can provide a guide
as to how that API should behave if it's
399
00:32:34,169 --> 00:32:38,539
supposed to be reasonable. If you're still
bear with me and have a little bit of
400
00:32:38,539 --> 00:32:44,529
patience left, here's another concept it's
a little bit more abstract called the
401
00:32:44,529 --> 00:32:49,309
homomorphism. And that's useful and
thinking about APIs, at least APIs that
402
00:32:49,309 --> 00:32:54,940
combine in this way via something like a
monoid. So look at the first equation: It
403
00:32:54,940 --> 00:33:00,279
says, well, if you take an overlay of two
images, a and b, - more like this - right,
404
00:33:00,279 --> 00:33:04,120
and you rotate it, that is the same as
taking one image, rotating it, take
405
00:33:04,120 --> 00:33:10,049
another image, rotating it and slapping
them together after the fact. And what
406
00:33:10,049 --> 00:33:15,109
that means is really, "rotate" here is
what's called a homomorphism that can kind
407
00:33:15,109 --> 00:33:22,149
of slip inside the overlay operation. Or
another way to talk about it is, commutes
408
00:33:22,149 --> 00:33:27,029
or can trade places with the overlay
operation in that, on the left hand side
409
00:33:27,029 --> 00:33:31,269
of the equation, the rotate is outside and
the overlay is inside, and on the other
410
00:33:31,269 --> 00:33:34,819
side of the equation, it's exactly the
other way around. With the next equation
411
00:33:34,819 --> 00:33:38,909
there flip-vertical of beside, [noise
while indicating the flip], right, and
412
00:33:38,909 --> 00:33:45,049
then the idea is, well, you flip one, you
flip one and then do "beside". That's
413
00:33:45,049 --> 00:33:48,350
certainly eminently reasonable, but if you
think about it, it might depend on the
414
00:33:48,350 --> 00:33:52,460
alignment that you choose for your images
as you put them side to side, right, you
415
00:33:52,460 --> 00:33:57,589
might decide to align them by the top half
like this. And then you might come to the
416
00:33:57,589 --> 00:34:01,940
conclusion that that equation does not
hold. So, but again, it provides a guide.
417
00:34:01,940 --> 00:34:05,749
It probably should hold - you should
design the "beside" operation in such a
418
00:34:05,749 --> 00:34:11,420
way that it works. Now the equation at the
bottom really does not work, right? There
419
00:34:11,420 --> 00:34:19,339
it is. But if you have five minutes after
this talk, or even now, you might think
420
00:34:19,339 --> 00:34:22,889
about an equation that's very similar to
that one, that does hold and that gives
421
00:34:22,889 --> 00:34:29,480
you some insight. That's also a useful
notion when you're designing APIs. Here's
422
00:34:29,480 --> 00:34:36,100
another useful notion in that, Well, with
images, there's the visual aspect, right,
423
00:34:36,100 --> 00:34:39,730
that if you perceive images by looking at
a certain pair of coordinates and
424
00:34:39,730 --> 00:34:45,200
perceiving a certain color. And that color
might be, you might represent it by a
425
00:34:45,200 --> 00:34:49,490
value and that value might come from
different types. And that gives you
426
00:34:49,490 --> 00:34:54,500
different notions of images. So, for
example, the image of bools well, so it
427
00:34:54,500 --> 00:34:58,920
means each coordinate can only be on or
off, or black and white. So it gives you
428
00:34:58,920 --> 00:35:02,800
black and white picture. The next one,
where there's just a number there might
429
00:35:02,800 --> 00:35:12,640
give you some some notion of grayscale. Or
you would, of course, then as in the
430
00:35:12,640 --> 00:35:16,340
bottom two examples, you could stick RGB
triples in there to give you arbitrary
431
00:35:16,340 --> 00:35:20,230
colors or even an alpha channel or
something like that. So when you have a
432
00:35:20,230 --> 00:35:25,310
type such as image that has a parameter,
very frequently you can add a little bit
433
00:35:25,310 --> 00:35:29,430
of structure, what's called a map
operation that you might have seen (not
434
00:35:29,430 --> 00:35:33,520
going to worry about the details there),
but you might get a structure called a
435
00:35:33,520 --> 00:35:42,020
functor. And the word functor comes from a
particularly abstract branch of algebra
436
00:35:42,020 --> 00:35:45,210
called category theory. But even, you
know, the mathematicians sometimes call
437
00:35:45,210 --> 00:35:51,770
that abstract nonsense. But, despite the
term, it really is something that's very
438
00:35:51,770 --> 00:35:56,830
useful and very insightful and it gives
you a lot of insight into the structure of
439
00:35:56,830 --> 00:36:01,830
things. And category theory frequently
describes relationships between things
440
00:36:01,830 --> 00:36:06,540
through diagrams that are quite beautiful.
So here's a characterization of the idea
441
00:36:06,540 --> 00:36:14,580
of a monoid. You don't have to understand
the diagram, but maybe, after this and
442
00:36:14,580 --> 00:36:18,110
after you've mastered monoids for a while,
you'll have look at category theory and
443
00:36:18,110 --> 00:36:22,960
enjoy it. You get more complicated
diagrams such as this one in more involved
444
00:36:22,960 --> 00:36:30,070
abstractions such as, I mentioned functor.
There's also the infamous monad and these
445
00:36:30,070 --> 00:36:35,870
are things that are practical, eminently
practical for creating higher order and
446
00:36:35,870 --> 00:36:41,070
generally higher level abstractions.
Again, not for this talk. That's a
447
00:36:41,070 --> 00:36:46,870
different talk. But I hope I've instilled
in you the sense that mathematics, at
448
00:36:46,870 --> 00:36:50,830
least this kind of simple mathematics, is
useful. If you felt that it hasn't been
449
00:36:50,830 --> 00:36:55,290
simple, that it's been hard, I want to
point out that, well, it might be hard to
450
00:36:55,290 --> 00:37:00,950
understand everything that's been on the
slides on this talk, but it's not due to
451
00:37:00,950 --> 00:37:05,980
the fact that it's complicated. It's not.
There's not a lot of moving parts or
452
00:37:05,980 --> 00:37:11,840
something like that, but it is abstract,
and the human mind needs some time. It
453
00:37:11,840 --> 00:37:14,810
finds it difficult to deal with
abstraction, and therefore you might -
454
00:37:14,810 --> 00:37:18,630
also, if you're interested in this stuff -
you might give your mind some time to get
455
00:37:18,630 --> 00:37:22,870
adjusted to those mathematical concepts
and maybe look at it again a couple of
456
00:37:22,870 --> 00:37:29,350
weeks. Just have a brief look. You know,
maybe look for a monoid or just a binary
457
00:37:29,350 --> 00:37:34,090
operation, look for associativity and by
and by, that stuff will become more
458
00:37:34,090 --> 00:37:38,600
familiar and commonplace to you, and
you'll find it easier to deal with it. And
459
00:37:38,600 --> 00:37:42,770
once that happens, I think you'll find
that very satisfying. So that's pretty
460
00:37:42,770 --> 00:37:48,910
much it. If you want to read up some more
detail on this, I put in four references
461
00:37:48,910 --> 00:37:52,150
that are linked from the slides that you
hopefully download from somewhere. But you
462
00:37:52,150 --> 00:37:59,560
can also just search for those titles and
you'll find those papers. So first one is
463
00:37:59,560 --> 00:38:03,820
a paper by Brent Yorgey that really takes
that idea of using monoids to structure an
464
00:38:03,820 --> 00:38:11,120
image library to the limit. That's just a
great paper. Then there's a book by Sandy
465
00:38:11,120 --> 00:38:17,630
Maguire on algebra-driven design, applies
that idea to different practical settings.
466
00:38:17,630 --> 00:38:22,330
Conal Elliot gave a great foundational
type talk on something called denotational
467
00:38:22,330 --> 00:38:25,330
design. So that's a video. Also has a
paper, but I really recommend you look at
468
00:38:25,330 --> 00:38:29,690
the video. And the classic paper that
introduced this notion of dealing with
469
00:38:29,690 --> 00:38:33,900
images by combining them is by Peter
Henderson, something called functional
470
00:38:33,900 --> 00:38:40,680
geometry. And I hope you'll enjoy looking
at that stuff as much as I will. And I
471
00:38:40,680 --> 00:38:51,880
hope you enjoy the Congress. I hope to see
you around. Well, have a good time. Bye.
472
00:38:51,880 --> 00:38:59,150
Herald: So thank you for this interesting
talk, Michael. And there are a few
473
00:38:59,150 --> 00:39:04,610
questions from the internet already. And
for those who haven't asked questions yet,
474
00:39:04,610 --> 00:39:13,020
if you use the hashtag #rc3cwtv on either
Twitter, Mastodon or the proper IRC
475
00:39:13,020 --> 00:39:18,440
channel, we can still include them in this
Q&A. And the first question I would like
476
00:39:18,440 --> 00:39:25,730
to ask you, Michael, is maybe a strange
one, but you mentioned this concept of
477
00:39:25,730 --> 00:39:33,370
homomorphisms of the monoids. And I was
wondering whether we could do the reverse
478
00:39:33,370 --> 00:39:40,010
rounds. Could could you use these
mathematics to visualize APIs?
479
00:39:40,010 --> 00:39:49,190
Michael: That's an excellent question. So
let me think about it for a moment..., so
480
00:39:49,190 --> 00:39:57,670
with a monoid... So yeah, so the answer
is, first of all, yes. So with the monoid,
481
00:39:57,670 --> 00:40:02,290
one way to think about a monoid is not
just this abstract thing that's going on
482
00:40:02,290 --> 00:40:08,480
right, but since, any value in the monoid,
can kind of be built up by this operation
483
00:40:08,480 --> 00:40:14,090
that's sitting in the monoid, you could
also just represent a monoid not just by
484
00:40:14,090 --> 00:40:22,601
some abstraction, but you can build what's
called a free structure, and that is tree
485
00:40:22,601 --> 00:40:26,950
structured and that you could visualize.
So that's one half of the answer. And on
486
00:40:26,950 --> 00:40:31,000
the last slide, I had to reference the
very first reference on a paper by Brent
487
00:40:31,000 --> 00:40:36,520
Yorgey shows how that works. And it's
generally a paper on visualization. So
488
00:40:36,520 --> 00:40:41,100
that would be one half of the answer. The
other half is that I remember one
489
00:40:41,100 --> 00:40:45,400
industrial project that I've worked on
where people wanted - so there was kind of
490
00:40:45,400 --> 00:40:50,870
a complicated data flow problem, and the
requirement of the customer was, well,
491
00:40:50,870 --> 00:40:57,380
people want to assemble a configuration
for a scheduling problem in semiconductor
492
00:40:57,380 --> 00:41:01,130
fabrication, if you will. And they said,
Well, we want we just want a bunch of
493
00:41:01,130 --> 00:41:06,520
boxes and arrows, and people should be
able to arrange that visually to specify a
494
00:41:06,520 --> 00:41:12,440
configuration. And we ended up looking for
the right formalism to do that. In fact,
495
00:41:12,440 --> 00:41:17,150
there is one in category theory. And
category theory generally is diagrams, but
496
00:41:17,150 --> 00:41:20,550
there is a concept in Category theory
which just happened to fit, and we found
497
00:41:20,550 --> 00:41:29,070
it by going from the customer requirement
to the mathematics. And that gave us a
498
00:41:29,070 --> 00:41:34,460
naturally and very pleasant and actually
mathematically precise visualization form
499
00:41:34,460 --> 00:41:39,380
for that. So I'd argue it's a great tool
to think about visualization. Hope that
500
00:41:39,380 --> 00:41:44,070
helps a little bit.
H: OK, so we can finally look forward to
501
00:41:44,070 --> 00:41:48,960
this, this kind of Neuromancer-like
landscapes while hacking.
502
00:41:48,960 --> 00:41:52,700
Michael: Well, yeah, it feels like that
sometimes, yes.
503
00:41:52,700 --> 00:41:56,340
H: Another question was from a viewer who
had never seen such sexy algebra in their
504
00:41:56,340 --> 00:42:01,820
life: Whether you're willing to submit a
proposal next year to go into a little
505
00:42:01,820 --> 00:42:09,060
more in-depth continuation of this talk.
M: Sure. I'm very happy to.
506
00:42:09,060 --> 00:42:14,080
H: That's a short answer to a relatively
long...
507
00:42:14,080 --> 00:42:18,180
M: OK. Can't say you haven't been warned,
but yeah, I'll try.
508
00:42:18,180 --> 00:42:24,840
H: Yeah, and also it needs to be accepted
by the content team, obviously. Another
509
00:42:24,840 --> 00:42:29,350
question that is about something you said
you wouldn't talk about, and that is about
510
00:42:29,350 --> 00:42:34,390
formal verification of algorithms *M:
Yeah*, but none the less might be useful
511
00:42:34,390 --> 00:42:40,180
for the audience to know if they're
seeking formal verification for
512
00:42:40,180 --> 00:42:43,700
algorhithms. What avenues you would
suggest to people, especially people
513
00:42:43,700 --> 00:42:48,480
without much of a formal background in
mathematics, to start looking at, as in,
514
00:42:48,480 --> 00:42:54,370
placed for further learning.
M: Yes. Yeah, that's that's an excellent
515
00:42:54,370 --> 00:42:58,650
question. So I think one place that I'd
start with, and I think there have been
516
00:42:58,650 --> 00:43:02,190
talks about this at earlier iterations the
of the Congress that I'm sure you can
517
00:43:02,190 --> 00:43:06,860
find. There is, in fact, there's a new, if
you will, family of programing languages
518
00:43:06,860 --> 00:43:11,410
that are based on strong types called
dependent types. And they're very
519
00:43:11,410 --> 00:43:16,070
expressive and they allow you to express
mathematical properties. Now, in the old
520
00:43:16,070 --> 00:43:20,480
days, we would write down a mathematical
property, of a program that we wanted to
521
00:43:20,480 --> 00:43:25,450
have, and then we would use - if things
are good, we would use a proof assistant
522
00:43:25,450 --> 00:43:31,031
to find the proof, and that would be a
very cumbersome process that you would
523
00:43:31,031 --> 00:43:35,630
have to do. Now, with this new family of
programing languages, Idris and Agda are
524
00:43:35,630 --> 00:43:42,910
two prominent examples, what you can do is
you can give the type and you can push a
525
00:43:42,910 --> 00:43:46,130
button (essentially - it's not quite so
easy, but there's actually IDE support
526
00:43:46,130 --> 00:43:50,050
where you can push a couple of buttons and
it will generate a program that has that
527
00:43:50,050 --> 00:43:56,010
type). And that program is guaranteed to
be correct, right? Because with the
528
00:43:56,010 --> 00:43:59,940
combination of the type and the program
itself, there is the proof right there
529
00:43:59,940 --> 00:44:05,490
sitting there. And that, at least for
simpler things, takes away a lot of the
530
00:44:05,490 --> 00:44:12,540
burden, at least at the burden of getting
into this kind of tool. It's still kind of
531
00:44:12,540 --> 00:44:16,080
intricate work to put together more
complicated proofs, but to get into that
532
00:44:16,080 --> 00:44:20,490
medium, it's just great fun and it's a
very satisfying activity. And you don't
533
00:44:20,490 --> 00:44:23,150
have that impression that you sometimes
have with proof assistants that you're
534
00:44:23,150 --> 00:44:28,260
kind of fiddling in the dark with a
screwdriver. So, it it's a concrete place
535
00:44:28,260 --> 00:44:31,030
that you're looking for. I would I would
recommend looking at a programing language
536
00:44:31,030 --> 00:44:35,090
called Idris and maybe look at some of the
Congress talks that we've had about in the
537
00:44:35,090 --> 00:44:41,070
past.
H: Yeah. Having been to at least one of
538
00:44:41,070 --> 00:44:45,830
those Congress talks, I also would ask a
follow up question to that: Does the new
539
00:44:45,830 --> 00:44:51,730
typing capability that, for example, Rust
provides, rise to this level that you
540
00:44:51,730 --> 00:44:55,320
mentioned with Idris and other languages,
or is that not advanced enough for that
541
00:44:55,320 --> 00:44:58,600
yet?
M: I'm not an expert on rust. I haven't
542
00:44:58,600 --> 00:45:05,540
seen IDE support on that level. I'm pretty
sure the type - I mean Rust has a type
543
00:45:05,540 --> 00:45:10,450
system that has a specific kind of
expressive capability that allows you to
544
00:45:10,450 --> 00:45:15,190
express memory safety. Right? And then
because, your type-correct program, if
545
00:45:15,190 --> 00:45:18,550
you're not using the unsafe features, is
guaranteed, is kind of proven to be
546
00:45:18,550 --> 00:45:27,030
correct and to adhere to those to those
memory safety criteria. But I have not
547
00:45:27,030 --> 00:45:32,020
seen the general expressivity that
language is like Idris gives you in Rust.
548
00:45:32,020 --> 00:45:39,420
Maybe there's a way to do it, but I'm I'm
reasonably confident it's not as practical
549
00:45:39,420 --> 00:45:44,430
and not as easy to get into.
H: Yeah, and also it's very off-topic
550
00:45:44,430 --> 00:45:48,940
since you said you wouldn't be talking
about this anyway right now. So we're sort
551
00:45:48,940 --> 00:46:01,020
of veering. One of the other questions is,
will you be around in the 2D world
552
00:46:01,020 --> 00:46:03,830
sometime to talk directly to people from
the audience?
553
00:46:03,830 --> 00:46:09,870
M: Yeah, sure, we'll do that right after
the talk. Maybe after a little lunch
554
00:46:09,870 --> 00:46:12,420
break.
H: And then what nickname will you be and
555
00:46:12,420 --> 00:46:15,480
where will you be hanging out?
M: My Twitter handle, which was also being
556
00:46:15,480 --> 00:46:21,050
called "sperbsen".
H: We have this 2D rc3 world, this kind of
557
00:46:21,050 --> 00:46:26,710
online adventure thing where the people
visiting are walking around with their
558
00:46:26,710 --> 00:46:31,260
avatars and, well you haven't been there
yet, I take it from your...
559
00:46:31,260 --> 00:46:34,330
M: No, no, no. I have been there. I'm just
saying my avatar there has the same name
560
00:46:34,330 --> 00:46:37,270
as my Twitter handle.
H: I'm sorry. I'm sorry for interrupting
561
00:46:37,270 --> 00:46:40,300
you..
M: So it's called "sperbsen" "Sperber" was
562
00:46:40,300 --> 00:46:44,340
not available anymore.
H: I apologize.
563
00:46:44,340 --> 00:46:52,730
M: So I'll be there.
H: And I think this... There's another
564
00:46:52,730 --> 00:46:58,720
question, and it's: Could something like a
Turing machine have been constructed with
565
00:46:58,720 --> 00:47:06,750
the mathematics of 2000 years ago?
M: So I got to Turing machine and I got
566
00:47:06,750 --> 00:47:08,640
mathematics as of two thousand years ago,
but I lost...
567
00:47:08,640 --> 00:47:12,730
H: Could something like a Turing machine
be constructed with the mathematics of two
568
00:47:12,730 --> 00:47:17,930
thousand years ago. This may be a bit of a
speculative question.
569
00:47:17,930 --> 00:47:28,400
M: I don't see anything that wasn't there.
I don't see why not. I'm not 100 percent
570
00:47:28,400 --> 00:47:34,670
sure what exactly the mathematics of 2000
years ago was, right. You know, my basic
571
00:47:34,670 --> 00:47:40,320
knowledge goes back a couple of hundred
years, but the basic mechanism of a Turing
572
00:47:40,320 --> 00:47:44,280
machine is very simple. It's not my
preferred mechanism to talk about
573
00:47:44,280 --> 00:47:50,210
mathematics and hacking, but, sure, why
not?
574
00:47:50,210 --> 00:47:58,160
H: And the, I think, final question is
[...] start teaching Haskell in teaching?
575
00:47:58,160 --> 00:48:02,970
M: Well, that's a great question. It kind
of goes, I'm doing a workshop later on
576
00:48:02,970 --> 00:48:07,120
teaching programing. I think teaching
programing using Haskell is a terrible
577
00:48:07,120 --> 00:48:14,510
idea. So obviously, you all know, I'm a
big fan of functional programming. I
578
00:48:14,510 --> 00:48:17,780
actually do a lot of Haskell in my daily
life. and I've given talks using and on
579
00:48:17,780 --> 00:48:21,540
Haskell in the past. But Haskell is a
programing language coming out of the
580
00:48:21,540 --> 00:48:25,250
research community and used for
professional programing. If you really
581
00:48:25,250 --> 00:48:29,170
want to do an effective introduction to
programing, you're well off using
582
00:48:29,170 --> 00:48:33,500
specialized programing languages for
learning. That's what I will advocate
583
00:48:33,500 --> 00:48:39,260
later today at 4pm Middle European Time.
H: OK, thank you. And this concludes the
584
00:48:39,260 --> 00:48:48,460
session, thanks for being here.
M: Thank you. Thanks for having me.
585
00:48:48,460 --> 00:49:06,460
*postroll music*
586
00:49:06,460 --> 00:49:09,020
Subtitles created by c3subtitles.de
in the year 2021. Join, and help us!