Computer Graphics and Visual Communication

A very popular website about The History of Visual Communication recently hit the web. Here's a related one but applied to computer graphics/animation entitled A Critical History of Computer Graphics and Animation.

BeOS

BeOS is an operating system for personal computers which began development by Be Inc. in 1991. It was first written to run on BeBox hardware. Unlike some other operating systems of the time, BeOS was written to take advantage of modern hardware. Optimized for digital media work, BeOS made full use of multiprocessor systems by utilizing modular I/O bandwidth, pervasive multithreading, preemptive multitasking and a custom 64-bit journaling file system known as BFS. The BeOS GUI was developed on the principles of clarity and a clean, uncluttered design. The API was written in C++ for ease of programming. It has POSIX compatibility and access to a command line interface through the bash shell, although internally it is not a Unix-derived operating system.

BeOS was positioned as a platform which could be used by a substantial population of desktop users and a competitor to Microsoft Windows and Linux. However, it was ultimately unable to achieve a significant market share and proved commercially unviable for Be Inc. The company was acquired by Palm Inc.

The Haiku operating system it's an open source BeOS inspired operating system currently being developed by a community of former and new BeOS enthusiasts.

See also Programming the Be Operating System, an O'Reilly open book

Computer Networks - The Heralds of Resource Sharing

A documentary film about the history of the ARPANET and birth of the Internet.

Lambda Calculus

In mathematical logic and computer science, lambda calculus, also λ-calculus, is a formal system designed to investigate function definition, function application, and recursion. It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s; Church used lambda calculus in 1936 to give a negative answer to the Entscheidungsproblem. Lambda calculus can be used to define what a computable function is.

In Turing's words:"a function is said to be 'effectively calculable' if its values can be found by some purely mechanical process. Although it is fairly easy to get an intuitive grasp of this idea, it is nevertheless desirable to have some more definite, mathematically expressible definition. Such a definition was first given by Godel at Princeton in 1934... These functions were described as 'general recursive' by Godel ... Another definition of effective calculability has been given by Church... who identifies it with definability. The author [i.e. Turing himself] has recently suggested a definition corresponding more closely to the intuitive idea... It was stated above that 'a function is effectively calculable if its values can be found by some purely mechanical process. ' We may take this statement literally, understanding by a purely mechanical process one which could be carried out by a machine... The development of these ideas leads to the author's definition of a computable function, and to an identification of computability [in Turing's precise technical sense] with effective calculability. It is not difficult, though somewhat laborious, to prove that these three definitions are equivalent."

Turing here gives a view on what is now known and famous as Church's thesis. Although Church's thesis is nowadays given various other interpretations, in 1936 it was the claim that effective calculability could be identified with the operations of Church's very elegant and surprising formalism, that of the lambda-calculus. As such it lay within the world of mathematical formalism. But Turing offers a reason why Church's thesis should be true, drawing on ideas external to mathematics such as that one cannot do see or choose between more than a finite number of things at one time. Church's thesis is now sometimes called the
Church-Turing thesis, but the Turing thesis is different, bringing the physical world into the picture with a claim of what can be done. It should not go without mention that Turing after referring to his machine definition of computability, also cited the work of the Polish-American logician Emil Post, which had also brought an idea of physical action into computation. However Post had not developed his ideas so fully.

The question of whether two lambda calculus expressions are equivalent cannot be solved by a general algorithm, and this was the first question, even before the halting problem, for which undecidability could be proved. Lambda calculus has greatly influenced functional programming languages, such as Lisp, ML and Haskell.

Lambda calculus can be called the smallest universal programming language. It consists of a single transformation rule (variable substitution) and a single function definition scheme. Lambda calculus is universal in the sense that any computable function can be expressed and evaluated using this formalism. It is thus equivalent to the Turing machine formalism. However, lambda calculus emphasizes the use of transformation rules, and does not care about the actual machine implementing them. It is an approach more related to software than to hardware.

History and Evolution

Originally, Church had tried to construct a complete formal system for the foundations of mathematics; when the system turned out to be susceptible to the analog of Russell's paradox, he separated out the lambda calculus and used it to study computability, culminating in his negative answer to the Entscheidungsproblem.

The lambda calculus was originally developed as a foundation for mathematics. This work was done in the 1930s several years before digital computers were invented. A little earlier (in the 1920s) Moses Schonfinkel developed another theory of functions based on what are now called combinators. In the 1930s Haskell Curry rediscovered and extended Schonfinkel's theory and showed that it was equivalent to the lambda calculus. About this time Kleene showed that the lambda calculus was a universal computing system; it was one of the first such systems to be rigorously analysed. In the 1950s John McCarthy was inspired by the lambda calculus to invent the programming language LISP. In the early 1960s Peter Landin showed how the meaning of imperative programming languages could be specified by translating them into the lambda calculus. He also invented an influential prototype programming language called ISWIM. This introduced the main notations of functional programming and influenced the design of both functional and imperative languages. Building on this work, Christopher Strachey laid the foundations for the important area of denotational semantics. Technical questions concerning Strachey's work inspired the mathematical logician Dana Scott to invent the theory of domains which is now one of the most important parts of theoretical computer science. During the 1970s Peter Henderson and Jim Morris took up Landin's work and wrote a number of influential papers arguing that functional programming had important advantages for software engineering. At about the same time David Turner proposed that Schonfinkel and Curry's combinators could be used as the machine code of computers for executing functional programming languages. Such computers could exploit mathematical properties of the lambda calculus for the parallel evaluation of programs. During the 1980s several research groups took up Henderson's and Turner's ideas and started working on making functional programming practical by designing special architectures to support it; some of them with many processors.

Definition

Lambda calculus power to express any computable function derived of a very simple mechanism to define functions. Grammatically it is composed of a set of rules for function conversion (or reduction). From that it is possible to represent algebra, logic, recursion and other formalisms. In that sense it is considered an universal language.

There are three main types of conversions allowed: alfa, beta, and eta. The most important kind of conversion is beta conversion; it is the one that can be
used to simulate arbitrary evaluation mechanisms. alfa conversion is to do with the technical manipulation of bound variables and eta conversion expresses the fact that two functions that always give the same results on the same arguments are equal.

A lambda expression (necessarily an abstraction) to which alfa reduction can be applied is called an alfa-redex The term 'redex' abbreviates 'reducible expression'. The rule of alfa conversion just says that bound variables can be renamed provided no 'name clashes' occur.

A lambda expression (necessarily an application) to which beta reduction can be applied is called a beta-redex. The rule of beta conversion is like the evaluation of a function call in a programming language: the body expression of a function is evaluated in an environment in which the 'formal parameter' is bound to the 'actual parameter'.

A lambda expression (necessarily an abstraction) to which eta reduction can be applied is called an eta-redex. The rule of eta conversion expresses the property that two functions are equal if they give the same results when applied to the same arguments. This property is called extensionality.

The central concept in lambda calculus is the "expression". A "name", also called a "variable", is an identifier. An expression is defined recursively as follows:

expression := name | function | application
function := λname.expression
application := expression expression

Computable functions and lambda calculus

A function F: N -> N of natural numbers is a computable function if and only if there exists a lambda expression f such that for every pair of x, y in N, F(x) = y if and only if f x == y, where x and y are the Church numerals corresponding to x and y, respectively. This is one of the many ways to define computability; see the Church-Turing thesis for a discussion of other approaches and their equivalence.

Undecidability of equivalence

There is no algorithm which takes as input two lambda expressions and outputs TRUE or FALSE depending on whether or not the two expressions are equivalent. This was historically the first problem for which the unsolvability could be proven. Of course, in order to do so, the notion of algorithm has to be cleanly defined; Church used a definition via recursive functions, which is now known to be equivalent to all other reasonable definitions of the notion.

Church's proof first reduces the problem to determining whether a given lambda expression has a normal form. A normal form is an equivalent expression which cannot be reduced any further. Then he assumes that this predicate is computable, and can hence be expressed in lambda calculus. Building on earlier work by Kleene and constructing a Gödel numbering for lambda expressions, he constructs a lambda expression e which closely follows the proof of Gödel's first incompleteness theorem. If e is applied to its own Gödel number, a contradiction results.

Lambda calculus and programming languages

As pointed out by Peter Landin's 1965 classic A Correspondence between ALGOL 60 and Church's Lambda-notation, most programming languages are rooted in the lambda calculus, which provides the basic mechanisms for procedural abstraction and procedure (subprogram) application.

Implementing the lambda calculus on a computer involves treating "functions" as first-class objects, which raises implementation issues for stack-based programming languages. This is known as the Funarg problem.

The most prominent counterparts to lambda calculus in programming are functional programming languages, which essentially implement the calculus augmented with some constants and datatypes. Lisp uses a variant of lambda notation for defining functions, but only its purely functional subset ("Pure Lisp") is really equivalent to lambda calculus.

Functional languages are not the only ones to support functions as first-class objects. Numerous imperative languages, e.g. Pascal, have long supported passing subprograms as arguments to other subprograms. In C and C++ the equivalent result is obtained by passing pointers to the code of functions (subprograms). Such mechanisms are limited to subprograms written explicitly in the code, and do not directly support higher-level functions. Some imperative object-oriented languages have notations that represent functions of any order; such mechanisms are available in Smalltalk and more recently in Eiffel ("agents") and C# ("delegates"). As an example, the Eiffel "inline agent" expression

agent (x: REAL): REAL do Result := x * x end

denotes an object corresponding to the lambda expression ? x . x*x (with call by value). It can be treated like any other expression, e.g. assigned to a variable or passed around to routines. If the value of square is the above agent expression, then the result of applying square to a value a (ß-reduction) is expressed as square.item ([a]), where the argument is passed as a tuple.

Concurrency and parallelism

The Church-Rosser property of the lambda calculus means that evaluation (ß-reduction) can be carried out in any order, even concurrently. (Indeed, the lambda calculus is referentially transparent.) While this means the lambda calculus can model the various nondeterministic evaluation strategies, it does not offer any richer notion of parallelism, nor can it express any concurrency issues. Process calculi such as CSP, the CCS, the p calculus and the ambient calculus have been designed for such purposes.

Conclusion

We thus see that an obscure branch of mathematical logic underlies important developments in programming language theory such as:

The study of fundamental questions of computation
The design of programming languages
The semantics of programming languages
The architecture of computers.

Bibliography:

"Lambda Calculus" in Wikipedia
A Tutorial Introduction to the Lambda Calculus by Raul Rojas
The Great Philosophers - From Socrates to Turing - "Turing" by Andrew Hodges
Introduction to Functional Programming by Mike Gordon

Alan Turing

Being as i am interested in computers and mathematics i have to begin this 'on the shoulders of giants' series with one of the most prolific and influent thinkers of our time: Alan Turing. In this brief essay i'll try to explain how come he singled ed invented the computer, the modern conception of one, by his conceptual thought of the Universal Turing Machine, an abstract device that gived enough time and space could implement any algorithm. The Turing Machine came to be as the conceptual formulation of the modern computer and a powerful instrument in the study of the foundations of mathematics in the footsteps of The Entscheidungsproblem proposed by Hilbert.

When i say that Alan Turing invented the computer i'm not trying to imply that he is the only one who have contributed to the actual invention and construction of the modern computer, i'm only saying that his work on the Turing Machine is at the fundamental level of what is the modern conception of a computer and it would be enough starting from that to actually build one.

One of my heroes, Leibniz, was near achieving that goal, but he missed in linking all his ideas to a coherent and precise definition of a computer. In spite of that, lets not forget that he develop the pascal adding machine into a full calculating device.

Turing's work, besides all is implications in the development of the computer, was also a step further in the achievement reached by Kurt Godel in his famous incompleteness theorem, by stating the foundations of mathematics in terms of the halting problem, meaning that no turing machine could decide if all programs halt or not and consequently any system of formal logic is incomplete if coherent. More recently Gregory Chaitin stated the halting problem in terms of the probability that a program halts and reached the perturbant conclusion that even at a fundamental level of mathematics as in algebra there are mathematical facts that are unproven unless we take them has an axiom; they are uncompressable truths with maximum entropy or randomness.

The Entscheidungsproblem mentioned above, question whether there exists a definite method which, at least in principle, can be applied to a given proposition to decide whether that proposition is provable. Turing's great insight in his 1936 paper 'On computable numbers, with an application to the Entscheidungsproblem' was to perceive Hilbert's question in terms not of proofs, but of computing numbers. As his title said, the Entscheidungsproblem was only an application of a new idea, that of computability.

His paper starts by asking how can we specify the infinite in finite terms? In particular, how can we specify the infinite sequence of digits in a 'real number', such as n = 3. 141592, 653...? What does it mean to say that there is a definite method for calculating such a number? Turing's answer lies in defining the concept of the Turing machine.

How Turing got his result? He use'd a version of Cantor's diagonal method from set theory. He first defined a turing machine as a device capable of a very simple set of operations gived by a 'table of behavior', each one being a specific turing machine, and in some state unequivocally gived by it's current configuration plus the symbol scanned on tape. (more details)Then he defines a computable number as an infinity sequence of symbols that can be printed on a turing machine starting with a blank tape. He then rationalizes that if we order all the turing machines in a sequence we can obtain a number that differs in the Nth digit of the Nth turing machine - the diagonal method - so it's uncomputable. But if it can be defined how is it uncomputable? The problem lies in knowing if a turing machine actually produce an infinite number; Turing prove that there is no turing machine which can be applied to another turing machine proving that it will ever produce an infinite number, so that the problem itself - know known as the halting problem - is not computable. Turing states that if there was such a machine it could be applied to itself raising a contradiction - another instance of the self referencing problem finded in Godel's proof and Russel's paradox. So the question of defining something to which that is no mechanical procedure to solve it can be easily translated to an abstract mathematical question and formal logic and therefore to give a negative answer to Hilbert's Entscheidungsproblem.

The Universal Turing Machine

Besides given a definitive answer to the Entscheidungsproblem and defining the field of computability in new terms Turing's work had a practical implication: it laid out the principle of the computer through the concept of the universal Turing machine.

Given that there is a mechanical procedure capable of implementing any 'table of behaviour' in a Turing machine then there is also a more abstract one capable of implementing any Turing machine, what Turing called a Universal Turing Machine.

Today we can not but associate Turing original ideas with the concept of the modern computer. It's easy to correlate the universal Turing machine, a specific Turing machine and is configurations respectively with the computer, a computer program and the instruction blocks of a computer program. Turing also gave an algorithmic view of computation applied to the human mind which makes him also a prominent thinker in the philosophy of mind, because in spite of his pioneer work in the development of the concept of the computer, the subject of his study was the human brain as a start point from which would eventually emerge a computer.

Starting with Godel's proof of incompleteness and Alonzo Church lambda calculus we already had the answers to the questions Turing set to solve in his own work at the time he published his results, but the novel approach he devised was so ingenious and new that he achieved the conception and definition of the computer on paper before it would be physically implemented so that we might even say that he invented it.

World War II

The advent of the World War II had a profound impact in Turing´s live. Earlier, he developed an interest and some ideas about codes, cyphers and the global field of cryptanalysis. Armed with that skills he naturally achieve a position in UK effort to break German codes and their Enigma machine at Bletcheley Park. This also related with his previous experience in constructing computers: at Princeton he spent time in building a machine out of electromagnetic relays which effected binary multiplication as an encoding device, with some theory of immunity to cryptanalysis. When back at Cambridge, Turing also designed and partially built another machine, which approximated by gear-wheel motion a Fourier series for the Riemann zeta-function. It was intended to shorten the hard labor of finding the possible locations of zeros - the subject of the Riemann hypothesis, which remains today perhaps the most important unsolved problem in mathematics.



In Bletcheley Park he participated in the design of a machine called 'the Bombe' and had direct contact with the Colossus which was used in breaking the german Enigma successor, the Lorenz cipher. Due to the classified nature of his war effort to reengenering german ciphers and codes, that facet of his life was keeped secret until much after the war ended. But we can now recognize the great impact of that work simultaneous in the war outcome and to the evolution, use and recognition of the intrinsic advantages of electronic computers as a tool to solve problems.



Post War

Following his war experience, Turing went to the National Physical Laboratory and worked on his detailed design for a computer, submitting it for approval in March 1946. Turing's Automatic Computing Engine (ACE), as it was dubbed was chronologically second to the June 1945 EDVAC report bearing von Neumann's name, but in addition to the originality of its hardware design, it was ideologically independent: for (i) it was conceived from the outset as a universal machine for which arithmetic would be just one application, and (ii) Turing sketched a theory of programming, in which instructions could be manipulated as well as data, a foresight vision of the metaprograming approach.

This is also related with Turing later interest in machine intelligence and learning in the broad field of Artificial Intelligence. In Manchester, where he got his first full academic post, he and the small group around him published articles under the heading 'Digital computers applied to games' in 1953, which mark pioneering research into machine intelligence. But this lead made no impact on the fresh start to artificial intelligence made by Newell, Simon, Minsky and McCarthy in the United States. Nevertheless in his famous 1950 paper 'Computing machinery and intelligence' he presents the idea of an 'imitation game' also known as the Turing test, in which a human has to interact with 'someone' in a closer room through a teletype device and tell if it is a human. Turing says that if a machine can play the human role well, it can elude his human interactor in thinking his talking to a human rather a machine, then the machine must exhibit intelligence behavior, human intelligence. Turing predicts that by the final of 20th century we should be able to construct such a machine, a bold assumption that we are yet to achieve.

Nevertheless much of his other contributions to philosophy, logic, mathematics, and the emergent field of computation provided invaluable tools of thought that enable us to progress the state of civilization and maybe, in the proper time, the fulfillment of his vision about computers, intelligence and their expression in an artificial intelligence synthesis and in doing so perhaps we be able to know a little more about ourselfs and answer the primordial philosophical question about who we are.

Colossus Strikes Back

It seems that World War II computer Colossus is cracking codes again.