fb18.de
/ Diplom Informatik
/ Theoretische Informatik (HS)
PNL: Rekursion
Dazu hab ich ein paar Fragen:
[*]Bei Beispiel 2.25, f versteh ich die zweite Lösung nicht. Wo kommt denn das "b" her ? Versteh ich die Definition mit den Gammas dahingehend richtig, daß kein gleichzeitiges "aa" bzw. "ab" stattfinden kann ?
[*]Definition 2.28, was soll denn die "Lösung Xi" sein? Und was bedeutet "in E" ?? Ich ahne, was gemeint ist, aber vielleicht kann das auch mal jemand verständlich erklären (z.B. die Bedeutung von <Z|Z=aZ>).
Vielen Dank im voraus!
zu 1.: Ich habe das so verstanden:
siehe 2.25 a), X = X hat alle Prozesse als Spezifikation.
Mit der Kommunikationsfunktion bei f) sind die atomaren Prozesse a und b gegeben, damit is a + b die Spezifikation vom zweiten parallelen Prozess bei f).
Bei mir ist der Groschen damit noch nicht gefallen:
Wieso bzw. wodurch sind denn die atomaren Prozesse a und b gegeben ? Bei der rekursiven Spezifikation steht ja nur ein a.
X = a||X
= (a|LX) + (X|La) + (a|X)
= (aX) + ((a||X)|La) + (a|(a||X))
= (aX) + ((a||((a|LX)+(X|La)+(a|X)))|La) + (a|(a||X))
<seufz> Und wo kommt da jetzt ein b ins Spiel ? Oder hat es was damit zu tun, daß man die Rekursion dank fehlenden guard beliebig häufig ausführen kann und somit immer ein offenes X hat, was auch ein b sein könnte??
so nun habs ich endlich verstanden, musste auch lange hinschauen
zu 1.
aus {X = a || X} kann natürlich niemand ein b rauslesen,
da wurde wohl stillschweigend angenommen,
dass wie immer a und b die beiden einzigen anwesenden Aktionen sind,
und dann ist doch klar: wenn b geht kommt b auch rein
die Definition verstehst du richtig,
a und a sowie a und b dürfen nicht gemeinsam ausgeführt werden,
2.
E ist eine Spezifikation, eventuell rekursiv,
jetzt betrachten wir nur geschützte rekursive Spezifikationen,
denn solche Spezifikationen sind eindeutig,also besitzen maximal eine Lösung,
Eindeutigkeit bedeutet wohl auch das sie immer lösbar sind?
ich denk mal ja, wenn nicht bitte korrigieren
Beispiel: Z = aZ
diese Spezifikationen sind also immer lösbar, und es existiert nur eine Lösung,
genau ein Prozess p, sodass p bisimilar zu a p ist
manchmal will man mit dieser Lösung arbeiten,
sie also hinschreiben ohne das p zu definieren
(wenn man mit vielen Spezifikationen rumhantiert, wären das viele ps),
dann schreibt man einfach <Z|Z=aZ>, denn das ist das gleiche wie p,
also p = <Z|Z=aZ> nach Definition,
<Z|Z=aZ> ist die eine eindeutige Lösung für Z in E gleich Z = aZ,
also in der Spezifikation Z = aZ
edit
bei diesem Beispiel gabs nur eine Prozessvarible,
wenn 2 da sind dann gibts in der Lösung auch 2 Prozesse,
für jede Variable einen
so nun habs ich endlich verstanden, musste auch lange hinschauen
Sehr beruhigned…
und dann ist doch klar: wenn b geht kommt b auch rein
Das ist mir grad nicht so klar, werd mir das aber nochmal zu Gemüte führen.
E ist eine Spezifikation, eventuell rekursiv,
jetzt betrachten wir nur geschützte rekursive Spezifikationen, denn solche Spezifikationen sind eindeutig,also besitzen maximal eine Lösung, Eindeutigkeit bedeutet wohl auch das sie immer lösbar sind?
ich denk mal ja, wenn nicht bitte korrigieren
Beispiel: Z = aZ
diese Spezifikationen sind also immer lösbar, und es existiert nur eine Lösung,
genau ein Prozess p, sodass p bisimilar zu a p ist
soweit klar
manchmal will man mit dieser Lösung arbeiten,
sie also hinschreiben ohne das p zu definieren
(wenn man mit vielen Spezifikationen rumhantiert, wären das viele ps),
dann schreibt man einfach <Z|Z=aZ>, denn das ist das gleiche wie p, also p = <Z|Z=aZ> nach Definition,
Wenn ich das jetzt richtig verstanden habe, gilt also im Beispiel 2.29 <X|E>=ababab… und <Y|E>=babababa… , oder?
<Z|Z=aZ> ist die eine eindeutige Lösung für Z in E gleich Z = aZ,
also in der Spezifikation Z = aZ
Also <Z|Z=aZ> = aaaaa…. ?
Auf jeden Fall schonmal Danke für die Hilfe
und dann ist doch klar: wenn b geht kommt b auch rein
Das ist mir grad nicht so klar, werd mir das aber nochmal zu Gemüte führen.
wenn die Gleichung X = X heißt dann steht da ja auch nicht was erlaubt ist und was nicht,
es ist alles erlaubt was da ist,
wenn a und b da sind, dann eben alle beliebigen Prozesse mit a und/ oder b,
bei X = a || X sinds natürlich nicht mehr alle Prozesse,
aber wenn es einen Prozess gibt, in dem b drin ist,
und der die Gleichung erfüllt, dann ist das eine ordentliche Lösung
Wenn ich das jetzt richtig verstanden habe, gilt also im Beispiel 2.29 <X|E>=ababab… und <Y|E>=babababa… , oder?
wenn E = {X=aY, Y=bX} ist dann sind das da oben zwei wahre Asussagen, ja
<Z|Z=aZ> ist die eine eindeutige Lösung für Z in E gleich Z = aZ,
also in der Spezifikation Z = aZ
Also <Z|Z=aZ> = aaaaa…. ?
ja
starker Smilie
@Björn -> einbauen
;)
Der einzige Smily der noch fehlt, ist der "ich wander aus!"-Smily…
Der ist aber mehr als 100 Pixel breit *duck*
jaja.. ich bin eh konservativ
Der einzige Smily der noch fehlt, ist der "ich wander aus!"-Smily…
…nach Neuseeland?!?
Nicht ganz. Der Smily sollte vielleicht etwas deprimierter gucken und ein Messer im Rücken haben oder ähnliches.
Ich dachte eher an so:
[img]
http://www.fb18.de/gfx/admin.gif[/img]
neue (alte) Frage:
Ist es bei Beispiel 2.25a nicht sinnvoller, wenn dort stehen würde:
X=X hat jeden Term als Lösung ?
Immerhin ist X=X ja schon eine Spezifikation ?
Oder ist es wieder ein omniöser Schreibfehler ??
Ist es bei Beispiel 2.25a nicht sinnvoller, wenn dort stehen würde:
X=X hat jeden Term als Lösung ?
find ich auch.
Die Fehler im Skript machen es besonders in dem Teil schwer, durchzusteigen…
wenn wir schon grad in diesem Teil sind:
Gibt es Spezifikationen, die keine Lösungen haben?
(abgesehen davon dass die Menge der zur Verfügung stehenden Aktionen nicht reicht)
S.33
da steht ACP_T mit gesch. lin. Rekursion sei vollständig und korrekt,
gilt das nur wenn auch Fairness dabei ist?
weil vorher (S. 24) für ACP mit gesch. Rekursion nur Korrektheit erfüllt ist
(bzw. über Vollständigkeit steht da nix, gilt das auch?,
oder gibt es ein prominentes Gegenbeispiel?)
wenn wir schon grad in diesem Teil sind:
Gibt es Spezifikationen, die keine Lösungen haben?
(abgesehen davon dass die Menge der zur Verfügung stehenden Aktionen nicht reicht)
Ich glaube, solche gibt es nicht.
S.33
da steht ACP_T mit gesch. lin. Rekursion sei vollständig und korrekt,
gilt das nur wenn auch Fairness dabei ist?
weil vorher (S. 24) für ACP mit gesch. Rekursion nur Korrektheit erfüllt ist
(bzw. über Vollständigkeit steht da nix, gilt das auch?,
oder gibt es ein prominentes Gegenbeispiel?)
Meinst du wirklich, das solche Sachen wie Vollständigkeit und Korrektheit drankommen ? <schauder>
Meinst du wirklich, das solche Sachen wie Vollständigkeit und Korrektheit drankommen ? <schauder>
also sagen ob ja oder nein ist ja nun nicht grad schwer,
was willst du sonst lieber lernen, die Transitions oder Gleichheitsregeln? ;)
Hi,
ich hab da mal auch eine ganz allgemeine Frage zu geschützter rekursiver Spezifikation und zwar:
- was "geschützt" nun eigentlich bedeutet
- das jede eindeutige R. Spez. geschützt ist steht ja im
Skript aber gilt das auch andersrum, also ist somit jede
geschützte R. Sp. auch eindeutig?
Danke im voraus
meinst du den Grund für die Benennung 'geschützt'?,
solche philosophischen Fragen solltest du direkt an den Professor schicken ;),
ich sage mal 'geschützt vor mehreren Lösungen',
zur anderen Frage:
in meinem Skript steht:
'eine rek. Spez. ist genau dann eindeutig (modulo Bisimulation) wenn sie geschützt ist'
das klingt doch deutlich
Wäre jemand vielleicht so nett und würde mir den Prozessterm aXb+c mit den Transitionsregeln auf Seite 22 genauer erklären?
(Bitte nicht auf die anderen Threads verweisen, die haben mir auch nicht weitergeholfen)
Danke im voraus
was bedeutet es denn einen Prozessterm mit irgendwelchen Transitionsregeln 'genauer zu erklären'?
aXb+c besteht aus einem a, einem großen X, einem b, einem + und einem c
wenn du den Prozessgraphen ableiten willst, dann steht das doch schon woanders hier,
(ich poste jetzt natürlich keinen Link),
soll das noch mal jemand wiederholen, oder ist deine Frage etwas konkreter/ anders?
nochmal wiederholen bitte. Ich hab es noch nicht verstanden.
bitte schön, copy + paste sind ja schnell gemacht
Prozessgraph:
a a
aXb+c----(aXb+c)b------(aXb+c)bb...
| | .
|c |c .c
| | .b
# |b .b
# ..
Ableitung:
a
(1) a-># ------
a
a->#
v
a x->#
(2) aXb->Xb ------ mit x=a, y=Xb, v=a
v
x*y->y
v
a y->y'
(3) aXb+c->Xb ------ mit x=c, y=aXb, y'=Xb, v=a
v
x+y->y'
v
a t1(X)->y
(4) X->Xb -------- mit t1(X)=aXb+c,y=Xb
v
X->y
