Lecture 19/20

Functional Programming

Lambda Calculus (Turing complete)

  exp := x            (* a variable *)
       | \x.exp       (* functional abstraction *)
       | exp exp      (* function application *)
       | exp + exp    
       | n            (* upto here is just abstract syntax *) 
       | (exp)        (* by liberally inserting parentheses => grammar *)


left association: f x y means (f x) y
. is tigher:      \x.f x  means \x.(f x)



            ------ Free variables
            |
            v
(\x. x + x) x
  ^  ^   ^
  |  |   |
  |  -------------> bond variables
  |
  ---------> binding occurrance

  FV(M) = free variables in expression set M

  e.g., 
   
       FV(x) = {x}
       FV(MN) = FV(M) U FV(N)
       FV(\x.M) = FV(M) - {x}
       FV((\f. f g x)(\x. x y)) = {f,x,y}

  substitution: substitute free variable x in M to N

      M[ x -> N]

  e.g.,   (x + x) [ x -> 5] = 5 + 5

        (\x. x+x) [ x -> 1+2] = \x. x+x
        ^^^^^^^^^             ^
            |                 |
          no free variables --


  rules:  x [ x -> N] = N
          y [ x -> N] = y           (x != y)
       (MM')[ x -> N] = M [ x-> N] M' [ x -> N]
       (\x.M) [ x -> N] = (\x.M)
       (\y.M) [ x -> N] = \y.(M [ x -> N])
        
        e.g.,  (\y.x) [ x -> y] = \y.y
                             ^
                             |
                             |
                             variables free in y should stay free. 
                             if bond, it's called name capture, which 
                             should be avoided.                             

   alpha, beta, and eta rules (defining equavilent classes in functions)

   Three properties for equivalent relationships 

     - reflectivity   M = M

     - symmetry      

                M = N 
              ----------
                N = M

     - transitivity   
 
               M = M' M' = M''
             ------------------
                 M = M''


   alpha rule (renaming): a name of a local variable doesn't matter: changing to 
                          another name* gives an equivalent expression 
      * should avoid name capture.

      \x.M = \y. (M[x->y])  where y no in FV(M)


    e.g.,   \x.(\x.x)x = \y.(\x.x)y


   properties of alpha rule:

        M = M'
      ------------
      \x.M = \x.M'




       M = M'  N = N'
    ------------------
          MN = M'N'



    beta rule:

           (\x.M)N = M[x->N]

           e.g.,   (\x.x+x)5 = 5+5
                   (\x.y)(1+2) = y


      properties:

             M = M'
          ----------
          \x.M = \x.M'

      Analogy of micro in C language:


         problem 1

         # define double(n) 2*n

             double(5+7) is parsed as 2*5+7. Due to the precedence of * and +, 2*5+7 will be
              interpreted as (2*5)+7, whereas what you really want is 2*(5+7)


         problem 2
           
         # define swap(x,y)  { int tmp; tmp=x; x=y; y=tmp;}

           swap(tmp, foo) will be parsed as

              {int tmp; tmp=tmp; ....}
                        ^^^^^^^
                           |
                           name capture



      These two problems are avoided in beta rule by
        1) parentheses are automatically inserted since we are dealing with abstract syntax

        2) name capture are avoided by the side condition in alpha and beta rules.


    eta rule (get rid of "surplus" abstraction):

         \x.Mx = M  where x not in FV(M)


       e.g.,
              fun add x y = x + y
              val inc = fn n => add 1 n
              val inc = add 1

       Note: 1. the side condition should be met. Otherwise, 
       e.g., 
             val double = fn n => add n n
                                  ^^^^^
                                    M
             val double = add n        
                          ^^^^^
                            |
                            n is not defined!


             2. situations where eta rule doesn't gain

                 e.g.,  val f = fn x => slow x
                        val f = slow



      Equivalence does not have directionality, evaluation does.

      beta redution:

          (\x.M)N -> M[x->N]


           M -> M'
         -------------
         \x.M -> \x.M'


           M -> M'
         -----------
          MN -> M'N



           N -> N'
         ----------
          MN -> MN'


      Normal form: An expression where no beta reduction can be done.


         e.g., 
                  (\x.x)((\y.z)a)
                         -------
                  ---------------

             ->   (\x.x)z
                  -------
             ->   z

           and z is a normal form since it can not be further reduced

           Redex: a place in an expression where a beta reduction can be done
           Note: redexes are underlined in aforementioned example.

      Question: does it matter with different order that beta reductions are done
                when multiple redexes exist?

      Answer: No.

      Church-Rosser Theorem:  Normal forms are unique.

               M
              / \
             /   \
            /     \
           M1      M2
            \     /
           * \   /*
              \ /

               M'
       
        where * means zero or more beta reductions

      Therefore, all paths will lead to the same normal form if the paths can terminate.


      There are expressions that do not have normal form

        e.g., 
                (\x.xx)(\x.xx)
                --------------

             -> (\x.xx)(\x.xx)
           
             -> ...


          "Bottom" is used to stand for expression that does not halt

          (\y.z)Bottom
                ------
          ------------


     choose outer redex -> z 

     choose inner redex -> (\y.z)Bottom

     Therefore, if keep choosing inner redex, you never end.



     Strategies to choose redexes for beta-reduction

       - leftmost, inner-most  (applicative order)
       - leftmost, outer-most  (normal order)


     Theorem: Normal order reduction always leads to a normal form if one exists.


      Note:

        1. Normal order may be inefficient

           e.g., (where argument is duplicated)

                    (\x.xx)slow
                           ----
                    -----------

              ->  slow slow


        2. not always inefficient.

           e.g., (when argument is not used)

                (\x.z)slow
                      ----
                ----------
  
           ->   z


       3. applicative order reduction (AOR) is equivalent to call-by-value (CBV)
          normal order reduction (NOR) is equivalent to call-by-name (CBN)


       4. both CBV and CBN do not evaluate under lambdas. but NOR will evaluate even under lambdas.

          e.g.,

               (\x.(\y.y)x)((\z.z)a)
                   -------  -------
               --------------------

             the redex (\y.y)x is under lambda.