Find file
Fetching contributors…
Cannot retrieve contributors at this time
84 lines (42 sloc) 5.1 KB
= The Top =
High level programming is primarily focussed on describing ways of doing things, also known as "algorithms". To do high level programming, we need a language to describe these algoritms in a way that is unambiguous so that we can be sure that what we are saying is what we intend, and any computer that hypothetically might run the algorithm would be able to.
Unlike low-level programming, high-level programming is not tied to the inner workings of any particular computer. Instead, we build abstractions that desribe what we want done and then build programs to translate these abstractions into instructions for the computer. There may be many different lists of instructions that perform the exact same algorithm.
The language we will start off with for high-level programming is called the Untyped Lambda Calculus. We will start with this language because it has a very simple syntax. Syntax is the term for what symbols we use in a language and the ways that they can be put together.
The simplest program in the Untyped Lambda Calculus is:
This program represents the symbol `x`, nothing more, nothing less. Base symbols in the lambda calculus are usually represented by single letters.
The other construct in the lambda calculus is called a lambda abstraction, sometimes called a function:
A lambda abstraction is always the Greek letter lambda (λ, sometimes represented by \) followed by a single symbol, then a dot (.), then any valid Untyped Lambda Calculus program. Everything after the dot is considered to be part of the lambda abstration, until the end of the line. If we do not want this, we may use parentheses to clarify where the end is:
Finally, we may express something called an application. An application is any lambda abstration, followed by any valid Untyped Lambda Calculus program. We'll start with the simplest program, a single symbol:
So, what do these programs represent? Well, we already said what this program represents:
Intuitively, a lambda abstraction represents something which takes in some program, and returns some other program. For example, intuitively:
represents just the symbol `y`, because in the right hand side of (λx.x), the `x` is "bound" to represent whatever program the lambda abstraction is applied to. So in (λx.x)y, it is applied to `y`, so then the `x` represents `y` (some of you may recognise this as very similar to the mathematical function f(x) = x). The process we use to define this is called a "reduction", because we are "reducing" a program from something longer to something shorter by rewriting using certain rules. We will cover this more in depth later.
== α-equivalence ==
One of the fundamental principles of the lambda calculus is called "alpha equivalence". This principle is the idea that:
represent the same program. The idea is that the symbol we bind in a lambda abstraction doesn't matter, since it really just represents the program we are going to apply the abstraction to. This matters because in order to really understand most useful reductions, we will need to be able to rename some things.
By the same logic:
represent the same program. So do:
(λx.x y)
(λz.z y)
But these programs are not the same:
(λx.z y)
(λz.z y)
Because in the first one, the `z` in the body of the lambda abstraction represents `z`, but in the second it has been "bound" (or "captured") by the abstraction, such that it now represents the symbol that the abstraction will be applied to.
== Turing Completeness ==
The Untyped Lambda Calculus may seem to be so simplistic that it could never be useful, but in fact, the Church–Turing thesis says that this language can represent any algorithm which can be transformed into a series of steps for a machine to follow.
This gives rise to the idea of Turing Completeness. Formally, a computational system is Turing Complete if it can compte every Turing-computable function (that is, it can simulate a universal Turing machine). The Untyped Lambda Calculus can be shown to be able to compute every such function, which means that something is also Turing Complete if it can implement an interpreter for the Untyped Lambda Calculus. Additionally, the Untyped Lambda Calculus cannot compute *more* functions than a universal Turing machine, and so it is Turing Equivalent.
The Church–Turing thesis says that every algorithmic system of computation is either Turing Equivalent or is not Turing Complete. This thesis is unproven, but there is no evidence against it, mounting evidence for it, and it is generally accepted in Computer Science.
Many different facilities may be used in order to implement Turing Completeness. In practise, for low level lanugages, having both conditional branching and infinite mutable storage is sufficient for Turing Completeness. In practise, we ignore the requirement for infinite storage, so our ARMv6 assembly will be seen to be Turing Complete. This also means that computers based on the ARMv6 CPU can evaluate arbitrary Untyped Lambda Calculus expressions (modulo storage space limitations).