Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Rule Formats for Nominal Process Calculi

Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, Yolanda Ortega-Mallén

TL;DR

The paper develops rule-formalism for nominal residual transition systems to guarantee that the induced semantics form a nominal transition system for calculi with binders. It introduces nominal residual transition system specifications (NRTSS) and two formats, Equivariant and alpha-conversion-of-residuals (ACR), together with partial strict stratification to enforce alpha-conversion of residuals and equivariance. It applies the framework to the early pi-calculus and demonstrates, via an example, that the generated NRTS satisfies the NTS properties, with binding-name handling via bn. The work provides a foundation for modular, binder-aware SOS rule formats and points toward congruence results and extensions for more expressive nominal semantics.

Abstract

The nominal transition systems (NTSs) of Parrow et al. describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specification of the early pi-calculus. Our study stems from the recent Nominal SOS of Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.

Rule Formats for Nominal Process Calculi

TL;DR

The paper develops rule-formalism for nominal residual transition systems to guarantee that the induced semantics form a nominal transition system for calculi with binders. It introduces nominal residual transition system specifications (NRTSS) and two formats, Equivariant and alpha-conversion-of-residuals (ACR), together with partial strict stratification to enforce alpha-conversion of residuals and equivariance. It applies the framework to the early pi-calculus and demonstrates, via an example, that the generated NRTS satisfies the NTS properties, with binding-name handling via bn. The work provides a foundation for modular, binder-aware SOS rule formats and points toward congruence results and extensions for more expressive nominal semantics.

Abstract

The nominal transition systems (NTSs) of Parrow et al. describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specification of the early pi-calculus. Our study stems from the recent Nominal SOS of Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.
Paper Structure (7 sections, 8 theorems, 11 equations)

This paper contains 7 sections, 8 theorems, 11 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Nominal terms
  4. Specifications of NRTSs
  5. Rule formats for NRTSSs
  6. Example of application to the early $\pi$-calculus
  7. Conclusions and future work

Key Result

lemma 1

Let $\varphi$ be a substitution and $\pi$ a permutation. Then, $\pi\cdot \overline{\varphi}= \overline{\pi\cdot \varphi}$.

Theorems & Definitions (29)

  • definition 1: Nominal sets
  • definition 2: Atom abstraction
  • definition 3: Nominal transition system
  • definition 4: Nominal residual transition system
  • definition 5: Nominal signature and nominal sort
  • definition 6: Raw terms
  • definition 7: Substitution
  • lemma 1: Extension to raw terms is equivariant
  • lemma 2: Substitution and permutation action
  • definition 8: $\Sigma$-structure
  • ...and 19 more