24 Infinite types

Finite representations and infinite sets

Representable values need not be restricted to a finite type. It is common to define representations over countably infinite sets of values. What matters is that each individual representation is finite, not that the set of values having representations is finite.

A lot of computer science theory and practice ignores the fact that finite memory imposes unpredictable limitations. Examples include grammars, automata, recursive types, Java BigInteger, and most string implementations.

An infinite set of representable values can have a finite representation for each of its members. In this context, a “representation of a value” is an abstract form available to the computational model; it need not refer to a representation that actually appears at a particular place and time.

Abstract programs and unlimited storage

A program can be regarded as an abstract specification expressed in a language. In many cases—particularly in languages such as Prolog or Lisp, which support recursive types and have no inherent need for pointers or index positions into finite address spaces—there is no upper bound on the sizes of the data structures that the abstract program can manipulate. Any bound is then an artefact of the execution environment rather than a property of the program itself.

A computer language, defined as a set of finite strings conforming to a grammar, is typically countably infinite and can easily support infinitely many selector expressions. Furthermore, the execution models of many computer languages are defined with respect to abstract machines having unlimited storage. Many computer languages are Turing complete.

Finite memory is not an essential factor in computational models, as evidenced by the many algorithms that work on arbitrarily large data structures. For example, the following Prolog is valid for lists of arbitrary size:

member(X,[X|_]).
member(X,[_|T]) :- member(X,T).

Incorporating finite memory into abstract computational models destroys much of their simplicity. It would also obviate mathematical induction, a fundamental proof technique in computer science.

Finite memory is a cumbersome, complicating factor. It resembles other ways in which real computers are imperfect imitations of abstract machines, such as radioactive impurities in semiconductors causing occasional soft errors through alpha particles.

Correctness and finite execution environments

Saying that finite memory is cumbersome does not imply that it is wrong or overly difficult to write useful programs in low-level languages. In practice, programmers make “unlimited memory” assumptions in various ways. For example, consider this recursive implementation of factorial in C:

int factorial(int n)
{
    return n == 0 ? 1 : n * factorial(n - 1);
}

This program works for only a rather small set of inputs because of overflow, yet it is inspired by an algorithm that works for integers of arbitrary size.

The implementation also assumes sufficient stack space, despite the risk of stack overflow partway through execution on a machine with finite memory. Verifying that assumption requires a detailed model of the hardware, machine code and memory usage, together with an analysis of the stack state for every possible call to factorial() by the rest of the program. Such a proof is usually too difficult and is never attempted. Instead, the programmer makes an infinite-memory assumption and avoids this intractable complexity.

A set whose members are finite strings is not necessarily finite. Turing computability is not concerned with infinite-sized programs manipulating infinite-sized data structures. The infinity concerns the number of finite programs that can potentially be executed and the number of finite data structures they can potentially manipulate.

Turing computability requires the computation of a function for a given input to complete in a finite number of steps. This captures the relevant fundamental limitations of computation by real computers. Not every function is Turing computable.

Although a Turing machine has an infinite tape, it can use only a finite part of it at any point in time because it accesses the tape at a finite rate. After a calculation has completed, the machine has executed a finite program, read a finite amount of input, manipulated a finite number of finite representations, and written a finite output.

The purpose of the infinite tape is to allow every computation that takes a finite number of steps to complete using as much finite tape as it needs. All Turing-equivalent computational systems can therefore agree on the infinite set of computable functions, each member of which is computable using finite resources.

Resource usage in practice

The ability to guarantee that a program operates correctly has more to do with what the program does. Many useful algorithms have predictable space and time requirements. Infinite types make it easier to write programs that might require large amounts of memory.

Some programs have inherently unpredictable space requirements that depend subtly on their inputs—for example, an interpreter for a scripting language or a theorem prover. In those cases, it is helpful to use data types that consume as much memory as necessary. There is inevitably a risk of exhausting memory, just as there can be difficulty predicting how long the computation will take. If the input represents a Turing-complete language, memory usage and termination are undecidable in general.

Finite types can still exceed available memory

As a rough rule of thumb, the number of bits required to store arbitrary values of a finite type T is:

`log_2 |T|`

Finite types often have cardinalities exceeding the number of atoms in the visible universe. For example, let STRING<100> contain at most 100 characters, with each character recorded in an octet. The cardinality of STRING<100> is then roughly 256100.

Let SET<T> denote the type of sets whose elements have type T. Then:

`log_2 |SET<T>| = log_2 2^|T| = |T|`

The number of bits required to store an arbitrary SET<STRING<100>> is therefore of the order 256100. SET<STRING<100>> is a finite type that can easily consume all available memory; whether it does so depends on how it is used.

Infinite types such as STRING and SET<STRING> are common, practical and often use memory effectively. Some programs operate in bounded space for every supported input, and their memory usage can be predicted from the implementation. This has little to do with whether they use SET<STRING> or the finite SET<STRING<100>>.

Conversely, the finite type SET<STRING<100>> provides no protection to a program that needs to represent a set of strings larger than the available memory.