Pi calculus can be transformed from lambda calculus by replacing a variable constructor with stream constructor. But the language and protocol for accessing this stream can vary for different backends with respect to design requirements.

Stream calculus provides different disciplines for accessing underlying streams used in Pi calculus. For example: 1) linear types, or streams with constant direction without rollbacks, where each element of the stream is accessed once; 2) random access arrays; 3) GPU sources; 4) runtime typed channels; 5) effect and coeffect streams (processes as streams). Such stream calculuses could be possible in GPU languages (e.g. Futhark) and AVX intrinsics languages (e.g. Julia). We could treat stream calculus as memory representation with different access protocols.

One type of disciplines is stream calculus. While Pi calculus could be viewed as lambda calculus where function arguments are channels or streams, stream calculus defines set of constructions over these streams. This calculus is needed to provide different forms of vectorization that can be used on GPU and AVX hardware.

Language AST

data Arith = Add | Sub | Mul | Div | Eq | Lt | Gt
data Builtin
   = Intop (a: Arith) | Floatop (a: Arith)
   | Get | Set | Duplicate | Free
   | Transpose | Size
   | Asum | Axpy | Dotp | Rotm | Scal | Amax
   | Symm | Gemm | Syrk | Posv

data Fraction = Z | S (_: Fraction)
data Dimension = Vector | Matrix | Stream | Table
data Linear
   = Empty | Unit | Bool
   | Int | Float
   | Tensor (a: Fraction) (x: Dimension)
   | Pair (a b: Linear) | Fun (a b: Linear)
   | Consume (a: Linear) | All (a: Var) (b: Linear)

data Exp
   = Variable (_: Var)
   | Prim (_: Builtin)
   | Star | True | False
   | Int (_: nat) | Float (_: float)
   | Lambda (a: Var) (b: Linear) (c: Exp)
   | App (a b: Exp)
   | Pair (a b: Var) (c d: Exp)
   | Consume (a: Var) (b c: Exp)
   | Gen (a: Var) (b: Exp)
   | Spec (a: Exp) (b: Fraction)
   | Fix (a b: Var) (c d: Linear) (e: Exp)
   | If (a b c: Exp)
   | Let (a: Var) (b c: Exp)

Formal Tensor Calculus

Linear types for linear algebra

Language AST

Calculus