Der π-Kalkül [Milner, Parrow, Walker]

• “The π-calculus is a model of concurrent computation based upon the notion of naming.”

• Kompakt, klein, flexibel aber spartanisch, umständlich.

• Basismodell für theoretische Betrachtungenüber Nebenläufigkeit— keine Spezifikations- oder Implementationssprache.

•

λ-Kalkül  ↔ π-Kalkül
Haskell, ML ↔ CSP

Der π-Kalkül: Syntax Gegeben: unendliche Menge X von Variablen. Defn: Prozesse: P, Q ∈ P

P ::= P | Q | !P | (νx)P

Defn: Prozesse in Normalform: N, M ∈ N

N ::= π.P | 0 | M + N

Zwei unterschiedliche Formen von Präfixen: • x(y) — bindet y, “lies Namen y über Kanal x”

• \overline{x}y — bindet y nicht, “schreibe Namen y auf Kanal x”

C. Lüth  Korrekte Software durch Formale Methoden  77

Der π-Kalkül: Erste Beispiele

• Notation: x(y) für x(y).0

• Aus \overline{x}y | x(u).\overline{u}v | \overline{x}z wird 0 | \overline{y}v | \overline{x}z oder \overline{x}y | \overline{y}z | 0

• Aus (νx)(\overline{x}y | x(u).\overline{u}v) | \overline{x}z kann nur 0 | \overline{y}v | \overline{x}z werden

• \overline{x}y | !x(u).\overline{u}v | \overline{x}z kann zu 0 | \overline{y}v | !x(u).\overline{u}v | \overline{x}z werden, daraus kann 0 | \overline{y}v | !x(u).\overline{u}v | \overline{y}z | 0 werden

C. Lüth  Korrekte Software durch Formale Methoden  78

Der π-Kalkül: Operationelle Semantik I

Defn: fn(P), freie Namen in P Defn: bn(P), gebundene Namen in P Defn: Strukturelle Kongruenz ≡ kleinste Kongruenzrelation auf P:

(1) α-Kongruenz: gebundene Variablen gleich.
(2) (N / ≡, +, 0) ist ein symetrischer Monoid
(3) (P/ ≡, |, 0) ist ein symetrischer Monoid
(4) !P ≡ P | !P
(5) (νx)0 ≡ 0, (νx)(νy)P ≡ (νy)(νx)P
(6) x ∉ fn(P) ⇒ (νx)(P | Q) ≡ P | (νx)Q
C. Lüth  Korrekte Software durch Formale Methoden  79

Der π-Kalkül: Operationelle Semantik II

Comm (R_{1} + x(y).P) | (R_{2} + \overline{x}z.Q) → P[z/y]

Par {P → P′ \atop P | Q → P′ | Q}

Res {P → P′ \atop (νx)P → (νx)P′}

Struct

Q ≡ P P → P′ P′ ≡ Q′
Q → Q′

Der π-Kalkül: Rekursive Definitionen Rekursive Definitionen durch Replikation: Lösung für eine rekursive Gleichung

A(x) =^{def} P

gegeben durch

!a(x).P̂ ,

wobei P̂ = P[\overline{a}y/A(y). Beim Aufruf A(z) ersetzen durch

(νa)(\overline{a}z | !a(x).P̂ .

C. Lüth  Korrekte Software durch Formale Methoden  81

Der π-Kalkül, Beispiel: das Autotelephon CAR (talk , switch )

=^{def} talk .CAR (talk , switch ) +switch (talk′, switch ′).CAR (talk′, switch ′)

BASE (t, s, g, a)

=^{def} t.BASE (t, s, g, a) +g(t′s′).\overline{s}t′s′.IDLEBASE (t, s, g, a)

IDLEBASE (t, s, g, a) =^{def} a.BASE (t, s, g, a)

BASE _{i} =^{def} BASE (talk_{i}, switch _{i}, give _{i}, alert _{i}) i = 1, 2

IDLEBASE _{i} =^{def} IDLEBASE (talk_{i}, switch _{i}, give _{i}, alert _{i}) i = 1, 2

CENTRE _{1} =^{def} \overline{give _{1}}talk_{2}switch _{2}.alert _{2}.CENTRE _{2}
CENTRE _{2} =^{def} \overline{give _{2}}talk_{1}switch _{1}.alert _{1}.CENTRE _{1}

SYSTEM

=^{def}
(νtalk_{1}, talk_{2}, switch _{1}, switch _{2}, give _{1}, give _{2}, alert _{1}, alert _{2})
(CAR (talk_{1}, switch _{1}) | BASE _{1} | IDLEBASE _{2} | CENTRE _{1})

Mögliche Verfeinerungen: mehr Kanäle, mehr Basen, kein festes (talk , switch )-Kanalpaar pro Basis … Der π-Kalkül: Erweiterungen

• Vorgestellt: monadischer π-Kalkül

• Erweiterung: der polyadische π-Kalkül mit Abstraktionen und Konkretisierungen und mit Sorten.

• π-Kalkül höherer Ordnung

• Operationale Semantik durch commitments, Bisimulation; Axiomatisierung (endliche Prozesse, ohne Replikation).

C. Lüth  Korrekte Software durch Formale Methoden  85