Lambda calculus -

Lambda calculus

programming, functional, logic
  • 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:

; an increment function:

; a sum function (note that this takes two inputs):
; 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):

; applying the "not" operator to TRUE:
; expanded:
=> λ(λx.λy.x).λx.λy.x FALSE TRUE
; result:
  • 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