Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Functional Array Programming in an Extended Pi-Calculus

Hans Hüttel, Lars Jensen, Chris Oliver Paulsen, Julian Teule

TL;DR

A translation of BUTF into a version of the pi-calculus with broadcasting and labeled names is given, both complete and sound, and a cost model is proposed by annotating translated BUTF processes.

Abstract

We study the data-parallel language BUTF, inspired by the Futhark language for array programming. We give a translation of BUTF into a version of the pi-calculus with broadcasting and labeled names. The translation is both complete and sound. Moreover, we propose a cost model by annotating translated BUTF processes. This is used for a complexity analysis of the translation.

Functional Array Programming in an Extended Pi-Calculus

TL;DR

A translation of BUTF into a version of the pi-calculus with broadcasting and labeled names is given, both complete and sound, and a cost model is proposed by annotating translated BUTF processes.

Abstract

We study the data-parallel language BUTF, inspired by the Futhark language for array programming. We give a translation of BUTF into a version of the pi-calculus with broadcasting and labeled names. The translation is both complete and sound. Moreover, we propose a cost model by annotating translated BUTF processes. This is used for a complexity analysis of the translation.

Paper Structure

This paper contains 20 sections, 7 theorems, 26 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. A language for array programming
  3. Basic Untyped Futhark
  4. Expressions in ButF
  5. Array Operations
  6. Extended Pi-Calculus
  7. Processes in E$\pi$
  8. Semantics
  9. Weak Bisimilarity
  10. Translating ButF to E$\pi$
  11. Translating the functional fragment
  12. Tuples
  13. Representing arrays
  14. Arrays
  15. Array Operators
  16. ...and 5 more sections

Key Result

Lemma 1

For any process $U$ it holds that if $U\rightarrow P'$ and $U$ is not observable on any channel, then $P'\in\mathcal{U}$.

Figures (4)

  • Figure 1: The structural congruence rules for the extended $\pi$ calculus
  • Figure 2: The reduction rules of extended processes in E$\pi$. Here, $q$ is either $\tau$ or some ${:}b$.
  • Figure 3: Labeled semantics for important ($\xrightarrow\bullet$) and administrative reductions ($\xrightarrow\circ$) in E$\pi$.
  • Figure 4: The translation for basic expressions.

Theorems & Definitions (13)

  • Definition 1
  • Definition 2: Weak Administrative Barbed Bisimulation
  • Lemma 1
  • Theorem 1
  • proof
  • Definition 3: Administrative Operational Correspondence
  • Lemma 2
  • Lemma 3
  • proof
  • Lemma 4
  • ...and 3 more