=================================
Functional programming

Functional langugaes such as Lisp, Scheme, FP, ML, Miranda, and Haskell
are an attempt to realize Church's lambda calculus in practical form as
a programming language.

The key idea: do everything by composing functions.  No mutable state;
no side effects.

Necessary features, many of which are missing in some imperative langs:
    1st class and high-order functions
    serious polymorphism
    powerful list facilities
    recursion
    structured function returns
    fully general aggregates
    garbage collection
Lisp also has
    homoiconography
    self-definition
    read-eval-print

Other functional languages: ML, Miranda, Haskell, FP.  Haskell is the
leading language for research in functional programming.

--------------------------

Introduction to programming in Scheme.

    (car '(1 2 3)) ==> 1
    ((car '(1 2 3))) ==> (1) => error

The '==>' arrow means 'evaluates to'.

Built-ins (Incomplete list)
    Boolean values #t and #f
    Numbers
    Lambda expressions (P596)
    Quoting
        (+ 3 4)             ==> 7
        (quote (+ 3 4))     ==> (+ 3 4)
        '(+ 3 4)            ==> (+ 3 4)
    Mechanisms for creating new scopes
        (let ((square (lambda (x) (* x x))) (plus +))
            (sqrt (plus (square a) (square b))))
        let*
        letrec
    Mechanisms for creating bindings in outer scope
        (define hypot (lambda (a b)
            (let ((square (lambda (x) (* x x))) (plus +))
                (sqrt (plus (square a) (square b))))))
    list operators
        car
        cdr
        cons
        list
    Conditional expressions
        (if (< 2 3) 4 5)    ==> 4
        (cond
            ((< 3 2) 1)
            ((< 4 3) 2)
            (else 3))       ==> 3
    Imperative stuff
        assignments
        sequencing  (begin)
        iteration
        I/O         (read, display)

--------------------------

More on Lists

| Formally, lists are really nested series of pairs, which can be
| written with 'dot' notation:
|     A.(B.(C.(D.())))
| In a "proper" list the second element of the last pair is always the
| empty list.
| This notation is really ugly, so the alternative:
|     (A B C D)
| is almost always used instead (though it doesn't work for improper lists).
| 

Lists as programs:
 
|     (define foo (lambda (a b)  
|         (lambda (x) (a (b x)))))
|     ((foo car cdr) '(1 2 3))        ==> 2
| 
|     (define bar (lambda (a b) 
|         (eval (list 'lambda '(x) (list a (list b 'x))) 
|             ())))
|     ((bar car cdr) '(1 2 3))        ==> 2
| 
| We say that Lisp is HOMOICONIC (so is Prolog).
| It can be implemented with a METACIRCULAR INTERPRETER.
| 
| Most functional languages are NOT homoiconic.
| 
| We can use meta-circularity to define the semantics of Scheme, formally.
| Suppose M is a denotational function mapping Scheme expressions to their
| meaning, where the meaning is a mathematical object.
| 
| Also suppose I is the Scheme interpreter (itself a Scheme expression).
| For all Scheme expressions E, M(E) = (M(I)) (E), or put another way,
| M(I) = M.
| 
| Now let H(F) = F(I) where F is any function that takes a Scheme
| expression as its argument.  We have H(M) = M(I) = M, so M is a *fixed
| point* of H.  We can use H and the tools of denotational semantics to
| obtain a rigorous definition of M.  (Beyond the scope of this course.)

--------------------------
Evaluation order

Applicative order
    what you're used to in imperative languages
    usually faster
Normal order
    like call-by-name: don't evaluate arg until you need it
    sometimes faster

In Scheme
    functions use applicative order
        defined with lambda
    special forms (aka macros) use normal order
        defined with syntax-rules

Solution to I/O which requires side effects:
    Streams and Monads
--------------------------
Higher-order functions

Take a function as argument, or return a function as a result.
Examples
    apply
        (apply + '(1 2 3)) ==> 6
    map
        (map * '(2 4 6) '(3 5 7)) ==> (6 20 42)
    compose 
        (define compose
            (lambda (f g)
                (lambda (x) (f (g x)))))
        (compose car cdr) '(1 2 3)) ==> 2

Currying (after Haskell Curry, the same guy Haskell is named after):

    (define curried-plus (lambda (a) (lambda (b) (+ a b))))
    ((curried-plus 3) 4)
        ==> 7
    (define plus-3 (curried-plus 3))
    (plus-3 4)
        ==> 7

    (define curry (lambda (f) (lambda (a) (lambda (b) (f a b)))))
    (((curry +) 3) 4)
        ==> 7
    (define curried-plus (curry +))

    (map (curried-plus 3) '(1 2 3))
        ==> (4 5 6)

--------------------------
| Lambda calculus
| 
| A notation/model of computation based on purely syntactic symbol
| manipulation, in which everything is a function.
| 
| Developed by Alonzo Church in the '30's as a model for computability
|     Church was one of a crowd that also included Chomsky, Turing,
|         Kleene, and Rosser
| 
| example lambda expressions
|     identity        Lx.x
|     const7          Lx.7
|     plus            Lx.Ly.x + y
|     square          Lx.x * x
|     hypot           Lx.Ly.sqrt (plus (square x) (square y))
| 
| Recursively, a lambda expression is
|     (1) a name,
|     (2) an abstraction consisting of a lambda, a name, a dot, and a
|     lambda expression,
|     (3) an application consisting of two adjacent lambda expressions
|     (juxtaposition means function application), or
|     (4) a parenthesized lambda expression.
| 
| Usually application associates left-to-right, so f A B means (f A) B,
| rather than f (A B).  Also, application has higher precedence than
| abstraction, so Lx.A B is Lx.(A B), rather than (Lx.A) B.  Note that
| ML follows these rules.
|
| These rules mean that the scope of the dot extends right all the way
| to the first unmatched right parentheses, or the end of the whole
| expression if there is no such parenthesis.
| | 
| free and bound variables
|     a variable is bound if it is introduced by a lambda.
|     For example, in Lx.Ly.(* x y) we have two nested lambda expressions.
|     x is free in the inner one (Ly.(* x y)), but bound in the outer.
|     Bindings have scopes, just like they do in programming languages.
| 
| evaluation of lambda expressions through
|     (1) substituting in arguments (beta reduction)
|        (Lx.times x x) y  =>  times y y
|     (2) renaming variables (alpha conversion)
|               (often to avoid naming conflicts)
|         (Lx.times x x) y  ==  (Lz.times z z) y
|     (3) extensionality (eta reduction/conversion)
|         (Lx.f x)  =>  f
| 
| ----------------
| Formalize everything in Lambda Calculus
| 
| Control Flow
| List Structure
| ----------------
| Recursive functions
| 
| Note that our usual specification of recursive functions uses names that
| are referred to recursively:
| 
|     factorial(n) = if n = 0 then 1 else n * factorial(n-1)
| 
| How do we do this in pure lambda calculus?
| Depends on the notion of fixed point.
| 
| Use beta abstraction to get
| 
|     factorial = (Lf.Ln if n = 0 then 1 else n * f(n-1)) factorial
| 
| This is of the form     factorial = F factorial
| What we need is a *fixed point* of F.
| 
| One can prove that Y F works, where Y == Lh.(Lx.h (x x))(Lx.h (x x)).
| 
| ----------------

=================================
Logic programming

----------------
Prolog

Horn Clause

functor
facts/axioms
rules/theorems
query/goal

A structure can play the role of a data structure or a predicate.  A
constant is either an ATOM or a NUMBER.  An atom is either what looks like
an identifier beginning with a lower-case letter, or a quoted character
string.  A number looks like an integer or real from some more ordinary
language.  A variable looks like an identifier beginning with an upper-case
letter.  There are no declarations.  All types are discovered implicitly.

The meaning of the statement is that the conjunction of the terms in the
body implies the head.  A clause with an empty body is called a FACT.  A
clause with an empty head is a QUERY, or top-level GOAL.  A clause with
both sides is a RULE.

The Prolog interpreter has a collection of facts and rules in its DATABASE.
Facts are axioms -- things the interpreter assumes to be true.

    mother(mary, fred).
        % you can either think of this as an predicate asserting that mary
        % is the mother of fred, or a data structure (tree) in which the
        % functor (atom) mother is the root, mary is the left child, and
        % fred is the right child.

Rules are theorems that allow the interpreter to infer things.
To be interesting, rules generally contain variables.

    employed(X) :- employs(Y,X).

can be read:
    for all X, X is employed if there exists a Y such that Y employs X.

The scope of a variable is the clause in which it appears.  Variables whose
first appearance is on the left hand side of the clause have implicit
universal quanitfiers.  Variables whose first appearance is in the body of
the clause have implicit existential quantifiers.

----------

Resolution
Unification
Lists
Arithmetic

----------

Search

The interpreter works by what is called BACKWARD CHAINING: it begins with
the thing it is trying to prove and works backwards looking for things that
would imply it, until it gets to facts.  It is also possible in theory to
work forward from the facts trying to see if any of the things you can
prove from them are what you were looking for, but that can be very
time-consuming.  Fancier logic languages use both kinds of chaining, with
special smarts or hints from the user to bound the searches.

See Fig. 11.4

We can visualize backtracking search as a tree in which the top-level goal is
the root and the leaves are facts.  The children of the root are all the
rules and facts with which the goal can unify.  The interpreter does an OR
across them: one of them must succeed in order for the goal to succeed.  The
children of a node in the second level of the tree are the terms in the body
of the rule.  The interpreter does an AND across these: all of them must
succeed in order for the parent to succeed.  The overall search tree then
consists of alternating AND and OR levels.

---------------------------------

Execution Order

PROLOG IS *NOT* PURELY DECLARATIVE.
    The ordering of the database and the left-to-right pursuit of
    subgoals gives a deterministic imperative semantics to searching
    and backtracking.

Changing the order of statements in the database can give you different
results.  It can lead to infinite loops.  It can certainly result in
inefficiency.

-------------------------------------
| Imperative control flow
| 
| To avoid unnecessary search (and even in some cases to get the logic to
| work right), the user is allowed in Prolog to outlaw specific instances
| of backtracking.  The cut ('!') is a special subgoal that always succeeds
| the first time, and CANNOT succeed again.  Putting it in a right hand
| side prevents attempts at re-satisfaction of subgoals to its left,
| including unification with the head of the rule.  Prolog programmers
| consider cut to be a necessary evil; it is as controversial as 'goto'.
| Consider
| 
|     member(X, [X|T]).
|     member(X, [H|T]) :- member(X, T).
| 
|     prime_candidate(X) :- member(X, candidates), prime(X).
| 
| If prime is really expensive to compute, we don't want to consider X twice
| just because it appears in candidates twice.
| 
|     member(X, [X|T]) :- !.
|         % cut commits us to this rule; won't let us try the next rule
|     member(X, [H|T]) :- member(X, T).
| 
----------------
Database Manipulation

-----------

first-order predicate calculus

Most statements can be written many ways.  That's great for people but a
nuissance for computers.  It turns out that if you make certain
restrictions on the format of statements you can prove theorems
mechanically.  That's what logic programming systems do.  Unfortunately,
the restrictions that we will put on our statements will not allow us to
handle most of the theorems you learned in math, but we will have a
surprising amount of power left anyway.

Clausal Form