# Functional Programming
> Lecture slide: [click here](https://www.kdocs.cn/p/105324573301)
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. 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
* [Yet Another Scheme Tutorial](https://www.kancloud.cn/kancloud/yast-cn/64461) (Chinese)
`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
```scheme
(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; given()
```
`(cadr xs)` is `(car (cdr xs))`\
`(cdddr xs)` is `(cdr (cdr (cdr xs)))`
#### List building
```scheme
(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.
```scheme
(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
```scheme
(if condition expr1 expr2)
```
#### Generalized form
```scheme
(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.
```scheme
; (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:
```scheme
(let
((v1 init1) (v2 init2) ... (vn initn))
body)
```
---
# Agent Instructions: Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.
Perform an HTTP GET request on the current page URL with the `ask` query parameter:
```
GET https://notes.dizy.cc/programming-languages/functional-programming.md?ask=
```
The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.
Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.