Lambda

A lambda is an anonymous function, in that it takes in a value and produces a value without being bound to an identifier.

Todo

Important

lambda is a value, this means that lambda x in x evaluates to itself.

inc x = x + 1

x - formal parameter
x + 1 - body

inc 3

3 - actual parameter
inc 3 - application of inc to 3

Note

We can define bind using lambda as well

# Concrete Syntax
bind i = a in s == ((lambda i in s) a)

# Abstract Syntax
((Lambda i s) a) == (Bind i a s)

This is called a Derived Form. More on that in derived forms

Churches Lambda Calculus

Can represent any computable function
- Equivalent to Turing machine
- Basis for functional programming
Turing machines give rise to imperative programming
Lambda Calculus gives rise to function programming

Concrete Syntax

lambda x in x + x

Defines a function value over formal parameter x
Called a lambda or abstraction
Lambdas are values
From a logical perspective lambda introduces a variable

(l a)

Applies a function l to actual parameter or argument a
Called an application of simply app
From a logical perspective, app eliminates a variable.

Alternate Concrete Syntaxes:

$λ x . s$ = lambda x in s

Examples

Currying:

(((lambda x in (lambda y in x+y)) 3 ) 2)
== (lambda y in 3+y) 2
== 3 + 2
== 5

Higher Order Function (Almost):

((lambda x in (x 3)) (lambda x in x))
== [x->(lambda x in x)](x 3)
== (lambda x in x) 3
== 3

Named Lambda:

bind inc = (lambda x in x+1) in (inc 3)

Inference Rules

Beta

\frac{f ⇓ (lambda i in s) a ⇓ v_{a} [i \to v_{a}] s ⇓ v_{s}}{(f a) ⇓ v_{s}}

LambdaE

\frac{}{lambda i in s ⇓ lambda i in s}

Definitions

First Order Functions - Cannot take other functions as arguments. Have special representation in the language that is not accessible.
Higher Order Functions - Can take functions as argument. Can return functions.
First Class Functions - Functions are values like any other value in the language.

Lambda Calculus

$Ω$ - combinator

(lambda x in (x x)) (lambda y in (y y))
-> (lambda y in (y y)) (lambda y in (y y))

Church vs Turing

Turing Machines operate on the principle of a stateful design. That is, state has to be manipulated to calculate values.

Churches Lambda Calculus operates on the principle of stateless design. There is no state in functional language.

Concrete Syntax

LC :: | id
	  | lambda id in LC
	  | (LC LC)

Inference Rules

Call by name

\frac{f ⇓ lambda i in s [i \to a] s ⇓ v_{s}}{(f a) ⇓ v_{s}}

Note

Call by name defers evaluation of a function's arguments until they are used in the function itself. This is also called lazy evaluation.

Call by value

\frac{f ⇓ (λ i . s) a ⇓ v_{a} [i \to v_{a}] s ⇓ v_{s}}{(f a) ⇓ v_{s}}

Evaluation

Using substitution

evalM (Lambda i s) = return (Lambda i s)
-- Eval App with Call by Value
evalM (App f a) = do { (Lambda i s) <- evalM f;
					   a' <- evalM a; -- Remove this line to Call by Name
					   evalM (subst i a' s)
					  }
evalM (Bind i a s) = do { a' <- eval a
						  evalM (subst i a' s)
						 }
-- Define bind with App
evalM (Bind i a s) = evalM (App (Lambda i s) a)

Using environment (deferred substitution)

Env = [(string, FBAE)]

eval e (Lambda i s) = (Lambda i s)
eval e (App f a) = do { (Lambda i s) <- eval e f;
                        a' <- eval e a;
                        eval (i,a'):e s
                       }
eval e (Id i) = lookup i e

Warning

This creates an issue with scoping of variables.

The inference rules we defined are developed for static scoping. However the deferred substitution interpreter we just defined here uses dynamic scoping.

Static v.s. Dynamic Scoping

Static Scoping - Identifier scope in a lambda is the scope where a lambda is defined

Dynamic Scoping - Identifier scope in a lambda is the scope where lambda is used

To fix this when using deferred substitution we just add a copy of the environment to the environment. In most other languages we just add a pointer to some stack space before function was defined. This leads us to closures.

Immediate substitution => Static scoping
Deferred substitution => Dynamic scoping
Deferred substitution + Closures => Static scoping