Update
This commit is contained in:
parent
f19efc7b70
commit
5604db85d2
24 changed files with 2048 additions and 2026 deletions
|
@ -1,18 +1,18 @@
|
|||
# Lambda Calculus
|
||||
|
||||
Lambda calculus is an extremely simple (one of the simplest possible), low-level [mathematical](math.md) system that can perform computation with mathematical [functions](function.md), and can in fact be used to describe and perform any conceivable computation. Lambda calculus provides a theoretical basis for **[functional programming languages](functional.md)** and is a **[model of computation](model_of_computation.md)** similar to e.g. a [Turing machine](turing_machine.md) or [interaction nets](interaction_net.md) -- lambda calculus has actually exactly the same computational power as a Turing machine, which is the greatest possible computational power, and so these systems are alternatives to one another. Lambda calculus can also be viewed as a **primitive [programming language](programming_language.md)**, however its extreme simplicity (for example the lack of even such basic concepts as [numbers](number.md)) doesn't allow its pure form to be used for practical programming, it is more of a mathematical tool for studying computers [theoretically](compsci.md), constructing [proofs](proof.md) etc. The system is a result of searching for most [minimal](minimalism.md) systems capable of computation, just like the most essential physics equations come from searching for the most basic rules of our [Universe](universe.md). Nevertheless anything that can be programmed in any classic programming language can in theory be also programmed in lambda calculus.
|
||||
Lambda calculus is an extremely simple (one of the simplest possible), low-level [mathematical](math.md) system capable of performing computation with mathematical [functions](function.md), and can in fact be used to describe and carry out any conceivable computation. Lambda calculus provides a theoretical basis for **[functional programming languages](functional.md)** and is a **[model of computation](model_of_computation.md)** just like for example the [Turing machine](turing_machine.md) or [interaction nets](interaction_net.md) -- lambda calculus has in fact exactly the same computational power as a Turing machine, which is the greatest possible, and so these systems are alternatives to one another. Lambda calculus can also be viewed as a **primitive [programming language](programming_language.md)**, however its immense simplicity (for example the lack of even such basic concepts as [numbers](number.md)) doesn't allow its pure form to be used for practical programming, it is more of a mathematical tool for studying computers [theoretically](compsci.md), constructing [proofs](proof.md) etc. The system is a result of the search for the most [minimal](minimalism.md) systems capable of computation, just like the most essential physics equations emerge from searching for the most elementary rules of our [Universe](universe.md). Nevertheless anything that can be programmed in any classic programming language can in theory be also programmed in lambda calculus.
|
||||
|
||||
While Turing machines use memory cells as the medium to carry out computation -- which closely imitates the "number crouching" of real life computers -- lambda calculus instead performs computation solely by simplifying an expression made of pure mathematical functions -- that means there are no [global variables](variable.md) or [side effects](side_effect.md) (the role of memory is essentially replaced by the expression itself, the lambda expression is both the program and its memory at the same time). It has to be stressed that the functions in question are mathematical functions, also called **pure functions**, NOT functions we know from programming (which can do all kinds of nasty stuff). A pure function cannot have any side effects such as changing global state and its result also cannot depend on any global state or [randomness](randomness.md), the only thing a pure function can do is return a value, and this value has to always be the same if the arguments to the function are same. In addition to this the pure mathematical functions are yet much simpler than those we encounter in high school, there are no algebraic operators or numbers, just symbols.
|
||||
While Turing machines use memory cells as the medium supporting computation -- which closely imitates the "number crouching" of real life computers -- lambda calculus instead performs computation solely by simplifying an expression made of pure mathematical functions -- that means there are no [global variables](variable.md) or [side effects](side_effect.md) (the role of memory is essentially replaced by the expression itself, the lambda expression is both the program and its memory at the same time). It has to be stressed that the functions in question are mathematical functions, also called **pure functions**, NOT functions we know from programming (which can do all kinds of nasty stuff). A pure function cannot have any side effects such as changing global state and its result also cannot depend on any global state or [randomness](randomness.md), the only thing a pure function can do is return a value, and this value has to always be the same if the arguments to the function are same. In addition to this the pure mathematical functions are yet much simpler than those we encounter in high school, there are no algebraic operators or numbers, just symbols.
|
||||
|
||||
## How It Works
|
||||
|
||||
(For simplicity we'll use pure ASCII text. Let the letters L, A and B signify the Greek letters lambda, alpha and beta.)
|
||||
(For the sake of simplicity we'll rely on pure ASCII text. Let the letters L, A and B signify the Greek letters lambda, alpha and beta.)
|
||||
|
||||
Lambda calculus is extremely simple in its definition, but it may not be so simple to learn to understand it. Most students don't get it the first time, so don't worry :)
|
||||
Lambda calculus is exceptionally simple in its definition, but it may not be so simple to grasp. Most students don't get it the first time, so don't worry :)
|
||||
|
||||
In lambda calculus function have no names, they are what we'd call anonymous functions or lambdas in programming (now you know why they're called lambdas).
|
||||
|
||||
Computations in lambda calculus don't work with numbers but with sequences of symbols, i.e. the computation can be imagined as manipulating the text string of the program itself with operations that can intuitively just be seen as "search/replace". That is we start with a program (text) that then gets transformed by simple rules over and over before reaching some final form -- the result of the computation. If you know some programming language already, the notation of lambda calculus will seem familiar to functions you already know from programming (functions, their bodies, arguments, variables, ...), but BEWARE, this will also confuse you; functions in lambda calculus are a little different (much simpler) than those in traditional languages; e.g. you shouldn't imagine that variables and function arguments represent numbers -- they are really just "text symbols", all we're doing with lambda calculus is really manipulating text with very simple rules. Things like numbers, their addition etc. don't exist at the basic level of lambda calculus, they have to be implemented (see later). This is on purpose ([feature](feature.md), not a [bug](bug.md)), lambda calculus is really trying to explore how simple we can make a system to still keep it as powerful as a Turing machine.
|
||||
Computations in lambda calculus don't work with numbers but with sequences of symbols, i.e. the computation can be imagined as manipulating the text string of the program itself with operations that can intuitively just be seen as "search/replace". That is we start with a program (text) that subsequently gets transformed by simple rules over and over before reaching a final form -- the result of the computation. If you know some programming language already, the notation of lambda calculus will seem familiar to functions you already know from programming (functions, their bodies, arguments, variables, ...), but BEWARE, this will also confuse you; functions in lambda calculus are a little different (much simpler) than those in traditional languages; e.g. you shouldn't imagine that variables and function arguments represent numbers -- they are really just "text symbols", all we're doing with lambda calculus is really manipulating text with very simple rules. Things like numbers, their addition etc. don't exist at the basic level of lambda calculus, they have to be implemented (see later). This is on purpose ([feature](feature.md), not a [bug](bug.md)), lambda calculus is really trying to explore how simple we can make a system to still keep it as powerful as a Turing machine.
|
||||
|
||||
In lambda calculus an expression, also a **lambda term** or "program" if you will, consists only of three types of [syntactical](syntax.md) constructs:
|
||||
|
||||
|
@ -48,7 +48,7 @@ Let's take a complete **example**. We'll use the above shown increment function
|
|||
(Lf.Lx.fx) B-reduction
|
||||
```
|
||||
|
||||
We see we've gotten the representation of number 1.
|
||||
We see we've gotten the representation of the number 1.
|
||||
|
||||
TODO: C code
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue