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.
Laws of algrebra of programs
Proof of laws I.11
Equivalence of two matrix multiply programs
"Solving" for least function
Expansion theorems, recursion
Correctness proof of recursive factorial function
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 )
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.
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 )
fac2 ( n, m )
Modern functional languages are numerous. I will name some : Miranda,
Haskell, ML. Most of them can be obtained freely from the universities.
loop: if n = 0 return m
else replace n with
n-1, m with n * m and goto loop