The Polyadic Pi Calculus: A Tutorial

Introduction - Chapter 2.2

Introductions

  • What is your background?
  • What do you hope to get out of this session?
  • What do you hope to get out of this collaborative learning group in general?
  • What is the name of a person that you love a lot?

Pi Calc is a way to describe… Concurrent computation

… Many agents active at once and can influence each other’s activity on the fly. We could treat these agents as lambda calc’s “functional computers” receiving arguments and producing results.

Based on the notion of naming.

A way of describing and analyzing systems consisting of agents which interact among each other, and whose configurations or neighborhood is continually changing

Naming strongly presupposes independence. It is natural to assume that the namer and the named are co-existing (concurrent) entities.
Naming is inextricably confused with the act of communication.
Naming is used to locate and modify data.

Treat data-access and communication as te same thing.
(data is a special kind of process. This is taken further with the rho calculus.)
Name channels, not entities.

The Monadic Pi Calculus

Names and Processes

Names: usually presented as lowercase letters like \(x, y, z\). They are the base elements of this calculus, there is no way to construct them, they just exist

Processes: usually presented as uppercase letters like \(P, Q\). Processes that are not (structurally congruent to) \(\emptyset\) (the empty, stopped, or “do nothing” process) have to be constructed using operations (atomic actions / prefixes) involving names.

Prefixes / Atomic Actions \(\pi\)

  • \(\overline{x}y\) Output the channel / name / link name \(x\)
  • \(x(z)\) Input some name from the channel / name / link \(x\) – call it \(z\)
  • Every process starts its life as \(\emptyset\), and grows by adding prefixes.

Normal Processes

Usually presented as uppercase letters like \(M\), \(N\), \(L\)

Ways to construct normal processes

  • \(M ::= \emptyset\)
  • \(M ::= \pi.P\)
  • \(M ::= N + L\)
  • \(M ::= \sum_{i \in I} N_i\)

Not Normal (Keep Pi Calc Weird) Processes

Ways to construct non-normal processes

  • \(P | Q\)
  • \(!P \rightarrow P | P | \cdots | P\)
  • \((\nu x)P\)

Examples (from section 2.2)

Example 1

Example 2

Am I a process?

Am I a process?

\(\overline{x}y.P\)

Process?

Yes

Normal?

Yes

Am I a process?

\(!N\)

Process?

Yes

Normal?

No

Am I a process?

\(P + N\)

Process?

No

Can’t “sum” non-normal processes

Am I a process?

\(N | M\)

Process?

Normal?

No

Am I a process?

\(N | P\)

Process?

Yes

Normal?

No

Am I a process?

\(!((\nu x) x(z).P) + N\)

Process?

No

The first item in the sum is not normal

Am I a process?

\(\overline{x}y.!((\nu x) x(z).P) + N\)

Process?

Yes

Normal?

Yes

Am I a process?

\(\overline{x}y.(\nu x)x(z).\emptyset | N\)

Process?

Yes

Normal?

No

Am I a process?

\(\overline{x}y.(\nu x)x(z).((\nu z)z(z).\emptyset | N)\)

Process?

Yes

Normal?

Yes

In Summary

Process constructions

  • \(P::=\sum_{i \in I}\pi_i.P_i\)
    • \(I = \varnothing \rightarrow P::= \emptyset\)
  • \(P::= P|Q\)
  • \(P::= !P\)
  • \(P::= (\nu x) P\)

After the session

Up next (potentially)

  • A more formal definition of behavior
  • Things that we can prove about our programs
  • Examples of programs that do things

Explorations

  • Create more interesting “Am I a process, and if I am, am I normal?” questions
  • Use JsonPi to run / examine examples from section 2.2
  • Create more interesting examples of Pi-Calc programs like the ones in section 2.2
  • Find other process calculi / variants on the pi calculus, record the differences
  • Learn the Lambda Calculus
  • Start learning about language definition frameworks / languages: BNFC, KFramework
  • Start learning about proof assistant frameworks: Coq, Isabelle

Feedback

https://goo.gl/forms/ehT0jj4U3Wh4gA4l2

#KFramework Pi Calc definition Create a KFramework definition of the Pi Calculus (challenge, do not use (or show the decomposition to) K Specialized Notation: Attributes, Contexts, Angle Brackets, Underscore Brackets)