Functional Programming

Functional programming was a new paradigm of programming aims to offer a programming system that has ability to "reason" of programs.  That is, verify if a program performs according to what the programmer intended (proof programs correct), check that two seemingly different programs are indeed give the same output when presented with the same input (proof equivalence of programs), check invariant properties of programs, etc.  Proving the properties of programs become more and more important today as programs become very large and complex.  John Backus proposed his idea in 1977 in the lecture of ACM turing award (Backus, J. "Can programming be liberated from the von Neumann style? A functional style and its algebra of programs", Communication of the ACM, August 1978, 20(8):613-641).  In this lecture I will illustrate Backus' system called "FP".  I hope that the audience will gain some new idea on alternative style of programming which is very different from procedural style.  I will show some "proof" on programs using nothing more than ordinary school algebra.
FP systems
        Functions  page1   page2
        Functional forms
Laws of algrebra of programs
Proof of laws I.11
Equivalence of two matrix multiply programs
"Solving" for least function
        Expansion theorems, recursion theorem
Correctness proof of recursive factorial function

About Efficiency

Today function programming systems are very powerful and complete.  Most of them can "compile" funcitonal programs into machine codes for conventional processors with results of very efficient programs comparable to programs in procedural style.  Most modern functional languages have strong type with sophisicate type inferences.  Because equivalence of two programs can be verified, it is possible to "transform" one program into another.  Hence an easy to understand program can be transformed into an efficient program.  For example the two factorial programs :
fac1 ( n )
if n = 0 return 1
else return n * fac1(n-1)

fac2 (n, m )   //  m = n !
if n = 0 return m
else return fac2( n-1, n * m )

Which are the two programs illustrated in the correctness proof above.  The two programs are both correct, they both compute factorial of input. fac2 is called by fac2( n, 1 ). The second program, fac2, is more efficient because the recursive call is the last call and can be optimised (call "tail-recursion optimization") which change recursive call into iterative loop.  The style of fac2 is called accumulating parameter.
fac2 ( n, m )
loop:  if n = 0 return m
       else  replace n with n-1, m with n * m and goto loop
Modern functional languages are numerous.  I will name some : Miranda, Haskell, ML.  Most of them can be obtained freely from the universities.