1
Hoofdstuk 1: Basis Proces Algebra
Hoofdstuk 1 BPA Basis Proces Algebra
1.0.
Inleiding
Wat is een proces? Een proces is iets dat voortgaat, verloopt, met stappen in de tijd. Processen komen overal in het dagelijks leven voor: in de rechtsspraak, in de industrie, en in de informatica. Net zoals je kunt rekenen met getallen in de algebra, of met logische uitspraken in de
logica,
kun
je
ook
rekenen
met
processen.
Zo’n
rekenmethode
voor
processen,
procesalgebra genaamd, is ongeveer 20 jaar geleden ontwikkeld, door onder andere de engelse on-
derzoekers Hoare en Milner. Beiden
hebben
voor
hun
werk
de
Turing Award gekregen, de ‘Nobelprijs voor informatica’. Procesalgebra
is in de ja-
ren 60 begonnen als automaten-
theorie, een onderdeel van ‘For-
mele Talen’. Ruwweg is een automaat iets dat in verschillende toe-
standen kan verkeren, en acties
Robin Milner
Tony Hoare
kan doen om van de ene in de andere toestand te komen. Een automaat kan daarmee ook gezien worden als een proces. De acties zijn hier nog onderling onafhankelijk. In de jaren 70 kwam de
noodzaak op om ook communicatie tussen acties te beschrijven; het trefwoord hierbij is ‘concurrency’. Systemen zijn nu niet langer op zichzelf staand, maar ‘interactief’ of ‘reactief’.
De belangrijkste calculi voor dergelijke systemen of procesen zijn CSP (Communicating Sequential Processes) van Hoare, en CCS (Calculus of Communicating Systems) van Milner.
Begin jaren 80 is een variant van deze formele systemen ontstaan die ACP heet, Algebra of Communicating Processes. In dit eerste hoofdstuk behandelen we de kern van ACP, Basis Proces algebra (BPA).
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
2
Hoofdstuk 1: Basis Proces Algebra
1.1.
Atomaire
processen.
Net zoals strings (woorden) gevormd worden door letters uit een alfabet, worden processen opgebouwd uit atomaire processen, die niet verder te ontleden zijn. We geven die atomaire
processen, ook wel ‘acties’ of ‘stappen’ of ‘events’ (gebeurtenissen) genoemd, vaak aan met letters a,b,c,... Wat die acties precies zijn, hangt af van de toepassing.
1.1.1.
V O O R B E E L D . Gegeven is een bord met 5 maal 5
vakjes. We willen de beweging van de zwarte stip (
) over
het bord beschrijven. De acties zijn: up, down, left, right, afgekort als, u, d, l, r. Het
na
elkaar
doen
van
acties
geven
we
aan
als
vermenigvuldiging. Zo is r.r.r de beweging die bestaat uit 3
stappen naar rechts; en r.r.r.u.u.u is een beweging van de punt naar het grijze veld. Vaak laten we de ‘punt’ weg, zodat
het laatste ‘bewegingsproces’ is: rrruuu. Een andere manier
Figuur 1.1
om op het grijze veld te komen is rururu. We gebruiken ook
exponenten, net als in gewone algebra, en kunnen dan voor de laatste twee processen schrijven: 3
3
3
r u , respectievelijk (ru) .
1.1.2. OPGAVE. Hoeveel manieren zijn er om met de acties u,d,l,r de stip naar het grijze veld te brengen? En als alleen de acties u en r gebruikt mogen worden?
1.2. Samengestelde
processen.
Boven hebben we al gezien hoe uit atomaire processen (acties) processen kunnen worden
samengesteld door de operatie “.”, vermenigvuldiging, ook wel ‘sequentiële compositie’ genoemd, omdat het een sequentie van acties maakt.
Er zijn nog andere operaties om processen op te bouwen. De eerste andere operatie is
met de “+”, som, ook wel ‘alternatieve compositie’ genoemd. Bijvoorbeeld in de situatie van Figuur 1.1 staat r
3
u
3
+ (ru)
3
voor het proces dat òf r
3
u
3
doet,
3
òf (ru) . Er wordt dan dus een
keuze gemaakt tussen beide alternatieven.
1.2.1. VOORBEELD. We bepalen het proces dat de beweging(en) beschrijft van de stip naar het
grijze veld op het 2-bij-3 bord als in Figuur 1.2.1(a), met alleen u en r acties. In de vakjes zijn
de ‘tussen-processen’ al ingevuld. Het gevraagde proces is dus r(ru + ur) + urr. Merk op dat in
deze ‘procesterm’ in één uitdrukking verschillende mogelijke procesverlopen weergegeven zijn.
Als we alleen in de feitelijke executies (procesverlopen) geïnteresseerd zijn, moeten we
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
3
Hoofdstuk 1: Basis Proces Algebra
bij
elke
+
een
keuze
maken; we krijgen dan
een “trace” of executie.
rr
Dit proces heeft dus 3
r
traces; rru, rur en urr.
r(ru+ur) + urr
1.2.1.OPGAVE. Zie het 3-
ru + ur
u
bij-3 bord in Figuur 1.2.1(b). (i)
Bepaal
dat
de
naar
het
bewegingen
proces van
(a)
beschrijft, met alleen
(b) Figuur 1.2.1
u en r acties.
(ii)
Geefde afzonderlijke traces.
Met de + en de . hebben we de basis-operaties om samengestelde processen te maken
uit de elementaire acties. Processen die alleen opgebouwd zijn uit atomen met + en ., heten basis procestermen. Er gelden voor + en . enkele wetten net als in gewone algebra. Deze staan in Tabel 1.1. Sommige van deze wetten zijn letterlijk hetzelfde als in gewone algebra, - maar de wet
x + x = x is nieuw, en betekent dat de keuze tussen proces x doen of proces x doen
hetzelfde is als proces x doen.
Merk ook op dat de “.” hier niet commutatief is, zoals in gewone algebra; het proces ur
is verschillend van ru, de volgorde van de acties doet er toe. Wel is u + r = r + u.
(A1)
x + y = y + x
(commutativiteit)
(A2)
x + (y + z) = (x + y) + z
(associativiteit)
(A3)
x + x = x
(idempotentie)
(A4)
(x + y) . z = x.z + y.z
(rechtsdistributiviteit)
(A5
x.(y.z) = (x.y).z
(associativiteit)
Table 1.1: BPA
1.2.3. OPGAVE.
Show that (a + b)
3
= a(a(a + b) + b(a + b)) + b(a(a + b) + b(a + b)).
1.2.4. NOTATIE.
om het gebruik van haakjes te beperken schrijven we bijvoorbeeld a.b.c in plaats van
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
4
Hoofdstuk 1: Basis Proces Algebra
(a.b).c;
de . bindt sterker dan de +, dus (a.b) + c schrijven we als a.b + c;
buitenste haakjes worden weggelaten;
de . wordt vaak weggelaten, net als in ‘gewone’ algebra, dus in plaats van a.b + c schrijven
we ab + c.
1.2.5. OPMERKING. We hebben niet algemeen z (x + y) = zx + zy, met als instantiatie bijvoorbeeld a(b + c)
= ab + ac. De reden is dat de ‘timing’ van de keuzemomenten verschillend is: in a(b + c) wordt na de a-actie pas voor b of c gekozen; in ab + ac wordt voor de a-actie, al meteen bij het begin, gekozen. Dit verschil in timing
van keuzes is belangrijk wanneer er communicatie tussen acties in het spel is, zoals in een later hoofdstuk. Dat
de vergelijking a(b + c) = ab + ac dan onwenselijk is, wordt dan precies gemaakt. Intuitief kunnen we het verschil tussen a(b + c) en ab + ac nu al inzien, bijvoorbeeld als volgt: automaten, K1 en K2.
Figuur 1 toont twee koffie-
K1 werkt zo: na inworp van 1 euro kan op de
knop K (koffie) gedrukt worden, of op T voor thee.
Als dit er is, volgt uitgifte van het gewenste artikel.
K
T
K
T
Als beide artikelen op zijn, gebeurt er niets.
K 2 werkt zo: Hier moet men van te voren
K1
kiezen voor koffie of thee; als het er is, volgt uitgifte,
K2
anders gebeurt er niets. Als de reservoirs altijd goed
gevuld zijn, is er geen verschil tussen K 1 en K2 . (Als ze altijd leeg zijn, ook niet.) Maar als ze soms vol, soms leeg zijn, is er wel verschil. Bij K1 kunnen we na weigering van knop K nog proberen thee te nemen. Maar bij
K2 zijn we na weigering van knop K onze euro kwijt. Dus:
1.3.
Procesgrafen.
‘procesalgebra’, procesgrafen.
In
deze
bestaande
uit
sectie
inworp.(K + T) ≠ inworp.K + inworp.T.
behandelen
procesgrafen,
of
we
een
preciezer,
BPA,
een
equivalentieklassen
van
model
voor
1.3.1. D EFINITIE. Laat A een verzameling atomaire acties zijn. Een procesgraaf over A is een drietal (N, E, r) zodat: N is een verzameling van elementen die we punten of knopen noemen; E is een verzameling gelabelde pijlen; dat wil zeggen: E
N x A x N. Om aan te geven dat
een element (s, a, t) in E zit, gebruiken we de notatie s → a t. Gelabelde pijlen heten ook transities. r ∈ N is een bijzondere knoop, die we de wortel noemen. Een knoop heet een eindknoop als er geen pijlen uit vertrekken. We zullen altijd samenhangende procesgrafen beschouwen, dat wil zeggen dat elk punt vanuit de wortel bereikbaar moet zijn. De graaf mag dus geen ‘loshangende’ stukken bevatten.
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
5
Hoofdstuk 1: Basis Proces Algebra
(Als in de loop van een constructie op grafen toch onbereikbare delen ontstaan, halen we deze meteen weg. Het verwijderen van onbereikbare delen heet ‘garbage collection’.
Een procesgraaf heet cyclisch als hij een lus (of ‘cykel’)
bevat (dat wil zeggen dat vanuit
een knoop in een aantal stappen dezelfde knoop weer te bereiken valt), anders acyclisch. Een punt heet cyclisch als het op een cykel ligt. Een eindigsplitsende graaf is een graaf, waarbij uit elke knoop slechts eindig veel zijden uitgaan. Een eindige graaf
(i)
bevat slechts eindig veel knopen en zijden. Een een
graaf
waarin
acyclisch
nooit
twee
samenkomen; als
er
p r o c e s b o o m is
die
naar
anders
iedere
is
a
a
en
zijden
b
b
gezegd,
knoop
(ii) a
a
a
b
c
(iii)
b
(iv) a
c
b
a
b
c
a
a
b
een
uniek pad is vanuit de wortel. De procesgraaf bestaande uit alleen
een
wortel,
en
geen
pijlen, heet triviaal. Procesgrafen kunnen oneindig zijn, en oneindige vertakkingen vertonen.
(v)
(vi) a
b
a
b
a
b
(vii) a
a
a
a
a
a
a
a
a
a a
1.3.2. VOORBEELDEN.
1.3.3. VOORBEELD . Het volgend voorbeeld van een procesgraaf, in Figuur 1.3, geeft het procesgedrag van een Stack, waarop data elementen 0 en 1 gezet kunnen worden. De actie 0 wil zeggen: plaats een 0 op de stack; idem voor 1. Met andere woorden: push 0, push 1. De onderlijnde acties 0 en 1 betekenen: pop 0, pop 1 (haal 0 van de stack, resp. 1). We zullen later zien hoe dit proces gespecificeerd kan worden met recursievergelijkingen.
1.4.
Het
graafmodel.
We zullen nu van deze verzameling procesgrafen een model maken van de theorie BPA.
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
6
Hoofdstuk 1: Basis Proces Algebra
1.4.1.
DE F I N I T I E .
Gegeven
een
alphabet A van atomaire acties, is
sta ck
G(A) de verzameling van alle niet-
triviale procesgrafen over A waarvan
0
de wortel acyclisch is. 0
1.4.2. DEFINITIE.Op G(A) definieren we operaties ‘som’ en ‘product’ als
0
volgt. Zij g1, g2 ∈ G(A). De
g1 , + +
som
g2
0
1
0
0
1
1
1
1
1
0
0
1
0
1
0
1
0
1
0
1
1
wordt
gedefinieerd als de graaf die ontstaat door de wortels van g 1 en g 2 met elkaar te identificeren. Het product g 1
..
terminating
sta ck
0
g2 van g1 en g2
0
ontstaat door g2 vast te plakken aan alle
eindknopen
wordt
steeds
van
de
geïdentificeerd
g1 .
wortel
met
de
Daarbij van
g2
betreffende
0
0
0
1
0 1
1 0
1
0
1
1 0
1
0 1
1
1
0 0
1
1
eindknoop van g1.
1.4.3. VOORBEELD. Zie Figuur 1.6.
1.4.4. D ISCUSSIE . Waarom bevat G(A) alleen de grafen met acyclische wortel? Dit lijkt vreemd, omdat
daarmee interessante en nuttige procesgrafen als die van Stack in Figuur 1.5 uitgesloten zijn. Dit is gedaan vanwege het volgende probleem. Beschouw grafen g1, g2 als in Figuur 1.7.
Als we deze optellen zoals gedefinieerd voor G(A), door de wortels te identificeren, krijgen we g3. Maar als we
g1 eerst ‘uitrollen’ tot de graaf h1 die oneindig veel a-stappen doet, en idem g2 tot h2 die oneindig veel b-stappen
doet, en dan h1, h2 optellen, krijgen we h3. Duidelijk is dat g3 en h3 zeer verschillend zijn wat betreft mogelijke
paden: in g 3 is een pad dat bijv. afwiselend een a-stap en en b-stap doet, maar in h 3 niet. Toch is h 3 de
‘bedoeling’, want cyclische grafen zijn eigenlijke een verkorte versie van hun ‘unwinding’. Als we toch root-
cyclische grafen willen optellen, moeten we eerst een klein stukje de graaf uitrollen (‘unwinding’), zodat de root acyclisch wordt. Dit gebeurt als volgt.
1.4.5. DEFINITIE. Zij g = (N, E, r) een procesgraaf, niet noodzakelijk root-acyclisch. Dan is g° =
(N°, E°, r°)
de root-unwinding van g, als volgt gedefinieerd:
r° is een nieuwe knoop, dus r ∉ N;
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
7
Hoofdstuk 1: Basis Proces Algebra
N° = N U {r°}; E° =
E U {(r°, a, v) | (r, a, v) ∈ E}
Met andere woorden, r° bootst r na:
g1
g2
als er een ‘oude’ transitie r →a v in g
a
was, komt er een ‘nieuwe’ transitie r°→a v in g°.
b
c
Opmerking: Bij het construeren van
laten staan, en de nieuwe r ° met de
g
1
+ + g
b
daardoor
g
2
nieuwe transities r° → a v daarbij te die
a
a
g° is het handig om de ‘oude’ g te
tekenen.Knopen
b
a
wortel , moeten vervolgens worden
.. g
a
c
b
a
verwijderd (garbage collection).
2
a
c
onbereikbaar worden uit de nieuwe
1
b
b
a
a
1.4.6. OPGAVE. Zij g root-acyclisch. Laat zien dat g en g° dan hetzelfde zijn.
1.4.7. OPGAVE. Zij g de procesgraaf van Stack in Figuur 8.5. Geef g°.
Door het procedé van root-unwinding te itereren, kunnen we een procesgraaf helemaal
cycle-vrij maken, dat wil zeggen, uitrollen tot boom (‘tree-unwinding’).
1.4.8. OPGAVE. Geef de eerste paar ‘lagen’ van de treeunwinding van de Stack procesgraaf.
1.4.9. D EFINITIE. acties.We
Zij A een verzameling atomaire
definieren
termopbouw)
de
inductie
procesgraaf
(gesloten) BPA-term t:
G(a)
(met
G(t)
naar
van
de
een
G(ab)
a b
G((a +
a)(b + b))
a
a
b
b
b
= o →a o
G(s + t) = G(s) + + G(t)
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
8
Hoofdstuk 1: Basis Proces Algebra
G(s.t) = G(s)
..
g
G(t)
g
1
a
Dit is nog niet alles, want om
g
2
3
b
a
b
een model te hebben van BPA moeten ook de axioma’s van BPA en
wat
daaruit
h
volgt,
waar zijn. Dat betekent dat we bijvoorbeeld de procesgrafen G((a + a)(b + b)) en G(ab) moeten BPA Deze
identificeren,
omdat
(a + a )(b + b) = ab. twee
grafen
zijn
in
h
1
a
b
a
b
a
b
a
b
Figuur 1.8 weergegeven.
h
2
a
3
b
a
b
a
b
a
b
a
b
Met welk criterium moeten we dergelijke grafen identificeren?
Figuur 1.8
Het blijkt dat de juiste notie is:
de notie van bisimulatie. Deze notie speelt een centrale rol in procesalgebra.
1.5.
Bisimulatie.
1.5.1. D EFINITIE . Laten g = (N, E, r) en g’ = (N’, E’, r’) twee procesgrafen zijn over de verzameling A. Een relatie R
N x N’ heet een bisimulatie tussen g en g’, notatie R: g
g’,
als
(r, r’) ∈ R voor alle a ∈ A geldt: als s →a t
en (s, s’) ∈ R, dan is er een knoop t’ ∈ N’ zodat s’ →a t’
en (t,t’) ∈ R. en vice versa.
We noemen twee procesgrafen g en g’ bisimilair, notatie g
g’, als er een bisimulatie bestaat
tussen g en g’.
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
9
Hoofdstuk 1: Basis Proces Algebra
g
h
R
s
⇒
t
a
g
R
s
s'
h
R
s
⇒
t a
g
a R
R
s
t'
h t
a s'
t'
t
a
s'
g
h
a R
t'
Figuur 1.9
1.5.2. OPGAVE. Laat zien dat
Als g
een equivalentierelatie is.
g’ denken we aan g en g’ als ‘dezelfde’ graaf, die verschillende ‘versies’ zoals g
en g’ kan hebben. Een mogelijk probleem is nu dat de optelling + en vermenigvuldiging van g1 en g 2 wel eens af zouden kunnen hangen van de gebruikte versies g 1’ en g2’. We zouden een probleem hebben als het volgende geval zich voordeed:
g1
maar niet
g1’,
g1 + + g2
g2
g2’,
g1’ + + g 2 ’,
en analoog voor vermenigvuldiging. Gelukkig doet dit geval zich niet voor, en hebben we:
1.5.3. PROPOSITIE.Gegeven zijn vier procesgrafen g, h, g’, h’ ∈ G(A).Dan: (i) g
g’, h
h’ ⇒ g + h
g’ + h’
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
10
Hoofdstuk 1: Basis Proces Algebra
(ii) g
g’, h
h’ ⇒ g . h
g’ . h’
We kunnen nu het graafmodel definiëren.
We hebben nu de volgende belangrijke stelling, waarvan het precieze bewijs nog wat
detailwerk vergt, dat we achterwege laten. 1.5.4.
D EFINITIE . Het graafmodel is het grafendomein G(A) met daarin bisimilaire grafen
geidentificeerd, notatie G(A)/
, in woorden G (A)
vermenigvuldiging g.g’ van g, g’ ∈ G(A)/
modulo
. Optelling g + g’ en
,worden verkregen door willekeurige (root-
acyclische) representanten (‘versies’) van g, g’ op te tellen, respectievelijk te vermenigvuldigen.
1.5.5. S T E L L I N G . Zij A een actie-alphabet. Dan geldt voor alle gesloten termen s, t ∈ Ter(BPA):
BPA
s = t ⇔
We hebben met G(A)/
G(s)
G(t).
dus een model van BPA gemaakt. De interpretatie van term t ∈
Ter(BPA), is als volgt: [t] ] = {g | g
G(t)}.
Deze stelling is een correctheids- en volledigheidsstelling van de
theorie BPA ten opzichte van de semantiek gegeven door het graafmodel. Een toepassing van de volledigheidsstelling is dat we nu kunnen bewijzen dat sommige vergelijkingen niet uit BPA zijn af te leiden. Bijvoorbeeld, de vergelijking a(b + c) = ab + ac is niet uit BPA af te leiden. Namelijk, bekijk de grafen G(a(b + c)) en G(ab +
ac). Het is makkelijk te bewijzen dat deze grafen niet bisimileren. Dus is de vergelijking niet afleidbaar.
1.4.7. OPGAVE. (i) Bewijs dat g
g°.
(ii) Zij g* de tree-unwinding van g. Dan geldt: g passen.
1.4.8. OPGAVE. (i). (ii)
(iii) (iv)
g*. ‘Begrijp’ dit feit door het op enkele voorbeelden toe te
Goed of fout: elke graaf met oneindig veel punten heeft een oneindig pad.
Goed of fout: als grafen g en h bisimilair zijn, hebben ze hetzelfde aantal eindknopen. Goed of fout: als g en h bisimilair zijn en g
is acyclisch, dan ook h.
Bewijs: als g en h bisimilair zijn, en g heeft een oneindig pad, dan heeft ook h een oneindig pad.
1.4.9. OPGAVE. Zij g een acyclische graaf. Bewijs dat de volgende twee eigenschappen equivalent zijn: College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
Hoofdstuk 1: Basis Proces Algebra
(i)
(ii)
11
g heeft geen punt waarin twee zijden samenkomen;
naar ieder punt van g is er een uniek pad vanuit de wortel.
Laat zien dat voor de equivalentie van (i) en (ii), het gegeven dat g acyclisch is, echt nodig is. 1.4.10. OPGAVE. Bewijs dat uit BPA niet afleidbaar is: a(b + c) = ab + a(b + c) + ac.
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
12
Hoofdstuk 1: Basis Proces Algebra
8.2.5. DEFINITIE. Een vergelijking s = t is afleidbaar in de theorie BPA, notatie BPA
s = t,
als men uitgaande van de axioma’s van BPA, en met behulp van de gebruikelijke afleidingsregels voor equationele logica (zie Intermezzo *8.2.5.1), s = t kan afleiden.
*8.2.5.1. INTERMEZZO. De volgende tabel geeft het afleidingssysteem ‘Equationele Logica’, voor een algemene vergelijkingenspecificatie (Σ, E) met signatuur Σ en stel vergelijkingen E.
s = t
(als s = t
s = t
_____________ s
σ
= t
∈ E, axioma)
(voor elke substitutie σ)
σ
s 1 = t1 ,..., sn = tn
______________________________
(voor elke n-aire F ∈ Σ
F(s 1 ,...,s n ) = F(t1 ,...,t n )
congruentie)
t = t
reflexief (axioma)
t 1 = t2
t 2 = t3 ____________________________
transitief
t1 = t 3 s = t
___________
symmetrisch
t = s
Tabel 8.2: Equationele Logica
Hierbij is σ: Var → Ter(Σ) een substitutie.Voor t ∈ Ter( Σ)
is t
σ
als volgt gedefineerd, met
inductie naar de opbouw van t:
x
σ
= σ (x )
F(t 1 ,...,t n )
σ
= F(t1
σ
,...,t n
σ
)
Voor BPA is het afleidingssysteem Equationele Logica dus als volgt (met s,t,t 1 ,t 2 ,t 3 ∈ Ter(BPA):
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
13
Hoofdstuk 1: Basis Proces Algebra
(A1),...,(A5)
axioma
s = t
_______ s
σ
= t
voor elke substitutie σ
σ
s 1 = t1 ,..., s2 = t2 ________________
congruentie voor +
s 1 +s2 = t1 + t2
s 1 = t1 ,..., s2 = t2 ________________ s 1 . s2 = t1 .
congruentie voor .
t2
t = t
reflexief (axioma)
t 1 = t2 t 2 = t3 ____________________________
transitief
t1 = t 3 s = t
___________
symmetrisch
t = s
Tabel 8.3: Equationele Logica voor BPA
8.2.4.2. VOORBEELD. BPA
aa + aa = a(a + a). Zie Figuur 8.2.
x + x = x _______ a + a = a
x + x = x (ax) __________
(ax)
(subst)
a = a + a a = a (ax) _________________
(subst)
aa + aa = aa aa = a(a + a) _____________________________________________ aa + aa = a(a + a)
(congr .)
(trans)
Figuur 8.2
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
14
Hoofdstuk 1: Basis Proces Algebra
Een afleiding uit BPA heeft dus de vorm van een boom van vergelijkingen. Een ander, equivalent, ‘format’ is zo’n bewijs te geven als een rij vergelijkingen:
1. x + x = x
(ax)
2. aa + aa = aa
(1, subst)
3. a + a = a
(1, subst)
4. a = a
(ax)
5. a(a + a) = aa
(3,4, congr)
6. aa = a(a + a)
(5, symm)
7. aa + aa = a(a + a)
(2.6. trans)
Figuur 8.2
In de praktijk doen we dit wat simpeler, namelijk door een rij van vergelijkingen achter elkaar te zetten: aa + aa = aa = a(a + a).
(Voor het tentamen volstaat de laatste methode.)
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
06-02-2002
Hoofdstuk 1: Basis Proces Algebra
College ITI, deel I , Procesalgebra, VU, voorjaar 2002
15
06-02-2002