🚀 go-pugleaf

Since at least some people, including myself, may not be entirely on top of
the whole of the literature of functional programming, I think it might be
enlightening to talk about a very small example of a formal system, namely
propositional logic, and then try to relate this to the more complex 
functional systems. Corrections and/or filling in and/or pointers to the
literature w.r.t anything in this message will be most welcome. 

In propositional logic, we work with forms rather than functions.

The terms in propositional logic consist of  (a) variables, and (b) well
formed combinations of variables drawn from an alphabet  V,
with the propositional operations, {and, or, implies, not, true, false equiv}
say.

A domain of interpretation contains only two elements,  B = {True, False},
with associated functions  AND OR IMPLIES NOT TRUE FALSE EQUIV, defined by
truth-tables. An environment is a mapping from a finite set  V1 contained in V
to  B. The function eval(T,E) is defined by:                     

    eval(T1 and T2,E) = eval(T1) AND eval(T2)
      etc. for or, not ...
      eval(v,E) = E(v)  if v in V

[Algebraically, eval is related to the concept of a homomorphism.]
A term T is said to be a tautology if eval(T,E) = True  for all environments
E. An environment is minimal for a given term if its domain is precisely the
set of variables occurring in the term. In the propositional calculus we can
decide if a term is a tautology since the set of minimal environments for a
given term is finite (tho' exponential in the number of variables). More
interesting logics do not admit this possibility.

If  S1 equiv T1,... Sn equiv Tn  are a set of tautologies then the
term-rewriting system:

E =
	{S1 -> T1,
	.
	.
	Sn -> Tn}

has the property of preserving truth functional equivalence, or we may say
that if S can be rewritten to T using E,  S -->(E) T, then  S equiv T is a
tautology. E may or may not have other nice properties, e.g. confluence.

I understand that interpretation in the Propositional Calculus corresponds to
denotation in Scott-Strachey semantics. (Indeed, given an ordering on the set
of variables, you could associate a truth function with a term). Thus it would
appear possible to relate syntactic manipulations using term-rewriting to
denotational identity, as can be done for the Propositional Calculus.  

What is clear is that this precludes certain kinds of pattern-matching
definitions, particularly those which are order-dependent. E.g.,

	lookup(x,[]) = false
	lookup(x,(x::y)::l) = y
	lookup(x,z::l) = lookup(x,l)

This issue is discussed in Peyton-Jones (see eg. section 5.5, p98 "Uniform
Definitions").

There is, of course, an intermediate formalism, namely the lamdba calculus,
which has its own syntactic manipulations, e.g. beta-reduction, which are
complicated by rules about avoiding name-clashes. I take it that these
have been proved sound with respect to the Scott-Strachey semantics.
So one could construct a diagram:

          compile                  denote
(E1,T)   -------------->    L1 ---------------------------> F1
  |                          |         		         /
  | R(spec)                  | R_L(Derive(E1,spec))     /
 \/       compile           \/                 	       /
(E2,T)   -------------->    L2 -----------------------/
                                     denote

Here (E1,T1) is a set of rewrite rules E1, together with a term T, to be
reduced by the rules. Given a specification, spec, a new set of rules can be
derived, using E1 to rewrite itself. (with the Burstall-Darlington approach,
the rules may be used bi-directionally in this rewriting). A compiler can
transform these (E1,T) and (E2,T) to a terms L1,L2 in the lambda-calculus,
which itself denotes a (possibly constant) function in the semantic domain F1.
A function  R_L provides a way of applying reductions in the lambda-calculus.
Now comes the question - does there exist a function  Derive  which takes  E1
and spec and produces a new specification for a series of reductions in the
lambda-calculus which will convert  L1  to  L2?  If there is, the soundness of
of the rewriting  R(spec) depends on the soundness of derivations in the
lambda-calculus.

Term rewriting systems are normally first-order - no function variables
are permitted. Thus only some functional programs using patterns could
actually be treated with them. Some of the associated theory of term rewriting
systems (e.g. Knuth-Bendix) is heavily dependent on the unification algorithm,
which is first-order. I understand that Sorted Universal Algebras also provide
only a first-order system. Thus a more general approach would seem to be called
for. I know that Sheard and Stemple in this Department have used an extended
Boyer-Moore method of inference that depends heavily on higher order functions
like  _reduce_  (_reduce_ in APL terminology = Strachey's _lit_ function).
I will endeavour to obtain their response to this message - they are not
news-junkies as I am becoming.

Peyton Jones,S.L (1987) The Implementation of Functional Programming Languages
Prentice Hall.