Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Nominal Automata with Name Deallocation

Simon Prucker, Stefan Milius, Lutz Schröder

Abstract

Data words with binders formalize concurrently allocated memory. Most name-binding mechanisms in formal languages, such as the $λ$-calculus, adhere to properly nested scoping. In contrast, stateful programming languages with explicit memory allocation and deallocation, such as C, commonly interleave the scopes of allocated memory regions. This phenomenon is captured in dedicated formalisms such as dynamic sequences and bracket algebra, which similarly feature explicit allocation and deallocation of letters. One of the classical formalisms for data languages are register automata, which have been shown to be equivalent to automata models over nominal sets. In the present work, we introduce a nominal automaton model for languages of data words with explicit allocation and deallocation that strongly resemble dynamic sequences, extending existing nominal automata models by adding deallocating transitions. Using a finite NFA-type representation of the model, we establish a Kleene theorem that shows equivalence with a natural expression language. Moreover, we show that our non-deterministic model allows for determinization, a quite unusual phenomenon in the realm of nominal and register automata.

Nominal Automata with Name Deallocation

Abstract

Data words with binders formalize concurrently allocated memory. Most name-binding mechanisms in formal languages, such as the -calculus, adhere to properly nested scoping. In contrast, stateful programming languages with explicit memory allocation and deallocation, such as C, commonly interleave the scopes of allocated memory regions. This phenomenon is captured in dedicated formalisms such as dynamic sequences and bracket algebra, which similarly feature explicit allocation and deallocation of letters. One of the classical formalisms for data languages are register automata, which have been shown to be equivalent to automata models over nominal sets. In the present work, we introduce a nominal automaton model for languages of data words with explicit allocation and deallocation that strongly resemble dynamic sequences, extending existing nominal automata models by adding deallocating transitions. Using a finite NFA-type representation of the model, we establish a Kleene theorem that shows equivalence with a natural expression language. Moreover, we show that our non-deterministic model allows for determinization, a quite unusual phenomenon in the realm of nominal and register automata.

Paper Structure

This paper contains 10 sections, 46 theorems, 51 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Explicit Deallocation
  4. Semantics
  5. Deallocation Automata
  6. Name Dropping and Closure under $\alpha$-Equivalence
  7. A Kleene Theorem for NDA
  8. Determinization of NDA
  9. Conclusions
  10. Omitted Proofs and Further Details

Key Result

Lemma 2.1

Let $f\colon X\to\mathcal{P}_\omega(Y)$ be equivariant. Then $\mathop{\mathrm{\mathsf{supp}}}\nolimits(y)\subseteq\mathop{\mathrm{\mathsf{supp}}}\nolimits(x)$ for all $x\in X$, $y\in f(x)$.

Figures (4)

  • Figure 1: Invariance of NDA transitions under $\alpha$-equivalence
  • Figure 2: An example NDA accepting valid logs of sessions with at most two participants (a and b) and an admin (c). The NDA accepts all logs where all users except for the admin are logged out in the end.
  • Figure 3: Correspondence between regular deallocation expressions, D-NFA, and NDA. Together, this yields a Kleene-theorem for NDA.
  • Figure 4: Proof sketch of \ref{['th:DDA']}.

Theorems & Definitions (81)

  • Lemma 2.1
  • Lemma 3.1: label=lem:cnConcat
  • Lemma 3.2
  • Lemma 3.3
  • Example 3.4: label=ex:boundAndClean
  • Definition 3.5: name=$\alpha$-equivalence,label=def:Alpha
  • Lemma 3.7
  • Remark 3.9
  • Definition 4.1
  • Lemma 4.2
  • ...and 71 more