📘
📘
📘
📘
Notes
Programming Languages
Search
K
Comment on page

# Functional Programming

Overview of the lambda calculus and Scheme.
Readings: Scott, ch. 10 (including 10.6.1 on the CD), Dybvig ch. 1,2 (optional)

## λ-Calculus

A Turing complete model of computation that has its syntax and reduction rules. It is the basis for functional languages.

### Syntax

ç-calculus has variables, abstraction and application.
Variables: lower-case letters. Such as `x`. Abstraction: (definition of function) `λx.M`, `x` being the function parameter, `M` being the function body. Application: (invocation of function) `M N`. Call function `M` with the argument `N`.
Abstraction is right-associative, application is left-associative. And application has precedence over abstraction. (For example,`λx. y λx. z` means `λx.(y (λx.z))`)

### Free and bound variables

In term `λx.M`, the scope of `x` is `M`. So, we call `x` bound in `M`. The variables that are not bound are free.

### α-conversion

Renaming bound variables. Usually used to avoid name collision.
λy.(...y...) → λw.(...w...)

### β-reduction

Applying the argument and calling the function.
(λx.M) N → [x→N]M
`[x→N]M` means `M` with all bound occurences of `x` replaced by `N`. Restriction: `N` should not have any free variables which are bound in `N`.

### Normal form

An expression that cannot be β-reduced any further is a normal form.
Not everything has a normal form. For example, `(λz.z z)(λz.z z)` reduces to itself which will result in infinite application.

### Evaluation strategies

Slide page 7
For example, `(λx.λy.yxx)((λx.x)(λy.z))`
1. 1.
normal-order: reduct the outermost "redex" first.
[x→(λx.x)(λy.z)](λy.yxx) → λy.y((λx.x)(λy.z))((λx.x)(λy.z)
2.applicative-order: arguments to a function evaluated first, from left to right.
(λx.λy.yxx)([x→(λy.z)]x) → (λx.λy.yxx)((λy.z))
Some observations:
• If a lambda reduction terminates, it terminates to the same reduced expression regardless of reduction order.
• If a terminating lambda reduction exists, normal order evaluation will terminate.

### η-reduction

η(eta)-reduction is used to eliminate useless variables.
(λx.M x) → M

### Computational power

The untyped λ-calculus is Turing complete.
Numbers and numerals: number is an abstract idea, numeral is the representation of a number.
Booleans:
TRUE ≡ λa.λb.a
FALSE ≡ λa.λb.b
IF ≡ λc.λt.λe.(cte)
AND ≡ λm.λn.λa.λb.m(nab)b
OR ≡ λm.λn.λa.λb.ma(nab)
NOT ≡ λm.λa.λb.mba
Arithmetic:
Some numerals
⌜0⌝ ≡ λfx.x
⌜1⌝ ≡ λfx.fx
⌜2⌝ ≡ λfx.f(fx)
⌜3⌝ ≡ λfx.f(f(fx))
Some operations
ISZERO ≡ λn.n(λx.FALSE)TRUE
SUCC ≡ λnfx.f(nfx) // n+1
PRED ≡ λn.n(λgk.(g⌜1⌝)(λu.PLUS(gk)⌜1⌝)k)(λv.⌜0⌝)⌜0⌝ // n-1
PLUS ≡ λmnfx.mf(nfx) // m+n
MULT ≡ λmnf.m(nf) // m*n
EXP ≡ λmn.nm // n^m
Iteration
MUL = λmn.m (ADD n) 0
EXP = λmn.m (MUL n) 1

## Scheme overview

`symbol?` `number?` `pair?` `list?` `null?` `zero?`

### List

`(cons 'a '(b))` => list `(a b)` `(cons 'a 'b)` => dotted pair `(a . b)`
`car`: get head of list. `cdr`: get rest of list. `cons`: perpend an element to a list. `'()`: null list.

#### List decomposition

(car '(this is a list of symbols))
=> this
(cdr '(this is a list of symbols))
=> (is a list of symbols)
(cdr '(this that))
=> (that) ; a list
(cdr '(singleton))
=> () ; the empty list
(car '())
=> Error: car expects argument of type<pair>; given()
`(cadr xs)` is `(car (cdr xs))` `(cdddr xs)` is `(cdr (cdr (cdr xs)))`

#### List building

(cons 'this '(that and the other))
=> (this that and the other)
(cons 'a '())
=> (a)
shortcut: `(list 'a 'b 'c 'd 'e)`

### Quoting data (`'...`)

`quote` or `'` to describe data.
(quote (1 2 3 4))
(quote (Baby needs a new pair of shoes))
'(this also works)

### Booleans

`#t`: true. `#f`: false.
Any value not equal to `#f` is considered to be true.

### Simple control structures

#### Conditional

(if condition expr1 expr2)

(cond
(pred1 expr1)
(pred2 expr2)
...
(else exprn))

### Global definitions

`define` is a special function that only can be used at the top level to create global variables.
; (define name value)
(define x 15)
(define sqr (lambda (n) (* n n))
; (define (name ...parameters) body)
(define (sqr n) (* n n))

### Locals: `let`, `let*` and `letrec`

Basic `let` skeleton:
(let
((v1 init1) (v2 init2) ... (vn initn))
body)