From 8676459adb14d9830259c83edbfcbc0988277d49 Mon Sep 17 00:00:00 2001 From: Max Sun Date: Wed, 18 Oct 2017 23:55:43 -0700 Subject: Added lambda calculus --- lambda-calculus.html.markdown | 121 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 121 insertions(+) create mode 100644 lambda-calculus.html.markdown (limited to 'lambda-calculus.html.markdown') diff --git a/lambda-calculus.html.markdown b/lambda-calculus.html.markdown new file mode 100644 index 00000000..6103c015 --- /dev/null +++ b/lambda-calculus.html.markdown @@ -0,0 +1,121 @@ +--- +category: Algorithms & Data Structures +name: Lambda Calculus +contributors: + - ["Max Sun", "http://github.com/maxsun"] +--- + +# Lambda Calculus + +Lambda calculus (λ-calculus), originally created by +[Alonzo Church](https://en.wikipedia.org/wiki/Alonzo_Church), +is the world's smallest programming language. +Despite not having numbers, strings, booleans, or any non-function datatype, +lambda calculus can be used to represent any Turing Machine! + +Lambda calculus is composed of 3 elements: **variables**, **functions**, and +**applications**. + + +| Name | Syntax | Example | Explanation | +|-------------|------------------------------------|-----------|-----------------------------------------------| +| Variable | `` | `x` | a variable named "x" | +| Function | `λ.` | `λx.x` | a function with parameter "x" and body "x" | +| Application | `` | `(λx.x)a` | calling the function "λx.x" with argument "a" | + +The most basic function is the identity function: `λx.x` which is equivalent to +`f(x) = x`. The first "x" is the function's argument, and the second is the +body of the function. + +## Free vs. Bound Variables: + +- In the function `λx.x`, "x" is called a bound variable because it is both in +the body of the function and a parameter. +- In `λx.y`, "y" is called a free variable because it is never declared before hand. + +## Evaluation: + +Evaluation is done via +[β-Reduction](https://en.wikipedia.org/wiki/Lambda_calculus#Beta_reduction), +which is essentially lexically-scoped substitution. + +When evaluating the +expression `(λx.x)a`, we replace all occurences of "x" in the function's body +with "a". + +- `(λx.x)a` evaluates to: `a` +- `(λx.y)a` evaluates to: `y` + +You can even create higher-order functions: + +- `(λx.(λy.x))a` evaluates to: `λy.a` + +Although lambda calculus traditionally supports only single parameter +functions, we can create multi-parameter functions using a technique called +[currying](https://en.wikipedia.org/wiki/Currying). + +- `(λx.λy.λz.xyz)` is equivalent to `f(x, y, z) = x(y(z))` + +Sometimes `λxy.` is used interchangeably with: `λx.λy.` + +---- + +It's important to recognize that traditional **lambda calculus doesn't have +numbers, characters, or any non-function datatype!** + +## Boolean Logic: + +There is no "True" or "False" in lambda calculus. There isn't even a 1 or 0. + +Instead: + +`T` is represented by: `λx.λy.x` + +`F` is represented by: `λx.λy.y` + +First, we can define an "if" function `λbtf` that +returns `t` if `b` is True and `f` if `b` is False + +`IF` is equivalent to: `λb.λt.λf.b t f` + +Using `IF`, we can define the basic boolean logic operators: + +`a AND b` is equivalent to: `λab.IF a b F` + +`a OR b` is equivalent to: `λab.IF a T b` + +`a NOT b` is equivalent to: `λa.IF a F T` + +*Note: `IF a b c` is essentially saying: `IF(a(b(c)))`* + +## Numbers: + +Although there are no numbers in lambda calculus, we can encode numbers using +[Church numerals](https://en.wikipedia.org/wiki/Church_encoding). + +For any number n: n = λf.fⁿ so: + +`0 = λf.λx.x` + +`1 = λf.λx.f x` + +`2 = λf.λx.f(f x)` + +`3 = λf.λx.f(f(f x))` + +To increment a Church numeral, +we use the successor function `S(n) = n + 1` which is: + +`S = λn.λf.λx.f((n f) x)` + +Using successor, we can define add: + +`ADD = λab.(a S)n` + +**Challenge:** try defining your own multiplication function! + +## For more advanced reading: + +1. [A Tutorial Introduction to the Lambda Calculus](http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf) +2. [Cornell CS 312 Recitation 26: The Lambda Calculus](http://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html) +3. [Wikipedia - Lambda Calculus](https://en.wikipedia.org/wiki/Lambda_calculus) \ No newline at end of file -- cgit v1.2.3 From 3ab2e88b4af9d072fbd2e0e2b9c0fe849d46892b Mon Sep 17 00:00:00 2001 From: YAN HUI HANG Date: Sun, 15 Jul 2018 15:33:01 +0800 Subject: SKI, SK and Iota --- lambda-calculus.html.markdown | 95 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 94 insertions(+), 1 deletion(-) (limited to 'lambda-calculus.html.markdown') diff --git a/lambda-calculus.html.markdown b/lambda-calculus.html.markdown index 6103c015..72ed78ba 100644 --- a/lambda-calculus.html.markdown +++ b/lambda-calculus.html.markdown @@ -3,6 +3,7 @@ category: Algorithms & Data Structures name: Lambda Calculus contributors: - ["Max Sun", "http://github.com/maxsun"] + - ["Yan Hui Hang", "http://github.com/yanhh0"] --- # Lambda Calculus @@ -114,8 +115,100 @@ Using successor, we can define add: **Challenge:** try defining your own multiplication function! +## Get even smaller: SKI, SK and Iota + +### SKI Combinator Calculus + +Let S, K, I be the following functions: + +`I x = x` + +`K x y = x` + +`S x y z = x z (y z)` + +We can convert an expression in the lambda calculus to an expression +in the SKI combinator calculus: + +1. `λx.x = I` +2. `λx.c = Kc` +3. `λx.(y z) = S (λx.y) (λx.z)` + +Take the church number 2 for example: + +`2 = λf.λx.f(f x)` + +For the inner part `λx.f(f x)`: +``` + λx.f(f x) += S (λx.f) (λx.(f x)) (case 3) += S (K f) (S (λx.f) (λx.x)) (case 2, 3) += S (K f) (S (K f) I) (case 2, 1) +``` + +So: +``` + 2 += λf.λx.f(f x) += λf.(S (K f) (S (K f) I)) += λf.((S (K f)) (S (K f) I)) += S (λf.(S (K f))) (λf.(S (K f) I)) (case 3) +``` + +For the first argument `λf.(S (K f))`: +``` + λf.(S (K f)) += S (λf.S) (λf.(K f)) (case 3) += S (K S) (S (λf.K) (λf.f)) (case 2, 3) += S (K S) (S (K K) I) (case 2, 3) +``` + +For the second argument `λf.(S (K f) I)`: +``` + λf.(S (K f) I) += λf.((S (K f)) I) += S (λf.(S (K f))) (λf.I) (case 3) += S (S (λf.S) (λf.(K f))) (K I) (case 2, 3) += S (S (K S) (S (λf.K) (λf.f))) (K I) (case 1, 3) += S (S (K S) (S (K K) I)) (K I) (case 1, 2) +``` + +Merging them up: +``` + 2 += S (λf.(S (K f))) (λf.(S (K f) I)) += S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)) +``` + +Expanding this, we would end up with the same expression for the +church number 2 again. + +### SK Combinator Calculus + +The SKI combinator calculus can still be reduced further. We can +remove the I combinator by noting that `I = SKK`. We can substitute +all `I`'s with `SKK`. + +### Iota Combinator + +The SK combinator calculus is still not minimal. Defining: + +``` +ι = λf.((f S) K) +``` + +We have: + +``` +I = ιι +K = ι(ιI) = ι(ι(ιι)) +S = ι(K) = ι(ι(ι(ιι))) +``` + ## For more advanced reading: 1. [A Tutorial Introduction to the Lambda Calculus](http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf) 2. [Cornell CS 312 Recitation 26: The Lambda Calculus](http://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html) -3. [Wikipedia - Lambda Calculus](https://en.wikipedia.org/wiki/Lambda_calculus) \ No newline at end of file +3. [Wikipedia - Lambda Calculus](https://en.wikipedia.org/wiki/Lambda_calculus) +4. [Wikipedia - SKI combinator calculus](https://en.wikipedia.org/wiki/SKI_combinator_calculus) +5. [Wikipedia - Iota and Jot](https://en.wikipedia.org/wiki/Iota_and_Jot) -- cgit v1.2.3 From 3a48077c16b2a7f083cd096cf146e16b9bcebdb1 Mon Sep 17 00:00:00 2001 From: Chris Zimmerman Date: Mon, 8 Oct 2018 13:57:53 -0400 Subject: Fixes lambda calculus evaluation formula by fixing associativity --- lambda-calculus.html.markdown | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lambda-calculus.html.markdown') diff --git a/lambda-calculus.html.markdown b/lambda-calculus.html.markdown index 72ed78ba..79dc20e7 100644 --- a/lambda-calculus.html.markdown +++ b/lambda-calculus.html.markdown @@ -55,7 +55,7 @@ Although lambda calculus traditionally supports only single parameter functions, we can create multi-parameter functions using a technique called [currying](https://en.wikipedia.org/wiki/Currying). -- `(λx.λy.λz.xyz)` is equivalent to `f(x, y, z) = x(y(z))` +- `(λx.λy.λz.xyz)` is equivalent to `f(x, y, z) = ((x y) z)` Sometimes `λxy.` is used interchangeably with: `λx.λy.` -- cgit v1.2.3 From 3f685318635b69d1492238378cd90c5908264b6c Mon Sep 17 00:00:00 2001 From: Chris Zimmerman Date: Tue, 9 Oct 2018 07:08:41 -0400 Subject: Fixes associativity issue in Lambda Calculus doc. --- lambda-calculus.html.markdown | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lambda-calculus.html.markdown') diff --git a/lambda-calculus.html.markdown b/lambda-calculus.html.markdown index 79dc20e7..3d080de7 100644 --- a/lambda-calculus.html.markdown +++ b/lambda-calculus.html.markdown @@ -87,7 +87,7 @@ Using `IF`, we can define the basic boolean logic operators: `a NOT b` is equivalent to: `λa.IF a F T` -*Note: `IF a b c` is essentially saying: `IF(a(b(c)))`* +*Note: `IF a b c` is essentially saying: `IF((a b) c)`* ## Numbers: -- cgit v1.2.3 From 34b2ab3a8b8ab345193585fd686e2ddbf6d36169 Mon Sep 17 00:00:00 2001 From: Nick Henderson Date: Wed, 21 Nov 2018 15:22:52 -0800 Subject: propose correction for ADD MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit I think it should be: `ADD = λab.(a S)b` --- lambda-calculus.html.markdown | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lambda-calculus.html.markdown') diff --git a/lambda-calculus.html.markdown b/lambda-calculus.html.markdown index 3d080de7..8343d62a 100644 --- a/lambda-calculus.html.markdown +++ b/lambda-calculus.html.markdown @@ -111,7 +111,7 @@ we use the successor function `S(n) = n + 1` which is: Using successor, we can define add: -`ADD = λab.(a S)n` +`ADD = λab.(a S)b` **Challenge:** try defining your own multiplication function! -- cgit v1.2.3 From ef11bde030bc530f713d35f1ff03a248ea658b56 Mon Sep 17 00:00:00 2001 From: nichijou Date: Sun, 17 Feb 2019 12:10:49 +0800 Subject: markdown syntax issue --- lambda-calculus.html.markdown | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'lambda-calculus.html.markdown') diff --git a/lambda-calculus.html.markdown b/lambda-calculus.html.markdown index 8343d62a..a5535d6c 100644 --- a/lambda-calculus.html.markdown +++ b/lambda-calculus.html.markdown @@ -139,6 +139,7 @@ Take the church number 2 for example: `2 = λf.λx.f(f x)` For the inner part `λx.f(f x)`: + ``` λx.f(f x) = S (λx.f) (λx.(f x)) (case 3) @@ -147,6 +148,7 @@ For the inner part `λx.f(f x)`: ``` So: + ``` 2 = λf.λx.f(f x) @@ -156,6 +158,7 @@ So: ``` For the first argument `λf.(S (K f))`: + ``` λf.(S (K f)) = S (λf.S) (λf.(K f)) (case 3) @@ -164,6 +167,7 @@ For the first argument `λf.(S (K f))`: ``` For the second argument `λf.(S (K f) I)`: + ``` λf.(S (K f) I) = λf.((S (K f)) I) @@ -174,6 +178,7 @@ For the second argument `λf.(S (K f) I)`: ``` Merging them up: + ``` 2 = S (λf.(S (K f))) (λf.(S (K f) I)) -- cgit v1.2.3 From 753325355a8e22b050fb32e3e48d74cb20d92403 Mon Sep 17 00:00:00 2001 From: Brian Berns Date: Sun, 17 Mar 2019 13:36:27 -0400 Subject: Update lambda-calculus.html.markdown --- lambda-calculus.html.markdown | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lambda-calculus.html.markdown') diff --git a/lambda-calculus.html.markdown b/lambda-calculus.html.markdown index a5535d6c..53a7a7cd 100644 --- a/lambda-calculus.html.markdown +++ b/lambda-calculus.html.markdown @@ -85,7 +85,7 @@ Using `IF`, we can define the basic boolean logic operators: `a OR b` is equivalent to: `λab.IF a T b` -`a NOT b` is equivalent to: `λa.IF a F T` +`NOT a` is equivalent to: `λa.IF a F T` *Note: `IF a b c` is essentially saying: `IF((a b) c)`* -- cgit v1.2.3