{title}

Back to notes

Lambda calculus

Keywords: programming, functional, logic
Date:
  • Lambda calculus was invented by Alonzo Church

  • Lambda calculus concerns the nature of a function from a computational perspective

    • "what is a function, from a computational perspective?"
  • Analogous to Turing's state machine, except functional (not state-based)

    • any Turing machine program can be converted into a lambda calculus program
  • A function is a small machine that takes an input, processes it, and produces an output

  • Functions are "black boxes", so we don't know or care about what happens inside, just what goes in and comes out

  • Functions are pure, so they have no internal state or side effects, simply producing an output from an input

"Church" notation

; overview:
λ<input>.<output(s)>

; an increment function:
λx.x+1

; a sum function (note that this takes two inputs):
λx.λy.x+y
; demonstration of increment function:
   (λx.x+1) 5
=> λ5.5+1
=> 6
; encoding "true" and "false":
TRUE = λx.λy.x
FALSE = λx.λy.y

; "not" operator (note, `FALSE` and `TRUE` are outputs):
λb.b FALSE TRUE

; applying the "not" operator to TRUE:
   (λb.b FALSE TRUE) TRUE
; expanded:
=> λ(λx.λy.x).λx.λy.x FALSE TRUE
; result:
=> FALSE
  • These definitions of true and false functions represent the concept of choosing between one thing and another

  • They can be used to implement all of the logical operators, not just the "not" operator

  • The most popular lambda calculus expression is the "Y combinator"

    • invented by Haskell Curry
    • a way to implement recursion in lambda calculus

Backlinks: