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)
A Turing complete model of computation that has its syntax and reduction rules. It is the basis for functional languages.
ç-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)))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.Renaming bound variables. Usually used to avoid name collision.
λy.(...y...) → λw.(...w...)
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.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.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.
η(eta)-reduction is used to eliminate useless variables.
(λx.M x) → M
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
symbol?
number?
pair?
list?
null?
zero?(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.(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)))(cons 'this '(that and the other))
=> (this that and the other)
(cons 'a '())
=> (a)
shortcut:
(list 'a 'b 'c 'd 'e)quote or ' to describe data.(quote (1 2 3 4))
(quote (Baby needs a new pair of shoes))
'(this also works)
#t: true.
#f: false.Any value not equal to
#f is considered to be true.(if condition expr1 expr2)
(cond
(pred1 expr1)
(pred2 expr2)
...
(else exprn))
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))
Basic
let skeleton:(let
((v1 init1) (v2 init2) ... (vn initn))
body)
Last modified 1yr ago