How exactly does on describe the formal semantics of the Applied $\pi$-Calculus? - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-09-18T03:06:05Z https://cs.stackexchange.com/feeds/question/56474 https://creativecommons.org/licenses/by-sa/4.0/rdf https://cs.stackexchange.com/q/56474 2 How exactly does on describe the formal semantics of the Applied $\pi$-Calculus? josh https://cs.stackexchange.com/users/47935 2016-04-25T11:26:53Z 2016-04-25T22:13:28Z <p>In <em>"Mobile Values, New Names, and Secure Communication"</em>, Abadí and Fournet describe thet Applied-$\pi$-Calculus. Although I understood a great part of the description of the Applied $\pi$-Calculus, I'm still a bit confused as to what exactly its formal semantics consists of.</p> <p>The authors define (on page 2):</p> <blockquote> <p>A <em>signature</em> $\Sigma$ consists of a finite set of function symbols, such as <code>f</code>, <code>encrypt</code>, and <code>pair</code>m each with an arity.</p> </blockquote> <p>On page 3, they say that</p> <blockquote> <p>Given a signature $\Sigma$, we equip it with an equational theory, that is, with an equivalence relation on terms that is closed under substitution of terms for variables.</p> </blockquote> <p>Then they proceed, still on page 3, to define <em>Structural equivalence</em>, which also <em>is</em> an equivalence relation, but defined on extended processes and not terms.</p> <p>So after reading the paper a number of times and consulting some other resources on the Internet, I have concluded that the semantics of the $\pi$-Calculus depends on a given signature (and hence is "parametrized" in a sense); and that it is composed of:</p> <ul> <li>the signature and its equational theory, which is provided by us, depending on the application context (I may include symmetric cryptography functions and some equations modeling their behavior, and no asymmetric constructions at all, for example);</li> <li>the structural equivalence relation for processes;</li> <li>the internal reduction relation (structural semantics used for plain processes);</li> <li>the reduction relation including interaction with the environment.</li> </ul> <p>Is this correct, or did I miss anything?</p> https://cs.stackexchange.com/questions/56474/-/56502#56502 3 Answer by Martin Berger for How exactly does on describe the formal semantics of the Applied $\pi$-Calculus? Martin Berger https://cs.stackexchange.com/users/2887 2016-04-25T22:13:28Z 2016-04-25T22:13:28Z <p>You are roughly correct. From an operational point-of-view, applied-$\pi$ is 'just' a $\pi$-calculus where interesting values (rather than just pure names) can be communicated.</p> <p>Note that in process theory we usually care about coarser notions of equality, such as observational equivalence. This is defined in Section 4.1. Alas observational equivalence is hard to work with in practise due to the universal quantification over all contexts, so we define a second relation which is easier to deal with, in this case labelled bisimilarity. In order to do this, we need labelled transitions rather than reductions. We must show that these two forms of computation coincide.</p> <p>To make matters even more complicated, Theorem 1 which claims that observational equivalence coincides with labelled bisimilarity is wrong.</p>