Lambda Calculus – The Universal Programming Language – Why λ Calculus?



Lambda Calculus – The Universal Programming Language – Why λ Calculus?

0 0


lambda-calculus-presentation


On Github whitehead1415 / lambda-calculus-presentation

Lambda Calculus

The Universal Programming Language

Why λ Calculus?

  • Encoding of logic
    • Typed λ calculus
    • Howard-Curry Isomorphism
  • Transparency {Location, Execution, Sugar}

Why Learn λ Calculus?

  • Understanding of reduction strategies
  • Equational Reasoning = Easy to refactor
  • Pure Functional programming = λ + Sugar
-- Definition of λ Calculus
<expression> ::= <name> | <function> | <application>

<function> ::= λ<name>.<body>

<body> ::= <expression>

<application> ::= (<expression> <expression>)

-- Examples
λx.x
λfoo.λbar.foo
λf.λa.(f a)
-- Defining functions 

def identity = ???
def self_apply = ???
def apply = ???
def true = ???
def false = ???
def identity = λx.x
def self_apply = λs.(s s)
def apply = λf.λa(f a)
def true = λfirst.λsecond.first
def false = λfirst.λsecond.second
-- Mmmmm... Sugar!
identity x = x
self_apply s = s s
apply f a = f a
true first second = first
false first second = second
def cond = ???
def not = ???
def and = ???
def or = ???
def cond e1 e2 c = c e1 e2
def not x = cond false true x
def and x y = cond y false x
def or x y = cond true y x
--Natural Numbers
def zero = identity
def succ n s = s false n
Lambda Calculus The Universal Programming Language