A Lambda Calculus for Transfinite Arrays: Unifying Arrays and Streams

TL;DR

This paper introduces a functional language with a lambda calculus that supports infinite arrays using ordinal numbers, unifying arrays, lists, and streams with transfinite recursion capabilities.

Contribution

It proposes a novel calculus extending array theories to include infinite and transfinite structures, enabling recursive specifications and unification of data structures.

Findings

Supports infinite arrays using ordinal numbers

Preserves universal equalities from array/list/stream theories

Demonstrates expressibility with various examples

Abstract

Array programming languages allow for concise and generic formulations of numerical algorithms, thereby providing a huge potential for program optimisation such as fusion, parallelisation, etc. One of the restrictions that these languages typically have is that the number of elements in every array has to be finite. This means that implementing streaming algorithms in such languages requires new types of data structures, with operations that are not immediately compatible with existing array operations or compiler optimisations. In this paper, we propose a design for a functional language that natively supports infinite arrays. We use ordinal numbers to introduce the notion of infinity in shapes and indices. By doing so, we obtain a calculus that naturally extends existing array calculi and, at the same time, allows for recursive specifications as they are found in stream- and list-based settings. Furthermore, the main language construct that can be thought of as an $n$-fold cons operator gives rise to expressing transfinite recursion in data, something that lists or streams usually do not support. This makes it possible to treat the proposed calculus as a unifying theory of arrays, lists and streams. We give an operational semantics of the proposed language, discuss design choices that we have made, and demonstrate its expressibility with several examples. We also demonstrate that the proposed formalism preserves a number of well-known universal equalities from array/list/stream theories, and discuss implementation-related challenges.