π-calculus in the Wolfram Language
π-calculus in the Wolfram Language
Contributors:
Nikolay Murzin
José M. Rodríguez Caballero
Update: February 23, 2021
Abstract: We formalize a minimal version of π-calculus in the Wolfram Language. We develop a simple proof assistant to keep track of the transformation of π-expressions according to valid rules.
Introduction
For decades, Stephen Wolfram has been using his Wolfram Language to systematically study the properties of computational models like cellular automata [Wolfram2002, Wolfram2018], λ-calculus [Wolfram2002], combinators [Wolfram2002, Wolfram2020B, Wolfram2020C], ..., and even human thought seen as a computation [Wolfram2020A]. The present computational essay aims to add to the list of computational models studied in the Wolfram Language a new one, known as π-calculus.
The π-calculus was introduced in 1989 by R. Milner, J. G. Parrow and D. J. Walker [MPW1989] to develop a new conceptual framework for concurrency and interaction [Milner1993]. Indeed, even though any computation can be expressed in λ-calculus, the encoding may be rather hard to understand for humans. The goal of π-calculus is to be closer to human intuition when dealing with concurrency and interaction than λ-calculus.
There are several variations of the π-calculus, the applications of which range from biochemistry [RSS2000] to knot theory [MS2010]. In the present computational essay, we formalize the π-calculus version of Milner's paper [Milner1990] that we call minimum π-calculus.
Chapter I: Proof assistant
As a preliminary for introducing the π-calculus, we present a minimal proof assistant in the Wolfram Language. This proof assistant is not specific to π-calculus and it can be used to any (constructive) mathematical theory, e.g., (constructive) ring theory.
The Wolfram Language can be used as a tool to work with proof assistants. Some proofs can be easily generated using the resources of Wolfram Technology and then compiled to the proof assistant. In many cases, it may be more productive to use the Wolfram Language as a tool rather than to develop the tool in the proof assistant itself. Also, the Wolfram Language can be used as a proof assistant.
1. Minimal proof assistant
1. Minimal proof assistant
In this section we present a proof assistant designed in a minimalistic way. In the next sections we develop some user-friendly tools for working with this proof assistant.
◼
Theorems and proofs
Theorems and proofs
The main concepts of this proof assistant are proof and theorem. A proof is a composition of "have” and "mp" (modus ponens) that involve expressions in the Wolfram Language and patterns.
In[]:=
ProofQ[have[s_(*statement*),p_(*pattern*)]]:=MatchQ[s,p](*"have"iswell-definediffthestatementsatisfiesthepattern*)ProofQ[mp[h_?ProofQ(*hypothesis*),impl_?ProofQ(*implication*)]]:=MatchQ[Thm[impl],#⊢_]&[Thm[h]](*"mp"iswell-definediffthereareproofsofboththehypothesisandtheimplication,andtheimplicationcontainsthehypothesisasapremise*)ProofQ[_]:=False(*exceptinthesituationsabovewehavenotaproof*)Thm[have[s_,p_]]:=s(*thetheoremcorrespondingtoa"have"isthestatement*)Thm[mp[h_,impl_]]:=Function[{H,Impl},First[Replace[{Impl},(H⊢k_)k,All]]][Thm[h],Thm[impl]](*thetheoremcorrespondingtoamodusponensistheconclusionintheimplication*)
◼
Syntactic sugar
Syntactic sugar
In[]:=
makePiBox[box_,expr_]:=InterpretationBox[box,expr,Tooltip"Proof"]
In[]:=
have/:MakeBoxes[expr:have[p_,q_],form_]:=makePiBox[RowBox[{"have[",MakeBoxes[p,form],",",MakeBoxes[q,form],"]"}],expr]
In[]:=
mp/:MakeBoxes[expr:mp[p_,q_],form_]:=makePiBox[RowBox[{"mp[",MakeBoxes[p,form],",",MakeBoxes[q,form],"]"}],expr]
◼
Patterns in a proof
Patterns in a proof
Patterns[proof] returns the set of patterns used in proof.
In[]:=
Patterns[have[s_,p_]]:={p}Patterns[mp[h_?ProofQ,impl_?ProofQ]]:=DeleteDuplicates[Union[Patterns[h],Patterns[impl]]]
◼
Verification of a theorem
Verification of a theorem
CheckThm[proof, thesis, ValidPatterns] checks whether proof yields a proof of the statement thesis, only using the patterns from the list ValidPatterns.
In[]:=
CheckThm[proof_?ProofQ,thesis_]:=If[#==thesis&&SubsetQ[Values[ValidPatterns],Patterns[proof]],#,Failure]&[Thm[proof]]
◼
Valid Patterns
Valid Patterns
AddPattern[ x, p] adds the element x p to the list ValidPatterns, where x is the name of the new pattern and p is the new pattern itself.
In[]:=
ValidPatterns=<||>;
In[]:=
AddPattern[x_String(*nameofthenewpattern*),p_(*newpatttern*)]:=If[MemberQ[ValidPatterns,#],Failure,ValidPatterns=Append[ValidPatterns,#]]&[xp]
◼
Axioms of inference
Axioms of inference
Reflexivity.
In[]:=
HoldPattern[P_⊢P_]AddPattern["infeRefl",%];
Out[]=
HoldPattern[P_⊢P_]
Transitivity.
In[]:=
HoldPattern[(P_⊢Q_)⊢(Q_⊢R_)⊢(P_⊢R_)]AddPattern["infeTrans",%];
Out[]=
HoldPattern[(P_⊢Q_)⊢(Q_⊢R_)⊢P_⊢R_]
Commutativity of the hypothesis (not of the hypotheses and the thesis).
In[]:=
HoldPattern[(P_⊢Q_⊢R_)⊢(Q_⊢P_⊢R_)]AddPattern["infeComm",%];
Out[]=
HoldPattern[(P_⊢Q_⊢R_)⊢Q_⊢P_⊢R_]
Curry of inference.
In[]:=
HoldPattern[((P_&&Q_)⊢R_)⊢(P_⊢Q_⊢R_)]AddPattern["Curry",%];
Out[]=
HoldPattern[(P_&&Q_⊢R_)⊢P_⊢Q_⊢R_]
UnCurry of inference.
In[]:=
HoldPattern[(P_⊢Q_⊢R_)⊢(P_&&Q_)⊢R_]AddPattern["UnCurry",%];
Out[]=
HoldPattern[(P_⊢Q_⊢R_)⊢P_&&Q_⊢R_]
◼
Remark
Remark
We have not included the negation in this minimal proof assistant.
2. Supplements to the proof assistant
2. Supplements to the proof assistant
◼
Hypothesis and thesis
Hypothesis and thesis
We use the symbol ⊢ (esc rT esc) to express that an expression A (hypothesis) logically precedes another expression B (thesis) whenever A ⊢ B.
In[]:=
Hypothesis[A_⊢B_]:=A
In[]:=
Thesis[A_ ⊢ B_] := B
◼
Suggestion
Suggestion
Suggestion[x] returns a pattern from ValidPatterns such that x matches it, in case that this pattern exist.
In[]:=
Suggestion[x_(*expression*)]:=SelectFirst[Values[ValidPatterns],MatchQ[x,#]&]
◼
Automatic
Automatic
Using the following functions the user does not need to remember the patterns to use "have", it is enough to write the statement.
In[]:=
Have[s_]:=have[s,Suggestion[s]];
In[]:=
Hence[h_,t_]:=mp[h,Have[Thm[h]⊢t]]
Proof-valued functions
Proof-valued functions
A proof-valued function is a function in the Wolfram Language returning a proof as output if the proof exists. These functions will be the ground of automatic reasoning in the formalization of mathematics in the Wolfram Language, at least in our approach. They can be seems as an extension of ordinary functions, where the user is interested in the way in which the final result was found.
◼
Shortcut for transitivity of inference
Shortcut for transitivity of inference
In[]:=
Trans3[A_(*proofofP⊢Q*),B_(*proofofQ⊢R*)]:=(*proofofP⊢R*)Function[{X,Y},Function[{P,Q,R},mp[B,mp[A,Have[(P⊢Q)⊢(Q⊢R)⊢(P⊢R)]]](*proof*)][Hypothesis[X],Thesis[X],Thesis[Y]]][Thm[A],Thm[B]]
◼
Shortcut for commutativity of inference
Shortcut for commutativity of inference
In[]:=
Comm3Thm[X_(*claimP⊢Q⊢R*)]:=(*claimQ⊢P⊢R*)Function[{P,Q,R},Q⊢P⊢R][Hypothesis[X],Hypothesis[Thesis[X]],Thesis[Thesis[X]]]
In[]:=
Comm3[A_(*proofofP⊢Q⊢R*)]:=(*proofofQ⊢P⊢R*)Hence[A,Comm3Thm[Thm[A]]]
In[]:=
MP2[A_(*proofofP⊢Q⊢R*),B_(*proofofQ*)]:=(*proofofP⊢R*)mp[B(*Q*),Comm3[A(*P⊢Q⊢R*)](*Q⊢P⊢R*)]
Chapter II: π-calculus
In this chapter, we introduce π-calculus. We will use the same notation as [Bengtson2016], to make easier the transition between the Wolfram Language's implementation of π-calculus and the Isabelle/HOL's implementation. Nevertheless, despite the similarities in names, there are a lot of conceptual differences between the foundations of this theory in the Wolfram Language and in Isabelle/HOL.
π-expression
π-expression
We introduce the π-calculus using the following grammar.
◼
Syntactic sugar
Syntactic sugar
Rules for bounded/free variables
Rules for bounded/free variables
◼
Unambiguous expressions
Unambiguous expressions
Extraction of free names of an expression in π-calculus.
Extraction of bound names of an expression in π-calculus.
We eliminate the following two kind of ambiguity.
(i) two bound variables having the same name.
(ii) a free and a bound variables having the same name.
(i) two bound variables having the same name.
(ii) a free and a bound variables having the same name.
In this way, we avoid scope intrusion and we do not need α-conversion.
◼
Free and bound as propositions
Free and bound as propositions
◼
Syntactic sugar
Syntactic sugar
freeIn[x, p] is the claim (proposition) that x is free in p.
boundIn[x, p] is the claim (proposition) that x is bound in p.
◼
Axioms
Axioms
Introduction of the propositions freeIn[x, P] and ! freeIn[x, P] corresponding to the values True and False of FreeInQ, respectively.
Introduction of the propositions boundIn[x, P] and ! boundIn[x, P] corresponding to the values True and False of BoundInQ, respectively.
If a variable is not free in a parallel composition, it is not free in neither of the composed processes.
If a variable is not bound in a parallel composition, it is not bound in neither of the composed processes.
Axioms of unambiguity: a variable cannot be both free and bound in the same process. We assumed this axiom for simplicity, but it is possible to develop a version of π-calculus where it is false by using PiExpQ instead of PiQ in the patterns.
◼
Propositional simplification
Propositional simplification
Given a π-expression proc, ToThm[proc] yields the corresponding theorem expressed as a pattern.
Given two expressions, P and Q, we implement the relation P ≡ Q (esc === esc) known as structural congruence using the following axioms.
◼
Release substitution
Release substitution
◼
Axioms of α-conversion
Axioms of α-conversion
◼
Axioms for parallel composition
Axioms for parallel composition
Parallel composition is commutative.
Parallel composition is associative.
The null process behaves as a neural element at the right with respect to the parallel composition.
◼
Axioms for restriction
Axioms for restriction
The composition of two consecutive restrictions is commutative.
The evaluation of a restriction at the null process yields the null process.
◼
Axiom for replication
Axiom for replication
Definition of replication of a process.
◼
Axiom for restriction and parallel
Axiom for restriction and parallel
If x is not a free variable in Q then the restriction of the parallel composition of P and Q with respect to x is the same as the parallel composition of the restriction of P with respect to x and Q without restriction.
◼
Congruence as equivalence
Congruence as equivalence
Reflexivity.
Symmetry.
Transitivity.
Reduction
Reduction
Given two pi-calculus expressions P and Q, we consider a relation P Q (esc -> esc) known as reduction and defined by the following axioms.
◼
Rule of communication
Rule of communication
The agent on the left outputs the value z through the communication channel x to the agent on the right, who receives it as the symbol y.
Elimination rule for substitution.
Introduction rule for substitution
◼
Reduction and parallel composition
Reduction and parallel composition
The reduction is not affected by parallel composition at the right.
◼
Reduction and restriction
Reduction and restriction
The reduction is not affected by taking restrictions with respect to the same variable.
◼
Congruence and reduction
Congruence and reduction
The reduction is compatible with the structural congruence.
A congruence implies a reduction.
◼
Reduction as order
Reduction as order
Reflexivity.
Transitivity.
Chapter III: Proof compilers
In this chapter we introduce several compilers of proofs from the Wolfram Language to other systems. To transfer the code from the Wolfram environment to the other environment, copy as plaintext the output of the compilation.
◼
Export to LaTex
Export to LaTex
◼
Export to Graph
Export to Graph
Graph proof is the most human readable compilation of a proof.
Given a proof P, GraphProof[P] yields a graph where each node is a statement and each arrow is an inference.
The graph of a “have” is just a vertex.
The graph of a “mp” is the confluence of the two premises to the thesis and the graph of each premise.
To labels the vertices of a graph by numbers and to have the corresponding legend.
Remark: The numbering in the graph is compatible with the numbering in the compiled proof in latex.
◼
Export to Isabelle/Isar
Export to Isabelle/Isar
To use this compiler in Isabelle/HOL, it is required to import the library “Pi_Calculus” from Archive of Formal Proofs.
Expressions to Isar.
Proofs to Isar.
Important: Copy to Isabelle as plain text.
Chapter IV: Applications
In this chapter we show some applications of the proof assistant and the implementation of π-calculus that we developed above to prove concrete results.
Lemmas
Lemmas
◼
Lemma rParL
Lemma rParL
◼
Proof
Proof
◼
Qed
Qed
we compile this proof into a theorem, expressed as a pattern
Proof in LaTex. Copy as plaintext.
Compilation of the proof to Isabelle/Isar. Copy as plain text.
◼
Lemma axZeroL
Lemma axZeroL
◼
Proof
Proof
◼
Qed
Qed
Compilation of the proof to Isabelle/Isar. Copy as plain text.
◼
Lemma rParPlus
Lemma rParPlus
◼
Proof
Proof
◼
Qed
Qed
Compilation of the proof to Isabelle/Isar. Copy as plain text.
The examples in this section can be found in [MPW1989].
◼
Link passing (public)
Link passing (public)
◼
Proof
Proof
◼
Qed
Qed
Compilation of the proof to Isabelle/Isar. Copy as plain text.
◼
Link passing (private)
Link passing (private)
◼
Proof
Proof
◼
Qed
Qed
Compilation of the proof to Isabelle/Isar. Copy as plain text.
◼
Scope extrusion
Scope extrusion
◼
Proof
Proof
◼
Qed
Qed
◼
Example of α-redution
Example of α-redution
◼
Proof
Proof
We will substitute x by u in the following expression.
Notice that, we will need to use symbolic substitution subs, because we cannot substitute what is inside var[P] and var[Q].
◼
Qed
Qed
Conclusion
There is enormous and relatively unexplored potential in the Wolfram Language for developing proof assistants. In our approach, the theorems are just patterns, and the proofs are transformations of expressions in the Wolfram Language. Our framework is easy to use as the user does not need to remember the theorems' names but write what he thinks is the next step in the proof.
Future work
To go from π-calculus to spi-calculus [AG1999] and other extensions related to cybersecurity.
To add methods for automatic theorems proving in the Wolfram Language to this proof assistant, such as work by Jonathan Gorard, SAT solvers, and sum-check.
To explore the possible interactions between this proof assistant and the technology of Wolfram|Alpha.
To transforms the proofs in the Wolfram Language into SNARKs.
To explore the relevance of π-calculus in the frameworks of A New Kind of Science and the Wolfram Model.
Keywords
π-calculus
proof assistant
Wolfram Language
Acknowledgment
Supervisor: Xerxes D. Arsiwalla
We want to thank Xerxes for supervising this project. Thanks to Jonathan Gorard for showing his proofing assistant prototype in the Wolfram Language. A special thanks to Stephen Wolfram for conceptualizing and revealing the challenges of building a proof assistant in the Wolfram Language (from programming to sociological considerations). In general, we would also like to thank the entire Wolfram Physics Project.
References
[Bengtson2016] Bengtson, Jesper, and Joachim Parrow. “Formalising the π-calculus using nominal logic.” Logical Methods in Computer Science 5.2 (2009): 16-1.
[Wolfram2002] Wolfram, Stephen, "A New Kind of Science", Wolfram Media, 2002, URL = https://www.wolframscience.com
[Wolfram2020A] Stephen Wolfram's writings, "The Empirical Metamathematics of Euclid and Beyond", September 28, 2020, URL = https://writings.stephenwolfram.com/2020/09/the-empirical-metamathematics-of-euclid-and-beyond/
[Wolfram2020B] Stephen Wolfram's writings, "Combinators: A Centennial View", December 6, 2020, URL = https://writings.stephenwolfram.com/2020/12/combinators-a-centennial-view/
[Wolfram2020C] Stephen Wolfram's writings, "Combinators and the Story of Computation", December 7, 2020, URL = https://writings.stephenwolfram.com/2020/12/combinators-and-the-story-of-computation/
◼
Other implementations of π-calculus (links)
Other implementations of π-calculus (links)
Isabelle/HOL:
@article{Pi_Calculus-AFP,
author = {Jesper Bengtson},
title = {The pi-calculus in nominal logic},
journal = {Archive of Formal Proofs},
month = may,
year = 2012,
note = {\url{https://isa-afp.org/entries/Pi_Calculus.html},
Formal proof development},
ISSN = {2150-914x},
}
author = {Jesper Bengtson},
title = {The pi-calculus in nominal logic},
journal = {Archive of Formal Proofs},
month = may,
year = 2012,
note = {\url{https://isa-afp.org/entries/Pi_Calculus.html},
Formal proof development},
ISSN = {2150-914x},
}
Coq: https://github.com/coq-contribs/pi-calc
ProVerif: http://proverif16.paris.inria.fr/index.php