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