lambda.md

λ-Complete

Introduction

In mathematical logic, the lambda calculus (also written as $\lambda-Calculus$) is a formal system for expressing computation based on function abstraction and application using variable binding and substitution.

lλbmdλ cλlculus?

λ-calculus consists of constructing lambda terms and performing reduction operations on them. A term is defined as any valid lambda calculus expression. In the simplest form of lambda calculus, terms are built using only the rules below.

This is just about the untyped λ-calculus.

Expressions

$x$: A variable is a character or string representing a parameter.

$(\lambda x.M)$: A lambda abstraction is a function definition, taking as input the bound variable x (between the $\lambda$ and the punctum/dot .) and returning the body $M$.

$(M~ ~N)$: An application, applying a function $M$ to an argument $N$. Both $M$ and $N$ are lambda terms.

Turing complete

Lambda calculus is Turing complete, that is, it is a universal model of computation that can be used to simulate any Turing machine. Its namesake, the Greek letter lambda (λ), is used in lambda expressions and lambda terms to denote binding a variable in a function.

Definition of computing system

TRUE=λx.λy.x
FALSE=λx.λy.y
AND=λx.λy.((x y) (λx.λy.y))
OR=λx.λy.((x λx.λy.x) y)
NOT=λx.(x λx.λy.y) λx.λy.x

0=λf.λx.x
1=λf.λx.f x
2=λf.λx.f(f x)
3=λf.λx.f(f(f x))
...
SUCC=λn.λf.λx.(f ((n f) x))
PRED=λn.λf.λx.n(λg.λh.h(g f))(λu.x)(λu.u)
+=λm.λn.λf.λx.m f (n f x)
-=λm.λn.(m PRED) n
*=λm.λn.λf.m (n f)
^=λm.λn.m n
!=λn.λf.n(λf.λn.n(f(λf.λx.n f(f x))))(λx.f)(λx.x)
Ω=(λx.x x)(λx.x x)

Because there are too many formulas, I did not use LaTeX formatting.

β-Reduction

Just like this:

     (((λx.λy.x y) 1) 2)
=β=>          1 2
=β=> (λf.λx.f x (λf.λx.f(f x)))
=β=> (λf.λx.f(f x)) x
=β=> λf.λx.f(f x)
FINAL: λf.λx.f(f x) => 2

But when it's Ω:

    (λx.x x)(λx.x x)
=β=>(λx.x x)(λx.x x)
=β=>(λx.x x)(λx.x x)
=β=>(λx.x x)(λx.x x)
=β=>(λx.x x)(λx.x x)
...

Quine?

Fibbonacci

A Fibbonacci program can be this: λn.λf.n(λc.λa.λb.c b(λx.a (b x)))(λx.λy.x)(λx.x)f.

That's weird...

IF...ELSE expression

IF condition:
    f(x)
ELSE:
    g(x)

Represented as $\lambda$:

$$ IFELSE=\lambda c.\lambda f.\lambda g.(c~ ~ f ~ ~g) $$

$$ IF=\lambda c.\lambda f.(c~ f ~0) $$

Only the selection properties of True and False were used.

---

So you can use those expressions to write anything. Yes, $\lambda-nything!$

You can also use $\lambda$ to write a $\lambda$-interpreter.
For example, @tromp 's Binary Lambda Calculus Interpreter(IOCCC-2012/Most functional):

       Int L[A],m,b,*D=A,
        *c,*a=L,C,*U=L,u;s
         (_){u--&&s(a=*a);}
          char*B,I,O;S(){b=b
           --?b:m|read(0,&I,1
            )-1;return~I>>b&1;
             }k(l,u){for(;l<=u;
              U-L<A?*U++=46^l++[
               "-,&,,/.--/,:-,'/"
               ".-,-,,/.-,*,//..,"
              ]:exit(5));}p(Int*m){
             return!*U?*m=S()?U++,!S
            ()?m[1]=p(++U),2:3:1,p(U)
           :S()?U+=2:p(U[1]++),U-m;}x(
          c){k(7*!b,9);*U++=b&&S();c&&x
         (b);}d(Int*l){--l[1]||d(l[d(*l),
        *l=B,B=l,2]);}main(e){for(k(10,33
       ),a[4]-=m=e-2&7,a[23]=p(U),b=0;;e-2
      ?e?e-3?s(D=a),C=a  [3],++1[a=a[2]],d(
     D):c?D=c,c=*D,*D=    a,a=D:exit(L[C+1])
    :C--<23?C=u+m&1?O      =O+O|C&1,9:write(m
   ||(O=C+28),&O,1)+        1:(S(),x(0<b++?k(0,
  6),U[-5]=96:0)):(          D=B?B:calloc(4,X))
 ?B=*D,*D=c,c=D,D[            2]=a,a[++D[1]]++,D
[3]=++C+u:exit(6)              )e=L[C++],u=L[C];}

Also have BLC version:

      01010001
       10100000
        00010101
         10000000
          00011110
           00010111
            11100111
             10000101
              11001111
              000000111
             10000101101
            1011100111110
           000111110000101
          11101001 11010010
         11001110   00011011
        00001011     11100001
       11110000       11100110
      11110111         11001111
     01110110           00011001
    00011010             00011010