Notes (LCBB 01/07): Introduction
1 Introduction
The Entsheidungsproblem: The decision problem. Loosely speaking, whether it s possible to to come up with a general procedure to determine if statements are valid in some formal system.
Take arithmetic as an example of a formal system. It has statements “1 + 1 = 2”, “5 > 3” and so on. Some statements are true, like “1 + 1 = 2”, while others are false, like “1 = 0”. Given an arbitrary statement X, is there a function D such that D(X) returns True if X is true and False if X is false? That’s the decision problem. And the answer is no. No such function exists, nor can it exist.
lambda calculus: A formal system developed by Alonzo Church in 1936. Church proved the decision problem in the negative by showing that no function exists that can determine whether two expression in the lambda calculus were equivalent.
Turing Machines: A formal system developed by Alan Turing in 1936. Turing proved the decision problem in the negative by showing that no function exists that can determine whether a Turing machine will halt or run forever.
Church-Turing Thesis: The lambda calculus and Turing machines have equivalent power as formal systems. Any function defined in one can be defined in the other.
Von Neumann Machines: Turing machines with random access memory (RAM). The usual formulation of a Turing machine has sequential access memory on a tape. Most modern computers are hardware Von Neumann Machines.
Assembly languages and imperative programming languages are based on Turing machines, and are generally built around sequences of statements and commands.
Functional programming languages are based on the lambda calculus and are built around expression reduction.
Reduction Machine: A machine designed to execute expressions in a functional language. Such machines have been built in the flesh (in the silicon?), such as the Lisp Machines but are generally rare. Most functional programming languages compile to Von Neumann Machine instructions.
Reduction and functional programming
functional program An expression E that can be reduced. Reduction of E is equivalent to computing the function that E represents. E is reduced by some rewrite rules, such that a part P of E is replaced with P':
E[P] -> E[P']as long as the replacement P -> P' is implied by the rewrite rules.
Church-Rosser property: If applying the rewrite rules in a reduction system can be done in any order and yield the same expression, the reduction system satisfies the Church-Rosser property.
Application and abstraction
application: A pair of expressions F and A where F considered a function and A is the input to that function.
abstraction: An expression parameterized on some variable. The abstraction \x.M can be considered the function from x to M[x], where M[x] is the expression M containing some (or no) instances of x.
Beta reduction: When an abstraction is the first expression in an application:
(\x.M) Nthen the application can be reduced by replaceing each instance of x in the expression M with N:
(\x.M) N = M[x := N]Free and bound variables
binding a variable: Every abstraction binds some variable. Variables can be either free or bound. Free variables are those that are not bound by any abstraction. When an abstraction is applied, only the variables bound by that abstraction are substituted with the input.
(\x. y x (\x. x)) N = y N (\x. x)The x in \x. x is bound by inner \x. abstraction head, not the outer one. The expression N is only substituted for the variables bound by the abstraction being applied, not those bound by any other.
Functions of more arguments
currying: A construction of some function f that depends on multiple arguments by the repeated application of functions of single arguments. Suppose f(x, y) is a function that depends on both x and y. Then f can be constructed from some function F, such that
F(x) = F_x
F_x(y) = f(x, y)In the lambda calculus:
\x.(F x) = F_x
\y.(F_x y) = f(x, y)So that,
(\x.\y.(F x) y) x y = (\y. F_x y) y = f(x, y)In other words, we transform f which mapped from the space of pairs (x,y) to some output space, into the function F which maps from the space of xs to the space of functions F_x, which are the functions that map from space of ys to the output space.
In this way, we can build functions of multiple arguments out of chaining together functions of single arguments.