eep
-> joined the channel
eep
set the channel purpose: 'ₕₑₗₚ'
eep
@fromankyra maybe u want to be here
fromankyra
-> joined the channel
fromankyra
yuss
fromankyra
itll stop me spamming #random
eep
my first question is
fromankyra
do we wanna invite @sdhand ?
eep
yes lmao he is the only one who has a vague grasp of this dumbass subject
eep
what does this mean
eep
source: 2014/Spr exam
sdhand
-> joined the channel
fromankyra
I think it means that you have to show it for any graph derives from those rules? but idk
eep
hmm i was thinking something in my head but now i think i am wrong and must check things again ugh
sdhand
Henlo
eep
please explain question
eep
mostly i'm confused whether i'm supposed to be able to find something
eep
where H1 r1<= G =>r2 H2
eep
and it's parallelly independent
sdhand
Hold on I'm being taught stuff by Taneb right now
eep
that's okay
eep
do not fret
eep
can taneb teach us grat too
sdhand
I can answer in a bit if it is still makes no sense
eep
i would be v happy
sdhand
@eep ok I'm back
fromankyra
\o/
sdhand
@eep I don't think you need to find anything, given the whole point of the question is to prove this is true for arbitrary graphs
fromankyra
wait, "for each", does that mean that any derivation has to be paralelly independant?
fromankyra
also, how the fuck do you spell parallell
fromankyra
this makes no sense
sdhand
showing it is impossible to construct a derivation H1 r1 <= G => r2 H2 where H1 != H2 that is parallel dependent would work
sdhand
any derivation where H1 != H2 must be parallelly independent
sdhand
can someone post the definition of parallel independence again before I say something silly
fromankyra
that's when you have H1 <-r1 G r2 -> H2 such that H1 r2-> K <-r1 H2 is possible, right?
fromankyra
(imma check, just wanted to try just in case)
fromankyra
@sdhand
fromankyra
oh hey I got it right
sdhand
ok so its the one where the intersection of the left hand sides is a subset of the intersection of the interfaces
fromankyra
wat
fromankyra
ooh ok yes
fromankyra
interfaces are the ones that don't change, right?
sdhand
yup
eep
sdhand
and you only have parallel independence if neither deletes an item used by the other
fromankyra
and you mean that neither left hand side deletes the interface of the other's?
fromankyra
yes, parallell is that one
sdhand
the interface is what isn't deleted
eep
he's only shown us questions where we kinda just give some pair of derivations :(
sdhand
ye but that's not what this question asks right
eep
I don't know what the question wants from me ;_;
sdhand
a proof
sdhand
aight so lets break this down
sdhand
you definitely have parallel independence if both left hand sides match completely different parts of the graph right
sdhand
because then neither application even touches something used by the other
eep
yeah
fromankyra
wait hold on, is the intersection of the interfaces the empty set?
eep
is that allowed
sdhand
ignore that stuff for now
fromankyra
sorry
eep
to just have a graph and ur like the steps are parallel independent bcos they just don't touch
sdhand
I need to think that through cos I'm certain there's a helpful way of thinking about it in there but I need to convince myself my notes work frist
sdhand
@eep the point is that when doing this proof we only need to think about situations where the rules are applied in such a way that the left hand sides match parts of the graph that do overlap
sdhand
so we just take it on a case by case basis
sdhand
so for the start just think about applications of the form H1 r1<= G =>r1 H2
sdhand
how many ways of "overlapping" two applications of r1 are there
eep
that one does make sense I think
eep
there is: 1
sdhand
yup
sdhand
and if you take any application that looks like that does H1 = H2?
eep
yes
eep
and same for R2,R2 because here's only one node in the interface?
sdhand
ignore the interface for now
sdhand
how many ways of "overlapping" applications of r2 are there
eep
umm
eep
1?
sdhand
consider the graph: · -> · -> ·
eep
oh wait I see what u mean
eep
Ye me dumb
sdhand
you could either match the first 2 in that chain
sdhand
or match the second 2
eep
can you not also have .-->.
sdhand
there's also the obvious one where you match the same 2 nodes but that's obviously going to give you H1 = H2
eep
right yea
sdhand
so there's 2 ways of having applications of r2, r2 "overlap"
sdhand
now ignoring the trivial one (literally the same match for both applications) do we have H1 = H2?
eep
err
eep
They look the same
eep
but the numbers will be different
eep
I think that makes them different
sdhand
oh fuck I drew the graph wrong lol · -> · <- · I meant to consider this
eep
wait why
sdhand
numbers being different is fine the graphs are still isomorphic
eep
so is that still h1=H2 if isomorphic
sdhand
you can't apply r2 to · -> · -> · if you match the first 2 nodes in the chain
sdhand
cos of the dangling condition lol
eep
Oh shit ye
eep
I looked at it and was like it is fine
eep
But wrong
sdhand
I forgot which one the interface node was lol helps if I keep the question open
sdhand
ok but there are two ways of having applications of r2 overlap
sdhand
so ignoring me being a moron
eep
Wait don't you mean the arrows pointing outwards
sdhand
... probably
eep
Cos the source is interface and the other one is delet
sdhand
... ye
eep
nice
eep
it okay
sdhand
ugh lemme just open the question in another window so I stop scrolling up and forgetting what it is lol
sdhand
anyway, do both ways of having applications of r2 overlap give you H1 = H2?
eep
They are isomorphic I think so yes¿?
sdhand
they do
sdhand
which means we only need to think about overlapping r1 and r2
sdhand
how many ways of doing that are there?
eep
just .->. ?
sdhand
which node is r1s left hand side matching there?
eep
Where the overlap is the first one
eep
the other one doesn't work bcos dangling
sdhand
yup
sdhand
ok, so does doing those applications give you H1 = H2
eep
no
sdhand
aight
sdhand
so for this we need to show that they are parallel independent
eep
but it doesn't look parallelly independent either
eep
Oh no
sdhand
rugg
sdhand
fugg
sdhand
rug too I guess
eep
do they look p. Independent to u
sdhand
not really
sdhand
cos r1 deletes what r2 has matched
eep
ah
eep
hey well
sdhand
oh wait
sdhand
nah
eep
oh?
sdhand
there's no way of overlapping r1 with r2
eep
Oh
sdhand
cos of the dangllly booiiii
eep
Is .->. Disallowed
eep
which bit dangles wrong
sdhand
yeah cos it has to delete one of those nodes right
sdhand
which is bad
sdhand
cos both of those nodes have edges incident to them
eep
Yes but can't it delete the first one
sdhand
it can't delete either
sdhand
it just can't be applied
sdhand
you can only apply r1 to a lone node
eep
Ohh is not allowed to match
sdhand
cos it doesn't match any edges incident to the node that it matches, and then deletes that node
eep
ahh right ok
sdhand
which is like exactly what the dangling condition says you can't do
eep
I tried to convince myself earlier that it could match
eep
Because I thought there had to be a R1,R2 pair
sdhand
there are plenty of r1,r2 pairs
sdhand
but only matching in separate parts of the graph
sdhand
and we already know that those will be parallel independent
eep
right yeah
eep
I did draw one where they were just separate graphs
eep
and was like hangon,,, if I draw this I will have to draw lots
sdhand
Yeah I think you're allowed to say "clearly if the intersection of the left hand sides is empty then we have parallel independence"
sdhand
probably drop a trivially in there
eep
in his mark schemes it appears detlef likes using "clearly"
sdhand
oh nice
sdhand
use that then
eep
one 100 mark question. draw infinite graphs. go
sdhand
lmao
eep
overall thank you i think i have become more enlightened than before
eep
@sdhand i owe you baked goods of your desire (within reason)
sdhand
I know it was kind of a shit explanation cos I kept getting shit wrong
sdhand
but the basic idea of just doing a casewise proof should work for most questions of that type
eep
honestly if it had been detlef he'd have got everything right but i'd have nodded and understood nothing
eep
i v much appreciate the explanation
sdhand
like just take each possibility in turn and think about where the property you're trying to prove could be false
sdhand
and then prove that it actually turns out to still be true in that case
fromankyra
set the channel topic: 'aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa'
fromankyra
does this mean, choose a morphism where if you apply r to the morphism the dangling condition won't happen?
eep
yes
eep
dangly forbidden
fromankyra
ok that's doable
fromankyra
is there a reason why
r1: .1 => .1 -a-> .
r2: .1 -a-> .2 => .1 --> .2
-->.
r3: .1 -a-> .2 => .1 --> .2 wouldn't be a valid grammar for binary trees?
fromankyra
oh wait, I think I know why, nevermind
davidjn
-> joined the channel
davidjn
ey up
eep
eep
in my hideous quality photo... Am i correct in believing that the critical pair I've shown is joinable but not strongly joinable
sdhand
@eep hey can you post the joinable and strongly joinable definitions
eep
eep
indeed i can @sdhand
sdhand
Ugh remembering Detlef's notation is a pain
sdhand
The easy part is that it is defo joinable lol
sdhand
I'll see if my notes explain strongly joinable in a way that doesn't make me want to die
eep
nice
eep
thank u
sdhand
Lol mine just says "every node and edge ends up mapping to the same thing"
sdhand
So I guess if you trace through from the start what happens to an element in both derivations
sdhand
It should end up in the same place
sdhand
Which that certainly doesn't cos one of them deletes 2 and keeps 3
sdhand
And the other deletes 3 and keeps 2
eep
I think it does not quite
eep
Yes
eep
Oh wait
eep
I think it only matters what the persistent node does (1)
eep
but that does something different because in one side it's got arrows pointing at it and it another it doesn't
eep
I think I managed to find 6 critical pairs
sdhand
Oh yeah it has to persist in both I forgot
sdhand
In that case maybe it is strongly joinable?
sdhand
Cos you can just join it to a graph with 2 nodes, each with one vertex exiting and going to the other node
sdhand
And the only persistent node is 1
sdhand
Actually just ignore me tbh I can't remember how this formally works so I'm trying to do it by intuition and am probably fucking up
eep
eek
eep
yeah I tried to make it into (1) .-->. (2/3) but wasn't sure if that was ok
eep
Because then you are mapping different nodes in the rule to the (1)s on each side
eep
If that makes sense
sdhand
I just made them both into this
eep
oh wait I think that's what I meant
eep
but in the first one we have 1<--3 and in the second it's 1-->2
sdhand
Oh I see
sdhand
Does that matter
eep
Maybe
sdhand
Can you explain the notation in the strongly joinable definition
eep
Wait let me find an example
eep
No
eep
Help
sdhand
@eep I was just like well I can find an isomorphism between the two graphs in which 1 is isomorphic to itself so we good
sdhand
Can you link the slides so I can go through and remind myself how the notation is destined
sdhand
Defined*
eep
Oh wait actually check the Def of strongly join above
eep
And look at that example
eep
sdhand
Ye but that one I can't make 1 isomorphic to itself
sdhand
Oh that example
eep
ye
eep
that's isomorphic right
sdhand
Which example are we talking about
eep
but detlef is like >:( NOT STRONG ENOUGH
eep
eep
Bottom of the slide
sdhand
Yeah that's different
sdhand
The graphs are isomorphic
sdhand
But the isomorphism doesn't assign 1 to 1 and 2 to 2
sdhand
In the question I can construct an isomorphism that assigns 1 (the only persistent node) to 1
sdhand
Yeah I'm pretty sure it is strongly joinable in the question
eep
okay
eep
maybe I understand
sdhand
Does Detlef actually explain how equality is defined on nodes anywhere
eep
I think I just don't really understand what the track morphism bit means
sdhand
Cos that's the actual issue
eep
I don't think so
sdhand
Fucks sake
sdhand
The track morphism literally just maps all the stuff that is maintained by the application to where it ends up after the application
eep
why does he have to say track morphism
eep
why not just "it's isomorphic at the end"
sdhand
Lol
sdhand
Or just "the interface"
eep
makes u ree
sdhand
Cos that's all it does, it identifies the interface in both the start and end graph and maps it to itself
eep
right
sdhand
Ugh but what does he mean when he says "is defined (this bit is fine) and equal "
eep
:grimacing:
eep
maybe I'll send him an email later about that question
sdhand
Ah no wait it identifies more than the interface it identifies everything that's maintained including the stuff that just isn't touched by the rule application
sdhand
Either way
eep
eep brain go whirr
sdhand
I'm gonna go with the isomorphism definition of equality cos imo it's the only way it makes fucking sense
sdhand
If there's an isomorphism f between the two graphs such that for every persistent node v: f(v) = v then you have strong joinability
sdhand
If Detlef says otherwise he can naff off
eep
I'll be sure to tell him so
sdhand
I can't thing of anyway of distinguishing between the persistent nodes in the two end graphs in the question tbh
sdhand
So I can only assume they are equal
eep
detlef says there are 8 critical pairs
eep
I can only think of 6
eep
does he lie
eep
I cannot know
eep
sdhand
oh ye this is classic sometimes you think a pair is the same pair as another
sdhand
but actually it is not
eep
eep
I got as far as these lmao
eep
oh my fucking god i think i managed for the 1st time to actually get a grat question completely correct
eep
@detlef give me 100 marks
fromankyra
"this is obviously the halting problem, but I don't know how to explain that"
fromankyra
ok fine it's the membership problem
davidjn
does the video meeting link actually work for anyone?
fromankyra
@davidjn we just got emailed a new one
davidjn
ye
eep
new one works for me
fromankyra
same
eep
havent joined the call yet cos it would just be me and detlef
fromankyra
but I don't wanna join yet cause it's just^
eep
bit too intimate
fromankyra
@eep heh
fromankyra
wanna join together?
eep
maybe...
eep
shall we at 13:28
eep
oh shit thats now
eep
13:29
fromankyra
29
fromankyra
ok
fromankyra
good timing
eep
"hi both!"
eep
what a cutie
fromankyra
:D
fromankyra
also no one else is speaking
fromankyra
@eep questions
eep
I want him to tell me answers to questions I don't have alldfkdldl
eep
I can't navigate away from that now lol
davidjn
love the big DETLEF
eep
FUCK
davidjn
hahahahahahaha
eep
I am presenting??
davidjn
yes
eep
tell me if anything changes when I move the windows
fromankyra
eep
I'm scared to change the window but I guess all I have to do is listen to him
eep
Jfkdkd at least the massive DETLEF is gone
Slackbot
:crabpls::crabpls::crabpls::crabpls::crabpls::crabpls::crabpls::crabpls::crabpls::crabpls::crabpls:
eep
Slackbot wtf
fromankyra
oops, turns out I don't have a question
fromankyra
i thought I did
fromankyra
rip
eep
This is painful
eep
Someone else please ask a question next
fromankyra
I don't have any! I'm so sorry!
fromankyra
wait maybe
davidjn
desperately trying to find one
fromankyra
im gonna ask about applying r4
davidjn
are we just allowed to ask about the first part of GRAT or would critical pairs be acceptable?
fromankyra
eh, i dont see why not
eep
U asking @fromankyra
eep
Rip to recording my question lmao
fromankyra
yup oops
eep
ahaha
fromankyra
someone else question next
davidjn
eeeeeee
eep
eep
someone do "d) how many isomorphisms are there"
davidjn
which paper?
eep
2011
eep
Can find it in my drive
davidjn
!!!!!
eep
What's those !!! For lol
fromankyra
@eep that's in the first problem sheet I think
fromankyra
or last year's paper
eep
Not g->g I don't think?
eep
But double check if it is
fromankyra
I did g->g somewhere
eep
I can't rn do that easily lol
fromankyra
last year
fromankyra
do you want me to start presenting?
fromankyra
wait its slightly shorter
fromankyra
but mostly the same
eep
Exactly that question last year??
davidjn
currently trying to download slack on my laptop
fromankyra
fromankyra
similar
eep
Am I still sharing
eep
Look at how few nodes
davidjn
9
eep
David ask
eep
9??
davidjn
nein
eep
That's 2019!!
eep
:(
eep
We have answers of that
eep
Sad
eep
Presenting works
eep
Tbf 2x2 is confusing
eep
Lmao detlef
fromankyra
yeah I was confused yesterda
fromankyra
also riiiip I cant mute now
eep
"why did I say that :thinking_face: " - detlef
fromankyra
aaaaaaaaaaaaaaa
davidjn
should I ask?
fromankyra
I've run out of qs
eep
Someone askk
fromankyra
yes
fromankyra
oh nvm
davidjn
sorry
fromankyra
next time I guess
davidjn
I'm not quick enough
fromankyra
you can do it in a couple of weeks
fromankyra
aaaaaaaaaaa
fromankyra
why do I talk so much
davidjn
why do I talk so little
fromankyra
also I have no fucking clue how the recording works shit
eep
thank u for talking @fromankyra
eep
only 4 people spoke
eep
and i really tried to avoid it
davidjn
^^^
davidjn
shout out to my absolute god tier setup
davidjn
made typing in slack difficult
eep
i contemplated sending questions in advance before the thing but was scared he was gonna have a structured thing
eep
and then he just didnt lol
eep
but i didnt ahve loads of questions for the first part anyway
davidjn
yeah, I thought it was going to be highly structured
davidjn
now we know
eep
have a bunch of questions where im like :??? for 2 and 3 lol
fromankyra
how does access recordings of sessions
eep
unfortunately i do not know
eep
maybe someway through a google meet account(??)
eep
idk
eep
like the home page that shows if u just go to meet.google.com
fromankyra
fuuuuck I think by leaving the meeting I fucked it
fromankyra
aaaaa
fromankyra
that feeling when I spend two pages writing a proof for completeness of AC and detlef just....
fromankyra
like dude I went through every rule to show they couldn't introduce a cycle
eep
yea omg he's like that
eep
sometimes hes like i must go through every rule
eep
and other times hes like yeah clearly it works dumbass QED
fromankyra
@eep you've read a bunch of exam questions: what does detlef tend to ask in relation to chomsky grammars, is it just the same type of "prove this is undecideable" questions we got back in COCO days, or does he have "convert this chomsky grammar into a graph grammar"?
eep
uhh
eep
never seen him ask about them at all :)
fromankyra
ooh, neat
fromankyra
tfw the thing you're going through on the problem sheet literally has the answer in the slides
fromankyra
does anyone understand why r1 is not terminating but r2 is? Iike why does r1 not satisfy #G > #H ?
fromankyra
oh fuck, is this a dangling condition thing?
fromankyra
like, because one of the nodes in r2 isn't persistent, it can't have any other edges attached to it
fromankyra
so you can't do the same thing as r1
fromankyra
?
sdhand
Yup
sdhand
You got it
fromankyra
cool, do I need to explain that in an exam, or can I just say "this # expression applies" and not explain why?
fromankyra
I mean, as long as # does apply
fromankyra
also this isn't GRAT but I've written something in CSP for a CSAV past paper, and I really should test if it's equivalent to the answer using fdr
fromankyra
but that would involve getting my other laptop out
eep
@fromankyra possibly should mention it in the exam, but the explanation can probably be as simple as "rule x cannot be applied due to the dangling condition"
eep
don't have to spell out the dangling condition definition
sdhand
@fromankyra just give the # and you should be fine yeah
eep
reminder to think of questions to email detlef
fromankyra
o fuck
fromankyra
I may ask about "what type of question will you ask"
fromankyra
about chomsky grammars
fromankyra
also should we remind luke and the blonds this channel exists?
eep
lol can do
jacob
-> joined the channel
adam
-> joined the channel
Luke Moll
-> joined the channel
fromankyra
the problem is that all of the things I don't get are like
- critical pairs
- local confluence
- paralel and sequential independance
eep
you have been forcibly entered into GRAT
eep
@fromankyra LMAO same
Luke Moll
SCLECT
fromankyra
all of which are the last revision session
eep
i was like "hey i have tons of questions" *checks notes* ...for the next one
fromankyra
is it pushouts this session? I may ask about proving the universal property
eep
yes that is this session
fromankyra
cause I get the comutativity bit but not the universality
eep
for reference, i've asked these specific questions
adam
wow, how did I not notice this channel for a week?
fromankyra
@eep what's wrong with the first one?
fromankyra
but yeah, I may ask him to go over the universal property, like, will we be asked to prove it, and how do we prove it?
eep
@fromankyra nothing in particular i just kinda wanted him to go over pushouts ya know
fromankyra
I guess
eep
i also think i understand the second one but just want to check lol
eep
these ones are mostly for the sake of asking questions but he may tell us something useful or someone may ask something useful which provides better understanding
eep
also ngl what the hell is the universal property @fromankyra
eep
feel like that's just completely slipped my memory
fromankyra
one of the two propeties of pushouts
fromankyra
basically, you have your square, and then you have another graph D', with a function D -> D'
fromankyra
and there are functions from both corners of the square
fromankyra
it's the one when the square gets stretched out basically
eep
oh right yeah
sdhand
I SMELL CATEGORY THEORY
sdhand
I HUNGER
fromankyra
@sdhand pls explain category theory
sdhand
um so there's these arrow things
sdhand
and then
sdhand
eh fuck it i dunno
fromankyra
:oh-no:
fromankyra
how does prove universal property
sdhand
can you give an example question and explain where you're struggling?
fromankyra
example question
fromankyra
I haven't seen any example questions with this
sdhand
ah
fromankyra
just the explanations of pushouts are like "here is property 1 and property 2, x has both properties, so must be a pushout"
fromankyra
and I get the commutativity property
fromankyra
but not the universal property
fromankyra
if that makes sense
fromankyra
worst case I'll email detlef tomorrow
fromankyra
tonight I kinda wanna generate a knitting pattern help
sdhand
the universal property says that whenever you have anything that looks like it could fill the lower right box along with 2 morphisms, you have a unique way of getting that thing + the 2 morphisms from the existing graph in the lower right box
sdhand
it's kind of a "this is the most general solution" style thing
fromankyra
how do you show it's the most general one though?
sdhand
proof by contradiction usually works pretty well for such things
sdhand
as in assume there exists a D' and two morphisms where you don't have a unique morphism from D to D'
sdhand
I think usually when doing pushout stuff it's easier to do the "no junk" and "no " conditions that detlef comes up with tho
fromankyra
ah ok
fromankyra
thanks
fromankyra
when detlef says this, does he mean "such that there is an injective graph morphism", or does none injective work?
eep
@fromankyra which question's that? i vaguely remember it but context might help
fromankyra
@eep concrete graphs, 2010 & 2013
eep
ahh
eep
in the rest of the question he states whether he wants an injective or a non-injective morphism
eep
so i'd take it to mean that he means either in the case of (e)
fromankyra
aaaa
fromankyra
wait actually
fromankyra
if it can be noninjective then it's easy
eep
i think either would be okay
eep
being noninjective i think means more thinking!
fromankyra
all the nodes go to 9
all of the 'B' edges go to the B one
all of the 'A' edges go to the A one
eep
if it had to be injective all you would have to do is draw G and then add like 1 node to it
fromankyra
ooh tru
fromankyra
or an extra edge
eep
indeed!
eep
or simply an isomorphism?
eep
actually yea
eep
an isomorphism is injective
eep
(as well as surjective and therefore bijective obv)
fromankyra
I guess an isomorphism, then you just do the exact thing but relabel the nodes, right?
fromankyra
should we email to ask, or just assume any of these are fine?
eep
ahaha
eep
would we have to relabel the nodes? idk
fromankyra
rename*
eep
hmm something i want to ask is how we should show our "working" for questions like "how many injective graph morphisms are there"
fromankyra
yeah, I kinda ended up doing what he does in his answers
eep
like the one from 2019 he wrote 2 x 2 = 4
eep
lmao
eep
yea
eep
it's not the clearest
eep
writes down random multiplication tables and hopes one is correct
fromankyra
wait no
fromankyra
fromankyra
reminder that we have a GRAT revision session today
adam
Can't revise grat if I never learned it in the first place :roll-safe: :aaaaaaaaaaaa:
eep
a GRAT vision session
fromankyra
@eep wanna join simultaneuosly again? 13:28?
eep
sure
eep
someone want to ask about gp2?
eep
thats not included right...
fromankyra
it shouldnt be
fromankyra
we weren't taught
eep
one hopes
fromankyra
you can ask
eep
im afraid to lol
eep
@Cascades join secret grat channel
Cascades
-> joined the channel
fromankyra
worth noting that he's already written the exam, I haven't asked him any questions
fromankyra
awww, detlef!
fromankyra
the "always forgetting stuff" comment
eep
i have a "would we have questions involving gp2" ready to send but im waiting for him to stop his current train of thought lmao
fromankyra
fair
fromankyra
so what I'm getting is that we'll just have to do proofs analogous to the chomsky proofs
davidjn
had to go afk and now my sound isn't working
eep
boy hes stretching this one now
Luke Moll
@davidjn ono
Luke Moll
check pulseaudio volume control? (pavucontrol-qt)
fromankyra
eyy
fromankyra
I think I asked two questions??
eep
also what was that "ohh samanta" he sounde like he was gonna cri
fromankyra
wait sam did you ask the same question I did?
fromankyra
oh you just asked for exercises ok
eep
i dont think so
eep
i asked some exam questions
fromankyra
and that asks "how does show"
fromankyra
which is no junk, no confusion
eep
yea i did ask a question pushout related like that
fromankyra
which I think has to do wuth universal?
Cascades
Never felt so close to detlef’s face
fromankyra
junk is maybe universal?
fromankyra
@Cascades i am begging of you, don't make this weird
davidjn
@Cascades you've never lived
eep
sad timesss i wanted him to do the exam qhich doesnt have model solutionsnss ssn
davidjn
just feel the comforting touch of those chin bristles
Cascades
@fromankyra i never do!
fromankyra
@eep I think it was literally in the problem sheet though?
fromankyra
@Cascades Cussens.
davidjn
aaah, now it won't let me in at all
Cascades
@davidjn oh, dont i think that every day
eep
oh hang on yea the one in the problem sheet just lacked one of the boxes
eep
i see that now
fromankyra
oooh that explanation was pretty fucken neat
davidjn
wew and now the browser has crashed
fromankyra
he got confused, but did he get
fromankyra
junked
Cascades
@fromankyra cussens called me from bed the other day
Luke Moll
:thinking-guns:
Cascades
Very intimate
fromankyra
@Cascades same, it was odd
davidjn
In bed with James Cussens
davidjn
like a tv show
Cascades
Too confusing
fromankyra
aaaaa rip I dropped out
fromankyra
"at least those that are published"
fromankyra
also dude read the rest of the question before stopping presenting
eep
what was the rest?
eep
i havent been called samantha for a very longe time
fromankyra
didn't you have like two other questions?
Luke Moll
@eep change your google name to eep
eep
yeah hes showing them now ?
fromankyra
you were called samantha last thursday!
Luke Moll
a week is a very longe time
eep
before then i havent been called samantha for a very long time
Luke Moll
@fromankyra if you're gonna quote me, don't add words
fromankyra
oh i misread
fromankyra
apologies
Luke Moll
np :detlef:
fromankyra
oooh that's a good question epp
eep
why did he not look at the questions beforehand lmao detlef
eep
i think the answer is that it can be extended in any way
eep
but i may be wrong
fromankyra
I would guess so
eep
hence my asking
fromankyra
because the thing never deletes any nodes
fromankyra
so danglyboi doesn't apply
eep
detlef: german mumbling
fromankyra
how is that german
eep
accent
eep
my question broke his computer
eep
sorry detlef
fromankyra
:piece_of_crap:
eep
heck
Luke Moll
run rm -rf / --no-perserve-root
Luke Moll
@fromankyra more likely: linux is good software
eep
detlef is holding that position very well
Luke Moll
@eep he's so still isn't he
eep
aww he left
fromankyra
detlef plump has left the meeting
eep
fromankyra
rip
Luke Moll
bahaha now I'm just left with wonky georg
fromankyra
how does wonky?
Luke Moll
uhh
eep
someone else left besides detlef
eep
who
fromankyra
huh
fromankyra
I wanna say Tom somethingorother
fromankyra
I'm sure there was someone called Tom in here earlier
eep
he back
Luke Moll
@fromankyra the rule is img {transform: rotate(15deg);} but idk a good way to add it without much fiddlying
Luke Moll
somewhere in devtools but that depends on browser
fromankyra
bleh, I do not care that much
fromankyra
@eep we were right I think
eep
why would you prefer not to answer it directly........................................
fromankyra
rip
eep
:eyes: :fasteyes:
fromankyra
oof eep
fromankyra
I don't think detlef got my joke
Luke Moll
Might not have seen/parsed :P
fromankyra
Is confluence basically parallel independence, but over the whole rule system rather than a single rule?
eep
i...cant remember
eep
i dont think so quite
eep
you can have a confluent system which also has critical pairs
eep
(i think?)
fromankyra
I still don't get what critical pairs are
eep
but all those critical pairs gotta be strongly joinable or sommat
eep
wew
fromankyra
I'm going over all those slides again
fromankyra
trying to understand
eep
a critical pair is like T1 <= S => T2
eep
where S is created by overlapping LHS of two rules (possibly the same rule) in the system
fromankyra
a lot of things are like T1 <= S => T2
eep
the overlapping S can ONLY consist of the LHS of the rules, and the overlapping must be NOT parallelly independent
fromankyra
LHS?
eep
left hand side
fromankyra
oh ok
fromankyra
eh, I'm going to go over the slides
fromankyra
and I'll see if I get it this time
fromankyra
ah ok so if every pair is parallelly independent, that's strong confluence
fromankyra
and confluence is strong confluence but with, like
fromankyra
more wiggle room
eep
wiggly confluence
fromankyra
aaa dude you can't just say that
fromankyra
so strong confluence is you have no critical pairs (because either every rule is parallelly independent)
fromankyra
but if you have critical pairs and they're strongly joinable then you have confluence
fromankyra
or g1 == g2??
eep
eep
probably the best diagram detlefs done
fromankyra
I think I understand most of that now
fromankyra
I'm still vaguely confused as to what strongly joinable is
sdhand
do you know what is confusing you about it?
fromankyra
So I get that to prove strong joinability, you have to do something with persists
fromankyra
but I don't get what
fromankyra
like detlef just lists the persists set, and then says "it's strongly joinable" or "it's not strongly joinable" and I have no idea where he's coming from
sdhand
I think it's just that the persist sets for both rewrite "routes" has to be the same
sdhand
cos the whole point of strongly joinable is that every node and edge ends up mapped to exactly the same thing no matter which route you take
fromankyra
are they not the same here?
sdhand
I don't know what the rule set is, so I have no idea :stuck_out_tongue_winking_eye:
fromankyra
EFD, just a sec
sdhand
it sounds like there the "strongly" part doesn't even come into it
sdhand
and there's just no way of multi-step rewriting the left and right graphs to both be the same thing
fromankyra
fromankyra
so that ^-1
fromankyra
ah wait I might have it
fromankyra
is it just that you can't apply anything to the left hand one?
sdhand
I think you can apply dec2^-1
sdhand
but then from that point you can't proceed any further
fromankyra
no
fromankyra
cause node 3 isn't there
fromankyra
(node 3 in the rule I mean)
fromankyra
o wait
sdhand
I think in this case node 3 and node 1 are the same thing
sdhand
or does the matching morphism have to be injective I don't remember?
fromankyra
yeah oops
sdhand
I don't think it does though, cos that seems to be exactly what happens in the application of dec2^-1 in the slide
fromankyra
yeah, you're right
sdhand
but yeah after you apply that you get to a point where you can't go any further, and there's no way of rewriting the right graph to that same thing
sdhand
so it's not just not strongly joinable
sdhand
it's not joinable at all
fromankyra
ah ok
fromankyra
to prove that, do I just have to
show that the only derivation is rx, and so forth?
sdhand
Yeah it's kind of just "state why" usually
sdhand
As in "only these rules can be applied to the left graph, and only these to the right, at no point will you end up with the same result because..."
sdhand
Remember that in can still be joinable (and also strongly joinable) if no rules can be applied to one of the graphs
sdhand
It just means that the other graph has to have a way of being multi step derived to the graph to which no rules apply
fromankyra
let's do this
fromankyra
sequential independance is G r1=> H1 r2=> H2 and G r2=> K r1 => H2 right?
fromankyra
the fuck
eep
that looks right to me i think
fromankyra
and then parallel is G r1=> H1 => K and G r2=> H2 => K
fromankyra
correct?
fromankyra
So I guess what I'm gonna ask Detlef is "you can't have something that is sequentially independent without it also being parallelly independent, right?"
fromankyra
or can pls have example if not
fromankyra
oh nvm
fromankyra
there's an answer in the slides
eep
:D
fromankyra
!:D it means I don't have questions!
fromankyra
i mean i do but
eep
theres one critical pair question in past papers i fund
eep
found*
eep
that really pisses me off cos it says theres 8 pairs and i can only find 6 lmao
eep
ill find it later
fromankyra
are you gonna give an exam question with strong joinability ooi?
fromankyra
I wanna ask but I don't have the energy to find a specific exam question unless you aren't already doing it
eep
most questions have strong joinability
eep
i want to ask about joinable but not strongly joinable stuff
eep
idk if theres any specific exam questions
fromankyra
yeah, joinable but not strongly was what I was wondering about
eep
forgot to email him any questions lmao
fromankyra
i'm sure if you send them today he won't mind
fromankyra
and sign them samantha
eep
idk what to ask anyway cos i dont think he likes go through past questions
eep
ill just ask in the chat about more examples of joinable (but not strongly joinable) pairs
eep
and hope he doesnt just show us the slide with 1 fucking example on
sdhand
What's up re: strongly vs not
eep
idk i think i just confuse em a bit
eep
i kinda should reread slides again but i am currently distracted by other matters
eep
sad times
sdhand
they are basically the same
sdhand
just strongly joinable doesn't just require that shit gets joined to the same graph
sdhand
both routes have to map every vertex and edge from the start to the same vertex and edge at the end
fromankyra
hey @sdhand you alive? Can u confirm thing for me?
So Noetherian induction shows that in a grammar L with a terminating rule set r, and a property over the derivation G =>r H where H is a normal form, the properties applies to all derivations in L?
and an example of such a property is local confluence? which means that all derivations being locally confluent, the graph is generally confluent?
fromankyra
also wow I really feel guilty about not being there, cause I would have had questions and he was like "does that make sense"?
fromankyra
oh rip @eep did he just like go over that single slide again?
eep
for strong joinability n stuff?
eep
but yea
eep
i think i do understand it maybe better anyway
eep
idk i will actually have to look at some examples from past papers/questions and see if it makes any more sense
fromankyra
oh, wait, is what he's saying that
"joinable" is when you can find a derivation between the two elements of the critical pair
but "strongly joinable" is you can find a derivation when you apply the rules to any graph that has the LHS as a subgraph?
eep
err
eep
maybe
eep
thats kinda what hes saying with the extra edgy bois right
fromankyra
I think so?
fromankyra
and also that the persistent nodes have to have the same edges in and outgoing?
fromankyra
also I do not know how I feel about the fact that I've learned everything I know in this entire module since the end of last term
eep
bhahahaa
eep
big mood
fromankyra
I expect you all will have ninety percent plus
eep
YEAH AHHA A
eep
detlef ur faith in us is sweet and so misguided
fromankyra
hey detlef more people are taking this module than eep and jacob
eep
can u imagine if we were having to learn gp2 rn too
fromankyra
aaaaaaaa
fromankyra
no
fromankyra
kill
eep
thank god it is gone
Slackbot
:crabpls::crabpls::crabpls::crabpls::crabpls::crabpls::crabpls::crabpls::crabpls::crabpls::crabpls:
fromankyra
like, the only reason I've got any degree of confidence that I can surpass my safety net is that I only have two exams to revise for
eep
GRAT and DART rght
fromankyra
GRAT and CSAV
eep
oh yea u have 3 but u dont count DART
fromankyra
I'm not revising for DART, given it's literally all bookwork and algorithm application
fromankyra
@eep yeah
eep
they did say rip in kill bookwork
fromankyra
given he's not sent out another sample paper, I expect that means he's not actually changing the exam any though
eep
true
eep
stefano hasnt communicated with us at all abt icpa so i assume thats also staying the same
eep
if it isnt i will murder him or something
fromankyra
I believe the goss on icpa is that it's not bookwork cause it's algorithm application
fromankyra
but I'm not 100%
fromankyra
imagine having both DART and ICPA, the dream
fromankyra
although the people who I know have this also have EMBS, so maybe not the dream
sdhand
@fromankyra I have no idea about Noetherian induction, sorry
sdhand
I'm not sure why it's in the course really
fromankyra
fromankyra
:detlef: <3
sdhand
ahahha that's a classic slide
eep
eep
theres like not much i can do here right
eep
just H <= r1 G => r1 H and H <= r2 G => r2 H?
eep
for which H = H
eep
it feels wrong that's 12 marks??
fromankyra
have you doen H<=r2 G =>r1 H?
fromankyra
presumably that's slightly more complicated
eep
is that possible?
fromankyra
well, H1 <=r1Gr2=> H2
fromankyra
why wouldn't sit be
eep
hm like
eep
it is
eep
but it would have to be parallelly independent
eep
but like
fromankyra
thats the question??
eep
infinitely many parallelly independent
eep
how do i
eep
show ? that
fromankyra
can u show it for an arbitrary G
fromankyra
that if you apply the rules to it then its parallely independent
fromankyra
I can try and do it after donner if you want
fromankyra
try showing applying r1 wouldnt delet anything r2 needs
fromankyra
and vice versa
eep
mayeb
fromankyra
so I have this already for H1 <=rx G rx=> H2
fromankyra
sorry the picture is crap, just a sec
fromankyra
fromankyra
and the second bit. you'll want to double check cause I don't have the slides open
fromankyra
but I think this is right, and is a whole lotta writing, which justifies 12 marks
fromankyra
^ @eep
eep
that does make sense why it would be 12 marks
fromankyra
can you double check if the answer makes sense? or sam? I am genuinely curious now
eep
all i can think about is neils fucking email and how to say no in a way that isnt just NO
fromankyra
:(
eep
whys he phrased it like that as well? the "likely uptake"? am i allowed to just not do 60 credits? fucking dumb
fromankyra
it might be optional? like you can do modules from 3rd year/other degrees instead?
fromankyra
fuck I just had a sudden doubt
fromankyra
you know the property of, for parallel independance, that it's not parallely independent if one rule deletes something on the left hand side of the other
fromankyra
is that only "it's not parallely independent if" or is it also "it's parallely independent if not"?
fromankyra
aaa
fromankyra
why do none of the parallel independence questions have answers
fromankyra
@sdhand you might know
fromankyra
or is it email :detlef: time
fromankyra
cause all my parallel independence proofs rely on that property
eep
ye this is annoying lmao
fromankyra
can I say incident instead of incoming/outgoing? (for edges, I mean)
eep
if it doesnt matter that it's in/out then sure
fromankyra
ye it's like "given the LHS is just a single node and the interface just :delet: s it, it can't have any incident edges cause that would cause the danglyboi"
fromankyra
has emailed detlef
fromankyra
You could use this property. Parallel independence and parallel dependence are complementary.
fromankyra
w00t
fromankyra
time to see if I still understand critical pairs
fromankyra
(probably not)
fromankyra
ok wow not at all
fromankyra
I found six things I thought were critical pairs but none of them are in the answer paper
fromankyra
I'm so confused
eep
massive oof
eep
yeah there's a particular critical pair question that is bugging me i might find it later... asks for 8 critical pairs, i'm pretty sure of 4 of them being right, but the other 4 i'm like... are u right tho
fromankyra
@eep 2015?
eep
yes
fromankyra
hey @jacob did you say yesterday you had mark schemes for 2015?
eep
markschemes for 2015???
jacob
I think so
eep
how
jacob
VLE magic
eep
???
eep
you only have mark schemes for 2015 or more ??
jacob
I think 2015 is the oldest
eep
pls may i hab
fromankyra
@eep o/ do you have the answer for the 2017 critical pairs question?
eep
yes
fromankyra
would you mind sharing it? I can't figure out any of the r1/r3 pairs
eep
yes
eep
as in
eep
no
eep
but yes
eep
i have done it
fromankyra
@eep thank yoou
eep
question
eep
answer
eep
how come there aren't more pairs like the one in (b), with persistent node {2} and {3}?
eep
makes me thonks >:'(
fromankyra
oh hey that was the one I did the other day
fromankyra
where I found six pairs which I thought were critical pairs
fromankyra
and it turns out they weren't
eep
(screaming)
eep
i'm happy to accept all those 6 are critical pairs
eep
i just think there's 2 more?
fromankyra
@eep at a guess, the other critical pairs are isomorphic to those ones
eep
if you take a look at hmm
eep
the crit pair question in practical 9
eep
you'll see that the 2nd, 3rd, and 4th critical pairs are very similar
eep
which is why i was expecting (b) to have similar counterparts in this question
eep
(this is a forbidden markscheme so if I email detlef I'm just gonna be like "I found 8 but it says 6")
fromankyra
forbidden markscheme
eep
another one:
eep
eep
i can only find 6 of the fuckers
fromankyra
try combining nodes?
eep
in what way @fromankyra ?
fromankyra
1.->.2->.4/3
fromankyra
with a loop on 2/3
fromankyra
idk if it'll work though
eep
hmmm
eep
i literally can't think of anything else
eep
maybe that is allowed
fromankyra
see edit, sorry
eep
ahah
eep
that's
eep
confused me more
eep
is 1 . -> 2 . -> 4/3 supposed to be S?
fromankyra
sorry
fromankyra
yes
eep
like the middle one
eep
what does -> mean pointing to 4/3
eep
wait like
eep
-<
eep
a stick body
fromankyra
fromankyra
does this make sense
fromankyra
idk if it actually works
eep
eep
I think this might work
fromankyra
ooh nice!
fromankyra
oh rip sorry
eep
ahah what for
eep
Its hard to say a bit, because it depends how many critical pairs, and also whether it's a year with 1 paper or 2 papers
fromankyra
you've got ICPA now right? or did I misremember what exams you had
fromankyra
hmm, I wonder if, when we found extra "critical pairs", the issue was that it wasn't a critical pair cause it was parallelly independant?
eep
the extra critical pairs i found weren't parallelly independent im pretty sure
eep
i whacked an email at detlef hopefully herr senpai replies me
fromankyra
herr senpai zomg
fromankyra
gaaaaah I'm still lost why tf is this not parallelly independent
fromankyra
like, surely you can apply r2^-1 to bot
fromankyra
and end up with the same graph
fromankyra
fromankyra
oh is it that when they're isomorphic then it doesn't count as parallelly independent?
eep
no - it's like
eep
so on the left hand side, the rule matches to the top two S nodes
eep
and on the right hand side the rule matches to the bottom two S nodes
eep
applying the rule either way deletes part of the "match" of the other rule
fromankyra
oh ok
Luke Moll
I should probably do a slack export so I can read through the history of #grat
Luke Moll
Although the images people have posted will get slackdd
fromankyra
I think there were plans to do one right before the embargo begins
sdhand
post the definition of parallel independence again?
sdhand
oh nvm
sdhand
I was scrolled up and it was worked out
eep
oh yea detlef confirmed for me yesterday: there are 8 critical pairs lol
eep
dont do that in our exam this time round detlef thanks
fromankyra
I'm somewhat worried that on saturday I'll just be, like, "I don't wanna"
eep
eep
@fromankyra i dunno exactly how to explain my issue with this
eep
i was just confused to see that he was talking about D3 -> D3 rather than comparing D3 to the correct pushout (D2)
fromankyra
I think
fromankyra
ok, so, what it looks like is
- the edge 1 -> 2, because it exists in A, and thus both B and C, needs to map to something unique in Di
- however, as there are 2 of those edges in D3, from both B and C, you can have a morphism that applies to either edge
fromankyra
so you could have a morphism from {C, B} to D3, and a morphism from D3 to D3 which isn't isomorphism
fromankyra
does that make sense?
eep
i think so maybe
eep
let me throw something else in here
eep
a different question
eep
why does he look at D3 --> D2 this time
eep
oh actually... in the first one, there is a unique morphism from D3 to D2 isn't there
eep
so that's why i cant use it there right
fromankyra
at a guess, but I'm really not sure: when he was doing the first one you sent, he was looking at the commutativity property: because the pushout has to be commutative, show that the transformation to D3 isn't.
In the second one, he's looking at the universal property: ie, if you have a thing that fits the pushout, all other things that fit the pushout need to have a direct morphism to each other. Because we know D2 fits, by showing that there isn't a unique morphism D2 -> D3, we show that D3 doesn't fit
fromankyra
^^^ basically yes
eep
hmm i think i understand
eep
i admit i havent really looked at these questions overly carefully
eep
i was like "the answers look more or less the same every time i can just swap in and out the right numbers on the Ds right :^) "
fromankyra
I hope my explanation makes sense, I think that's the reason given what I understand about pushouts
eep
thank u
eep
also maybe #grat @Luke Moll :)
Luke Moll
nah #grat is for the smart questions ((:
eep
:'(
Luke Moll
dumb/confirmation question
Can you delete only edges, so instead of the following you could have K preserving 3 and R adding 5 and 3->5 and 5->2? This would mean that you could match L against graphs with *->3 w/o violating danglo
eep
yeah you can delete only edges
eep
as in the example you suggested
Luke Moll
sweet
Luke Moll
what do the arrows K->L and K->R actually mean
Luke Moll
like there's a different style for morphisms and rule application
fromankyra
I think it's just different ways of representing it? like how you can represent a function as
x \belong \Real, @ f(x) = x^2
or
\Real \arrow \Real; x \mapsto x^2
(sorry for latex speech, I've no idea how to represent these in ascii)
adam
So... what's GRAT?
Luke Moll
Kinda just a confirmation thing but does this make sense?
Luke Moll
(not super important q if people have important things)
fromankyra
yeah, that looks right
Luke Moll
yeet :)
Luke Moll
okay quick aside if I'd just watched the lecture for 5 more seconds I would have seen detlef's diagram that illustrates that but I'm happy I did it
eep
@Luke Moll lmao im on the fire alarm lecture
Luke Moll
@eep coffee time
eep
classic detlef
Luke Moll
I thought you meant the jaem one and I was like eep.no
eep
just taking the fucking mug right out of rch
eep
ahahah
eep
"what do u mean its not MAIG tomorrow"
fromankyra
@eep were you there with us when jacob was like
fromankyra
"hey people are going back in, are we doing the lecture?"
eep
yes i was
fromankyra
also why do we have a #grat channel and literally nothing else?
Luke Moll
Cause there were so many grat questions I think
eep
yeah and people were complaining about me asking questions in #politics
eep
(smh)
fromankyra
oh yeaaah
adam
i was fine to keep #politics as #grat
adam
but people are nerds
fromankyra
hayashi specifically, I believ
adam
fun fact: grat painful
adam
my degree partially depends on understanding the strange ramblings of a mad german
sdhand
Politics: dumb, gross, depressing
Grat: nodes! edges! detlef!
sdhand
how could you not want the latter
adam
because i ain't edgy enough for it
adam
:thinking-guns:
sdhand
n i c e
eep
one of my favourite detlef quotes
eep
"so what do you think - i don't know if you think -"
Luke Moll
Do we have to know the bits in the warning abstract maths bit
fromankyra
you need to be able to fill in a pushout
fromankyra
you do not necessarily need to be able to fully understand what a pushout is
Luke Moll
ahkay
Luke Moll
detlef points so much
Luke Moll
which of course is not recorded
eep
big screm
Luke Moll
Morneep
eep
:aaaaaaaaaaaa:
fromankyra
btw @Luke Moll did you want to do an export?
Luke Moll
uhh sure
Luke Moll
i'm trying to find it now lmao