Infinite types

The word 'finite' should be dropped. It is very common to define representations over (countably) infinite sets of values. What matters is that each representation is finite, not that the number of possible representations is finite. A lot of computer science theory and practise ignores the fact that finite memory imposes unpredictable limitations. E.g. grammars, automata, recursive types, Java BigInteger, most string implementations, .... number of possible representations: I was referring to an infinite set of values for which there is a finite representation defined for each value in the set. The word 'possible' crept in because the terminology "representation of a value" sometimes refers to an actual appearance in space and time, and I was instead referring to representations in an abstract sense (i.e. that may or may not appear at a given time). I think of a program as an abstract specification expressed in some language, and in many cases (particularly in languages like 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 can be manipulated by the (abstract) program. In such cases the limitation is only an artefact of the execution environment in which the program runs, and not a property of the program itself. A computer language, defined as a set of (finite) strings that conform to a grammar, is typically countably infinite, and can easily support infinite selector expressions. Furthermore, the execution model of many computer languages is defined with respect to an abstract machine with unlimited storage. Many computer languages are Turing complete, and I thought this was expected for a conforming D under TTM. Finite memory isn't an essential factor in computational models, as evidenced by so many algorithms that work on arbitrary sized data structures. For example the following prolog is valid for arbitrary sized lists: member(X,[X|_]). member(X,[_|T]) :- member(X,T). Incorporating finite memory into abstract computational models actually destroys their simplicity. I note that it would obviate the use of mathematical induction, a fundamental proof technique in computer science. Finite memory is a cumbersome, complicating factor and reminds me of other ways in which real computers are imperfect imitations of abstract machines, such as the inevitable radioactive impurities in semiconductors that lead to occasional soft errors due to alpha particles. When I claimed finite memory is cumbersome and complicating, I wasn't for example, suggesting it's wrong or even overly difficult to write programs in low level languages that tend to work in practise. Indeed what happens in such cases is that the programmer in various ways makes "unlimited memory" assumptions. For example, consider this recursive implementation of factorial written in C int factorial(int n) { return n==0 ? 1 : n*factorial(n-1); } It is noteworthy that this program only works for a rather small set of inputs because of overflow, and yet it is /inspired/ by an algorithm that works for arbitrary sized integers. With regard to the claim about complexity, this implementation assumes there is sufficient stack space even though there is risk of stack overflow part way though its execution on a machine with finite memory. To verify that assumption involves a detailed model of the computer hardware at the level of machine code and memory usage, and analysis of the state of the stack for each possible call to factorial() by the rest of the program. A proof of correctness is usually too difficult and never attempted. Instead the programmer makes an infinite memory assumption and avoids intractable complexity in the proof. As Semyon pointed out, you incorrectly assume a set of finite strings is finite. Your qualification "or rather uses of computer languages" also suggests you think Turing computability is concerned with infinite sized programs - perhaps that manipulate infinite sized data structures. That's incorrect. The infinity part has to do with the number of (finite sized) programs that are potentially able to be executed, or the number of (finite sized) data structures that are potentially able to be manipulated. Turing computability requires a computation of a function for given input to be completed in a finite number of steps. That's why it captures our intuition about the fundamental /limitations/ of computability for real computers. Remember, not all functions are Turing computable. Even though a Turing machine has an infinite tape, at no point in time is it able to use more than a finite part of it - because the machine is bound by the finite rate at which it can access the tape. Once a Turing machine has completed a calculation we can be sure that it was only able to execute a finite program, read a finite amount of input data, manipulate a finite number of finite sized representations of data and write a finite output. The only purpose of the infinite tape is to allow each possible computation that takes a finite number of steps to actually be allowed to complete using as much (finite) tape as it needs. The idea is that all Turing equivalent computational systems are able to agree on the (infinite) set of computable functions - i.e. where each function in the set is computable with finite resources. The ability to guarantee whether a program can operate correctly has more to do with what it does. Many algorithms of interest have predictable space/time usage. Infinite types make it easier to write programs that might require large amounts of memory. Some programs by their very nature have very unpredictable space usage - i.e. that can depend in subtle ways on the input. E.g. an interpreter for a scripting language, or a theorem prover. In such cases it's very helpful to use data types that use as much memory as they need to get the job done. Inevitably, there will be risk of running out of memory. This goes hand in hand with the difficulty in predicting how long the computation will take. Indeed if the input represents a Turing complete language then memory usage and termination is undecidable. As a rough rule of thumb the number of bits required to store arbitrary values of a given finite type T is given by log2 |T| (i.e. log base 2 of the cardinality of the type). Finite types often have cardinality exceeding the number of atoms in the visible universe. E.g. let STRING<100> have at most 100 characters where each character is recorded in an octet. Then cardinality of STRING<100> is roughly 256^100. Let SET denote the type for a set of type T. Consider this fact: log2 |SET| = log2 2^|T| = |T| So the number of bits required to store an arbitrary SET> is of the order 256^100. SET> is an example of a finite type that can easily consume all memory in the system. Whether it does so depends on how it is used. Infinite types like STRING and SET are very common, practical, and often utilise memory very effectively. Some programs perform computations in bounded space for all supported inputs, and it is possible to predict memory usage given the implementation, and this has very little to do with whether infinite types (e.g. SET versus SET>) are employed. Conversely the finite type SET> offers no protection for programs that happen to need to represent a set of strings that exceeds the amount of memory.