Jürgen Ernst, Dipl.-Ing.(FH) HomepageKontaktInformationLinksNews
Hard- & Software-EntwicklungInformation: Software patents under the magnifying glass
 

Information: Software patents under the magnifying glass



4.2 Mathematical proof

Table of contents

1 Divide and Conquer
2 Mathematical Basics
3 Turing Machines and -Calculus
4 Proof of Software
5 Analyses
5.1 Analysis of Statement a)
5.2 Analysis of Statement b)
5.3 Analysis of Statement c)
5.4 Analysis of Statement d)
6 Conclusion
7 Literature

1 Divide and Conquer

In the 19th century the emergence of the patenting (german Patents Act of 1877) was inevitable based on the scientific possibilities and knowledge at that time. An epistemological paradigm was that one can divide the knowledge of the world into independent categories, e.g. mathematics, physics, chemistry, biology, sociology, astronomy etc. and that in these fields of knowledge or sciences there should be further and finer independent partitioning. This is called the approach of Divide and Conquer.

Many years later one had to state that this approach did not work as one had imagined first. From a mathematical point of view the assumption of categories, a grouping of elements into disjoint sets (tree structure), was wrong. Today the modern aspects starts out from overlapping sets (network architecture). In particular our scientific understanding of the world had experienced a very fundamental change by the quantum theory (1925-1928), which represents in its core non-local theory. This insight is known as "everything is connected with everything" and has led to new interdisciplinary fields of research: biochemistry, bio computer science, economical informatics, physical chemistry, applied mathematics etc.

Despite of all scientific knowledge of the last 125 years, today the patenting is still based implicitly on the outdated categorical approach:

a) All ideas are well distinguished against each other and they are infinite.
In the illustration on the right side this is to be symbolized by coloured circles. Free ideas are represented "blue" and patented are "red". Ideas, which are based on other ideas and/or contain other ideas, are called derived ideas (see item c).
b) To any given idea there exists an immense number of realizations. Realizations of different ideas are different from each other as well.
In the illustration on the right side the white circles located below the ideas represent their concrete realizations. A red box stands for a patented idea. It's like a fence around a property. Commonly used soil does not exist. Therefore each patent has its own area of application.
c) A patent covers also the derivative of an idea and/or the derivative of the realization of an idea.
One level under the concrete realizations, attainable over arrows, derived realizations are drawn. If e.g. idea 1 were the "wheel", then x could stand for barrows. If e.g. idea 2 were a "brake", then z could stand for a push pull cable with brake. The case of a patent infringement is represented by y, if e.g. y were a bicycle with brake. The patentee argues that the person who builds y plagiarized that. This shows that the requirement range of the patent is extendable at will, if the derivative contains the patented idea.
d) There are still enough free ideas and realizations of ideas so that the set of all patented ideas does not disturb strongly.

Now we adapt the above statements from the patenting, so that they fit into the range of the software. For this we equate idea with function (and/or mapping) and the realization of an idea with a program (and/or algorithm):

a) All functions are well distinguished against each other and they are infinite.

b) To any given function there exists an immense number of realizations (programs). Programs of different functions are different from each other as well.

c) A patent covers also the derivative of a function and/or the derivative of the program of a function.

d) There are still enough free functions and programs of functions so that the set of all patented functions does not disturb strongly.

We regard these statements intuitively as correct due to our everydays life experiences and apparently it seems that closer proofs, which prove the correctness clearly, are not necessary. Now we would like to develop the appropriate proofs gradually in this text. It will turn out that the statements, mentioned above are inadequate and contradictory.


2 Mathematical Basics

In mathematics one derives relations from the set theory. If it depends on the order of two elements x1, x2, then the term of the ordered pair or 2-tuple ( x1, x2 ) is used. A set-theoretical definition of the ordered pair would be the following:

Definition (1)

( x1 , x2 ) { x1 , x2 } because of { x1 , x2 } = { x2 , x1 }
but:
( x1 , x2 ) := { { x1 } , { x1 , x2 } }

Another possibility to form 2-tuples consists of using numbers for the structuring of numbers (Goedel numbers).

With ordered pairs the cartesian product can be defined. On the one hand it serves for the construction of new mathematical things and on the other hand it helps to firmly establish the definition of relations.

Definition (2)

M1 ... Mn := { ( x1 , ... , xn ) | xi Mi } is called cartesian product of the sets M1 , ... , Mn.
The set M1 M2 := { ( x1 , x2 ) | x1 M1 x2 M2 } is called set of pairs.

Definition (3)

Each subset R M1 ... Mn is called n-ary relation.

Relations usually do no build a clear relationship between sets, i.e. an element can have several elements be assigned. If unambiguity is needed, one uses the term mapping and/or function.

Definition (4)

A left-total, right-definite relation f M N is called mapping (or function).

A function can be understood as a set of 2-tuples, whereby each tuple obtains an unambiguous allocation. With the definitions, mentioned above we have an abstract description of the objects we will discuss in this text: functions.


3 Turing Machines and -Calculus

In the years 1936-1941 the -Calculus has been developed by Alonzo Church [CHU36, CHU41] to formalize the term function. It is an abstract model of calculability, based exclusive on function definition and application of functions. Later one recognized that the -Calculus is an efficient means for the description of programming languages. In 1960 it served McCarthy as basis for the development of the programming language LISP. Already in 1937 Alan Turing [TUR37] proved that the -Calculus and the turing machine are alternative descriptions of the same thing: our understanding of what is calculable. Nowadays turing machines are pervasive, because each existing computer and/or PC is a Turing machine.

It follows a definition, what has to be understood by a calculus:

Definition (5)

  • An alphabet is a set of symbols.
  • The set of all possible words over the alphabet A should be described by A*.
  • A language K over an alphabet A is a subset of all possible words over the alphabet, thus: K A*.
  • A calculus is a language with a set of transformation rules, which are defined on the set of the words of the language.

On the basis of (5) the following definition of the -calculus becomes understandable:

Definition (6)

It is V a countable set of variables. The language L of the -terms is inductively defined over the alphabet V { (, ), } as follows:

x V x L
M , N L ( M N ) L                   Application
x V M L ( x M ) L         Abstraction

An exacter explanation is not of a greater use in this context. The interested reader can find it in the various literature to the -Calculus. Nevertheless the sufficient knowledge of the -Calculus is however presupposed for the further reading and understanding of this text.

Note

We will refer to a contradiction of the patent law, in case software becomes patentable. In the patent law one expressly excluded mathematical formulas from patenting. As we saw above, programming does not differ to mathematics, if one uses the -Calculus or something similar and programs are mathematical formulas. This works very well in practice as it is shown by several functional programming languages such as LISP, ML, Miranda, Haskell, Scheme, Clean etc.


4 Proof of Software

Proofs of programs' characteristics is a difficult venture, since there are many problem definitions in computer science, which are proven to be unsolvable.

The most well-known problem is certainly the halting problem (Halteproblem). The halting problem concerns the question whether there is a program that is able to decide whether an other programm will stop (or terminate). This question is unsolvable. Such a program does not exist.

However it still has come worse: In 1953 Rice [ RIC53] proved that practically all interesting statements about programs are generally not decidable (see also [RIC56 ] or alternatively [HOP79]).

Sentence of Rice

"Each not trivial semantic characteristic of algorithms is not decidable."

In this connection one calls a characteristic trivial, if either every or no computed function possesses it. Thus are not decidable for example,

  • whether the computed function is totally, everywhere undefined, injective, surjective or bijective etc.,
  • whether two given algorithms compute the same function,
  • whether a given algorithm is correct to a given function, which means, it will never exist a program for the general verification of software.

It is a little bit discouraging, if one reads the sentence of Rice, but on the other side one can gain somewhat positive from the fact. If a proof is possible, then one proves always a trivial characteristic of algorithms, which is valid for all. Naturally the sentence of Rice limits the possibilities. In addition, it gives tips how to design a proof and/or where one should search.


5 Analyses

5.1 Analysis of Statement a)

a) All functions are well distinguished against each other and they are infinite.

To get the statement more precisely, we prove that there are more than countably infinite functions and that only countably infinite of them are calculable.

Definition (7)

A function is calculable, if an abstract machine exists, which computes (implements) the function.

If we want to examine whether there are functions, which cannot be computed by algorithms, then the following general characteristic of algorithms helps us:

Each algorithm can be described by a finite text over a firm, finite alphabet.

If A is an alphabet A = { a1 , ... , an } with an alphabetical order a1 < a2 < ... < an, then it is well known that A* is the set of all texts and/or words over A:

A* = { , a1 , ... , an , a1a1 , a1a2 , ... , a4a1a6a2a1 , ... }

The character stands for the word with the length 0.
Now the set of A* can be ordered first by the length of the words, i.e. to each length m there are nm different words over A (thus finite); then within the words of the same length we sort lexicographical: b1b2 ... bm < c1c2 ... cm applies for b1 < c1 (b1 = c1 b2 < c2) ... (b1 = c1 ... bm-1 = cm-1 bm < cm). Thus we determined an order on A* and hence we can state: A* is countable.

Since there are no more calculable functions as calculating algorithms and no more algorithms than texts describing them, it obviously applies: The set of the calculable functions is countable.

However there are far more functions. We regard all functions f defined on the set of the natural numbers, which supply the values 0 or 1 as results only; every function defines a subset Mf of those numbers m , for which f(m) = 1. The other way around there is a function fM which is called the characteristic function of the set M for each subset M . The set of all subsets of M is known to be uncountably infinite, just as the set of their characteristic functions; and therefore the set of all functions too.

The consequence of that is, that not calculable functions exist.

On these results one can say that there are more functions, than one can compute, but the statement under a) is nevertheless true.

5.2 Analysis of Statement b)

b) To any given function there exists an immense number of realizations (programs). Programs of different functions are different from each other as well.

We know that functions can be computed by programs. If it concerns a concrete function f, then one can write it as mapping f: A B, i.e. f maps the set of the input values A on the set of the output values B.

Functions can be understood as set of 2-tuples. The simplest functions, which we can imagine would be those, which contain only one 2-tuple. More complicated functions can be constructed, by simply adding further 2-tuples. There are countless possibilities to compute the tuple allocation in order to avoid to enumerate all tuples explicitly.

Examples

f(x) = { 1234 for x=1
g(x) = { 1234 for x=1 and 48 for x=2 and 543 for x=3
h(x) = { 1234 for x=1 and 0 otherwise
k(x) = x 2 - 2x + 1

Now we regard three special functions f1, f2 and f3:

f1(x) = { 0 for x=0 and 1 for x=1
f2(x) = x
f3(x) = x2

f1 consists of two 2-tuples, that means, the definition range and the range of values are defined for only 2 values. In contrast to it f2 and f3 are defined completely over . If we now specify the fact that our calculations with all three functions will only use two points (0 and 1) in the definition range, we see that all three computations supply the same values.

Note: Programmers use type declarations to restrict the definition range and the range of values.

Therefore one can say that x and x2 represent likewise equivalent algorithms for the computation of f1 and one can say that f2 and f3 are derivatives of f1, because they contain f1 completely. The opposite does not apply.

This characteristic of functions is not coincidental. It is, because of the fact that relations were defined as subset. See definition (3).

While programming a computer one is still more restricted. Thus e.g. f3(x) = x2 cannot be really computed at all. Because of limited memory and computing speed programs usually calculate only approximations of functions, i.e. one computes only one subset of the actual function. However, strictly spoken a reduced definition range or range of values represents another function.

We have shown that a program can quite compute the correct mapping for several functions. In fact, programs must do so compellingly, otherwise they could not supply results at all.

This is in contrast to the statement b) that programs belong only to one function, which was a condition in the categorical approach.
Thus we have proved that statement b) is wrong.

Note

One compares ambiguity and resource restrictions of the computation of a function by programs with the consequence, according to the sentence of Rice, that it is not decidable whether two given algorithms compute the same function.

5.3 Analysis of Statement c)

c) A patent covers also the derivative of a function and/or the derivative of the program of a function.

According to statement c) all functions infringe a patented function, if they are a derivative of the patented function. In the previous section we have already got to know a kind of derivative, which was based on the fact that a derived function contains exactly the 2-tuples of the patented function.

Additionally there are functions, which possess no or only very few common tuples outward, but they are completely contained in another function, in order to realize a computation. So they are derivatives too.

Now we would like to exactly examine the presence of a function in another function.

In order to illustrate, let us have a look at these representations of relations as matrices. Let there always be a function f: A B and it applies: a0 , a1 , ... , aN A und b0 , b1 , ... , bM B. Further N and M designate the cardinality of the sets, thus N = card(A) and M = card(B).

We can easily see that there are only three cases. Since we are limited to functions, thus right-definite relations, case 3) is void and is shown only for the sake of completeness. Each cross stands for a tuple. As a characteristic we can determine the number of crosses per line and/or per column.

case 1)   case 2)   case 3)
line sum  1 1 2,...,M
column sum  2,...,N 1 1

Since the matrices represent only really existing tuples (please ignore the inaccuracy in the variable "..." range of the illustrations) each line or column must always be occupied with at least one cross.

In the case 2), i.e. N = M, all sums are equal to 1. Each input value is mapped on another output value. We can say that the mapping is biunique in this case, thus bi = f ai und ai = f-1 bi.

In the case 1), i.e. N > M, there are column sums, which are greater than 1. So several input values are mapped on the same output value. Now only bi = f ai is valid. The inverse function does not apply, because it would have to supply several values, which we excluded above. Nevertheless here we can find the biunique mapping too.

Sentence (1)

Each function f: A B possesses an internal biunique kernel function KQ with Q = card(B).

Proof (1)

Because of the structure of the 2-tuples a number of M = card(B) output values forces M input values. Since functions are right-definite, all input values must be different too. This 2-tuples form the function KQ (and/or the square matrix KQ) with Q = M = card(B). Q is the number of lines and/or columns of this matrix. If the number of N = card(A) of the input values is greater than Q, then N-Q input values must be redundant and must map on values, which were already reached by KQ. For N = Q = M applies: f = KQ.qed

Since KQ always exists, we now can represent each function based on its characteristic kernel function KQ.

Sentence (2)

Each function f can be expressed as a combination of a mapping function qA and the kernel function KQ.

Proof (2)

From sentence (1) we know that each function f: A B contains a kernel function KQ with Q = card(B). We chose two new sets Aq and Bq for the mapping KQ: Aq Bq. It applies: Bq = B und Aq A. We close the gap between A and Aq with a mapping function qa: A Aq.

Then the function f can be written in the -Calculus as f = x . KQ ( qa x ).

In the case card(A) = Q it's easy to set qa = I (identity).
Examination: f = x . KQ ( qa x ) = x . KQ ( I x ) = x . KQ x = KQ.

In the case card(A) > Q we must select qA in such a way that those Q elements from A, which form KQ, are mapped directly on Aq. The redundant input values remain and are mapped on Aq in such a way that the result values are the same after passing through KQ as if we would have mapped directly in B. The redundant input values are quasi mapped on a representative in Aq. This Mapping is always possible without any problems.qed

In proof (2) we specified Bq = B. However we could have done this also in a different way. By introducing a further mapping function qb: Bq B we set qb = I and receive the same result. Again we can generalize this and thus the kernel function KQ: Aq Bq is replaced by the identity function IQ: {1,2,...,Q} {1,2,...,Q}. The task of IQ is simply said to map the interval 1,2,...,Q of the natural numbers on itself. Depending upon the value of Q we get another identity function I1 , I2 , I3 , ...

Sentence (3)

Each function f can be expressed as a combination of two mapping functions qa and qb and one characteristic identity function IQ.

Proof (3)

In proof (2) a function f has been written as f = x . KQ ( qa x ) . Now we change this expression slightly to f = x . q'b ( KQ ( q'a x ) ) and imagine q'b = I and q'a = qa. Thereby we see that the statement does not change.
Since KQ obtains a biunique mapping, thus KQ: Aq Bq is isomorphic to IQ: {1,2,...,Q} {1,2,...,Q}. Let IQ be the identity matrix with size Q. Again we use two mapping functions ma: Aq {1,2,...,Q} und mb: {1,2,...,Q} Bq for the isomorphic mapping. For f we rewrite the expression as f = x . q'b ( mb ( IQ ( ma ( q'a x ) ) ) ). It does not make sense to connect two mapping functions in series, if one mapping function can carry out the same mapping. We define qb = x .( q'b ( mb x ) ) and qa = x .( ma ( q'a x ) ) and get f = x . qb ( IQ ( qa x ) ).qed

In proof (3) we could show that an identity function IQ with Q = card(B) is embedable into each function f. Thereby the identity function and/or the number Q is an important classifier. One can express the relations in f = x . qb ( IQ ( qa x ) ) graphically.

The picture above shows clearly, that there are two ways to express the mapping from A on B.

Now we can broaden our considerations to the connections between two arbitrary functions f1 and f2.
Thereby the following mappings apply:
      f1: A1 B1 and f2: A2 B2.
We seize the cardinalities with:
      N1 = card(A1), N2 = card(A2), M1 = card(B1) and M2 = card(B2).
And the following conditions apply:
      N1 >= M1 and N2 >= M2.
The identity functions are:
      IQ1 mit Q1 = M1 and IQ2 mit Q2 = M2.

Now we form equivalence classes over the differences N1-N2 and M1-M2. With that we can compare functions with one another. The idea behind is the following: It is not important how large the matrices are. It's only important how many lines or columns they differ from each other.

Examples

N1 M1 N2 M2 N1-N2 M1-M2
5 4 5 4 0 0
12 12 12 12 0 0
6 4 3 3 3 1
8 6 5 5 3 1
12 12 10 8 2 4

The differences N1-N2 und M1-M2 can be registered into a two-dimensional coordinate system. With that, the connections become clearer. Since we always subtract the cardinalities of f2 our reference system is f2. The origin of the coordinate system expresses the identity to f2, i.e. the point (0;0) is assigned to all functions with matrices which have the same size according to f2.

If f2 is a patented function, we can state that for each function f1, if it maps on (0;0), is a patent infringement of f2.

Proof (4)

N1-N2=0 und M1-M2=0 means equal matrices in size. The identity matrices have the same size because of Q1=M1=M2=Q2. There are directly many redundant input values too, because of N1-M1=N2-M2. Transformed: N1-N2=M1-M2, thus 0=0. Thus a biunique mapping between the two functions exists. f1 x can be represented as qb ( f2 ( qa x ) ).qed

Now we show that all functions f1 mit M1-M2=0 and N1-N2>0 represents a patent infringement of f2.

Proof (5)

M1-M2=0 means equal identity matrices in size because of Q1=M1=M2=Q2. Since N1-N2>0, this means that f1 has more redundant input values than f2. However redundant input values can always be reduced to a representative by a mapping function, see proof (2). Let f'1 x' = qb ( f2 ( q'a x' ) ) denote a function as under proof (4) which maps onto (0;0). With a mapping function ma we map the redundant values x on their representatives in x'. Thus: x' = ma x and f1 x = qb ( f2 ( q'a ( ma x ) ) ). Since we can combine two mapping functions to one, we write f1 x = qb ( f2 ( qa x ) ) with qa x = q'a ( ma x ).qed

If we use the proof (5) reversely, we can say that we can reach each function on the axis N1-N2>=0 by adding redundant input values to f2. From the view of the matrices this means an adding of lines.

In addition we can add columns and it arises a new axis. Now we show that all functions f1, which lie on this axis are a patent infringement of f2.

Proof (6)

We prove constructionally, by starting in f2. When adding columns we must note that we cannot do that independently of the lines. Since we are restricted to functions, each new column forces a new line. If this would not be like that, there would be several output values which is not a function. We will move on a 45 degrees axis. Thus actually everything is already proven. Since we went out of f2 then the new matrix contains f2 in a submatrix after adding. Since f2 cannot compute all values of f1, we can accomplish this with another function f3 and a conditional branching. f1 x can e.g. simply be represented as qb ( ( if ( zusatz x ) f3 f2 ) ( qa x ) ), with if = p x y . p x y and zusatz as a function, which supplies true = x y . x if x is a new added value and otherwise false = x y . y. This selects either the function f3 or f2 for further computation.qed

Since a 45 degrees axis is not very descriptive, we amend our coordinate system a little bit. We can make a transformation of coordinates, by subtracting simply N1-N2, i.e. our horizontal axis is now (M1-M2)-(N1-N2). Thus changes at the matrices concerning changes in the number of lines or columns are similar to moving parallel to the axises.

The results of proof (5) and (6) can be combined. Any function f1 is attainable, if one starts in (0;0) and continues in running to the right on the horizontal axis until the same coordinate value. Then one runs on the vertical axis until the same coordinate value upward is reached. Thus the whole first quadrant can be achieved.

Now we derive the patent infringement for the second quadrant. This is somewhat more difficult, since f1 possesses less tuples than f2. However, since one may assume that a computation over more tuples within f1 is possible which cannot be seen outward, then the following is immediately understandable.

Proof (7)

A function f1, which lies in the second quadrant, has less tuples than the embedded function f2. We create a function f3, which we obtain from f1 by adding further tuples. This means a horizontal shift to the right. We repeat until we meet the vertical axis N1-N2. This position is determined by (M1-M2)-(N1-N2)=0 and/or (M1-M2)=(N1-N2). From proof (5) we know that a function, which lies on this axis represents a patent infringement of f2. This function has enough tuples, in order to cover f2 totally. We embed f3 in f1. This is not a trick. In the analysis of statement b) we saw that it's a current practice. There we had described a function with only 2 tuples with functions, which were defined completely over . Due to proof (6) one must regard all functions as derivatives, which were obtained by moving to the right in this coordinate system. The function f3 is derivative both from f1 and from f2. Therefore a patent infringement can be demanded from both sides.qed

So we have proved a covering of the first two quadrants. We have shown the patent infringement for f1 regarding f2.

In addition, it's possible to change the point of reference into f1. Then we can check the patent infringement for f2 regarding f1. If we do so, the labelling of the axises changes, thus N2-N1 and (M2-M1)-(N2-N1) has to be computed. Transformed in -(N1-N2) and -(M1-M2)+(N1-N2), yields -((M1-M2)-(N1-N2)), thus one can see that only the sign changes.

If one changes the sign of both axises for any point in this coordinate system, it is equivalent to a sequence of reflections at both axises and/or a point reflection at the origin. The upper half plane turns down completely on the lower half plane. So the entire surface can be covered.

We must conclude that the requirement range in statement c) is totally exaggerated. Nearly any infringement of a patent can be obtained by the changeableness of functions. Statement c) has to be declared invalid in regard to software.

5.4 Analysis of Statement d)

d) There are still enough free functions and programs of functions so that the set of all patented functions does not disturb strongly.

According to the result of statement c) statement d) cannot longer be maintained. Patents on software represent a strong disturbance and there are no opportunities of evasion.

Thus statement d) is wrong.


6 Conclusion

We showed that a patent infringement condition exists always between two functions. If one expands this result to more than two functions, one can say that the most trivial function wins, because it can be shown that the trivial function is always included in the functions, which are more complex. The reverse does not apply in general. This shows concretely how dangerous trivial patents are.

Since we have proved the fact that a patent infringement is always present, the threat by software patents is not longer hypothetical. Everyone, who calls himself a programmer or computer scientist, cannot stay calm and watch the game of the patent lobby.

Also, the ones who believe that the own patents will provide an advantage, must see now that this is not possible in the range of software. Practically each software project is constantly exposed to the danger of a patent infringement. It's only a question of time and money, which one would like to invest, in order to construct a patent infringement.


7 Literature

[BAR81] Barendregt, H.P.: The Lambda-Calculus - Its Syntax and Semantics. Amsterdam: North-Holland, 1981.

[BAR90] Barendregt, H.P.: Functional Programming and Lambda-Calculus. See also in [LEE90], pp. 321-363.

[CHU36] Church, Alonzo: An Unsolvable Problem of Elementary Number theory. American Journal of Mathematics 58, 354-363, 1936.

[CHU41] Church, Alonzo: The Calculi of Lambda Conversion. Princeton, NJ: Princeton University Press, 1941.

[DTV74] dtv-Atlas zur Mathematik: Grundlagen Algebra und Geometrie, Tafeln und Texte, Band 1, Deutscher Taschenbuch Verlag GmbH & Co. KG, München, 1974.

[ERD22] Erdmann, Karl Otto: Die Bedeutung des Wortes, Aufsätze aus dem Grenzgebiet der Sprachpsychologie und Logik, Leipzig, 1922

[ERW99] Erwig, Martin: Grundlagen funktionaler Programmierung / von Martin Erwig. - München; Wien: Oldenbourg, 1999, ISBN 3-486-25100-7

[HOP79] John E. Hopcroft, Jeffrey D. Ullman: Introduction to automata theory, languages and computation, Addison-Wesley, 1979, §8.4

[LEE90] van Leeuwen, J. (Ed.): Handbook of Theoretical Computer Science, Vol. B: Formal Methods and Semantics. Amsterdam: Elsevier Science Publishers, 1990.

[RIC53] Rice, H.G.: Classes of recursively enumerable sets and their decision problems, Trans. AMS. 89 (1953), 25-59

[RIC56] Rice, H.G.: On completely recursively enumerable classes and their key arrays, J. Symb. Logic 21 (1956), 304-341

[SOEUR] M.H.B. Sørensen, P. Urcykcyn: Lectures on the Curry Howard Isomorphism.

[TUR37] Turing, Alan M.: Computability and -Definability, Journal of Symbolic Logic 2, 1937.

[TUR87] Turing, Alan M.: Intelligence Service: Schr./Alan M. Turing. (Hrsg. v. Bernhard Dotzler u. Friedrich Kittler). Berlin: Brinkmann & Bose, 1987, ISBN 3-922660-22-3

[WRG86] Whitehead, Alfred North; Russell, Bertrand; Gödel, Kurt (1986): Principia Mathematica: Vorwort und Einleitungen / Alfred North Whitehead; Betrand Russell. Übers. von Hans Mokre. Mit einem Beitrag von Kurt Gödel. - 3. Aufl. - Frankfurt am Main : Suhrkamp, 1994 (Suhrkamp-Taschenbuch Wissenschaft ; 593) Einheitsacht.: Principia Mathematica <dt.> ISBN 3-518-28193-3