ALGEBRA AND THE LAMBDA CALCULUS

			   by Aubrey Jaffer

ABSTRACT: An algebraic system which includes Church's lambda calculus
and currying is presented.  Closures, applications, and currying are
implemented using variable elimination.

The usual connection made between the lambda calculus and algebra is
to construct the integers using the lambda calculus and then construct
algebraic (and other formulas) by Godelizing them.

The system described here reverses this connection by implementing the
lambda calculus in an algebraic system.  It is used in the JACAL
symbolic mathematics system and gives JACAL the ability to represent
functions as members of the algebraic system.  All of the system's
operations (including simplification) can then be applied to functions
as easily as to expressions.

		       ALGEBRAIC REPRESENTATION

Given an underlying representation for multivariate polynomials we
can represent an equation as a multivariate polynomial with the
understanding that the polynomial is equal to zero.  We can convert
typical equations to this form by multiplying both sides by the
denominators and then subtracting the left side from both sides.  For
instance:

	f/(c+d) = (a-b)/g;

Yields:

	0 = (a - b) c + (a - b) d - f g

How to represent expressions?  The usual approach is to use a
polynomial or a ratio of polynomials.  Instead, we will introduce a
special variable "@", calling it the value variable.  The value of a
polynomial involving @ is that polynomial "solved" for @.  For
instance, the expression:

	-1 + x
	------
	1 + x

is represented internally as:

	0 = -1 + x + (-1 - x) @

This allows us to represent irrational expressions as well:

			  5
	0 = -1 - y - @ - @ 

Is the root of a fifth degree polynomial.

For the rest of this paper the examples will not show @ if the values
can be represented in usual mathematical notation without it (as JACAL
does).

			     SUBSTITUTION

At this level of algebraic abstraction we do all operations using
variable elimination.  Variable elimination is the process of
combining n polynomial equations so that m variables do not appear in
the (n-m) resulting equations (where n > m).  Common techniques used
include resultants [1][2][4][5] and Groebner Bases [3][4][5].

	eliminate([a+c^2=b,b+c^2=2],[c]);

Yields:

	0 = 2 + a - 2 b

Common symbolic transformations can be done by constructing auxiliary
polynomial equations and eliminating variables between them and the
original polynomial equations.  The operation we are interested in for
the next section is substitution.  We can substitute an expression for
a variable by constructing an auxiliary equation of the variable and
then eliminating that variable.  Suppose we want to substitute
(a*x+b)^2 for g in g+1/g.  We construct the equation g=(a*x+b)^2
and then:

	eliminate([g=(a*x+b)^2, g+1/g],[g]);

	     4        3        2  2  2      3    3    4  4
	1 + b  + 4 a b  x + 6 a  b  x  + 4 a  b x  + a  x
	--------------------------------------------------
		        2              2  2
		       b  + 2 a b x + a  x

Eliminate deals only with polynomial equations so remember that g+1/g
internally is:

		 2
	0 = 1 + g  - g @

and similarly for the result.

			      FUNCTIONS

A similar approach to the use of @ can be used for arguments as well.
We will name these arguments @1, @2, and so on.

Functions do not need to use all of their arguments.  However, in this
system, a function must use at least one of its arguments.  With this
constraint, the only difference between a function and an expression is
the presence of @n variables.  Our functions can return either
equations or expressions; those containing @ are expressions and those
without, equations.

A function which ignores its first two arguments is
lambda([x,y,z],1/z-z), which would be represented as

	      2
	1 - @3
	-------
	  @3

These functions can freely mix bound and free variables.  The
following expression, with free c and bound x and y,

	f : lambda([x,y],c*(y+x)/(y-x));

is simply:

	c @1 + c @2
	-----------
	 - @1 + @2

We can now apply this function.  We don't have to always apply it to
two arguments, we can apply it to just one also.  This is called
"currying" an argument.  The application

	g : f(x);

substitutes x for @1 from the polynomial equation for f.  It also
"bumps" @2 down to @1 (also by substitution).  This results in a new
function of one argument:

	c x + c @1
	----------
	 - x + @1

It this function is applied to one argument (which is a non-function)
the result will be a non-function.  For example g(a+b) yields:

	(- a - b) c - c x
	-----------------
	   - a - b + x

This result is exactly the same as the result of applying f(x,a+b).

			   ALPHA-CONVERSION

The above method is sufficient when the arguments to functions are not
themselves functions.  But when applying functions to functions
differences in the order of elimination produce different results.
Consider applying @1-@2 to the arguments (@2, @1).  The result should
be @2-@1.  But if we curry an argument we get @2-@2 -> 0 applied to
@1.

This problem is similar to the inadvertent capture of free identifiers
by macros in languages like C and Lisp.  The solution to this problem
is called alpha-conversion in the lambda calculus and Hygienic Macro
Expansion in a paper of that title by E.E.Kohlbecker, D.P.Friedman,
M.Fellinson, and B.Duba [6].

Since the names of bound identifiers are unimportant we will
substitute new names for those lambda variables for which we will
later substitute arguments.  This eliminates possible conflicts between
the variables bound in the current function and variables in its
arguments (which are free relative to this function).

In the above example substitute :@1 for @1 and :@2 for @2 in @1-@2
yielding :@1-:@2.  Now substitute @2 for :@1 and @1 for :@2.  This
then yields the desired result @2-@1.

Currying an argument would substitute @2 for :@1 and @1 for :@2 in
:@1-:@2 to produce @2-@1.  When this function is applied to the
remaining argument, @1, the result is @2-@1 as before.

				LAMBDA

A symmetrical situation to currying of arguments is binding a variable
over a function.  lambda([y],lambda([x],x-y)) should yield the same
function as lambda([y,x],x-y).  The trick here is to "bump up" any
lambda variables in an expression when binding additional variables.
To execute lambda([y],@1-y) we substitute @2 for @1 and then @1 for y.

			 VECTORS AND MATRICES

Vector and matrix valued functions can be represented by vectors and
matrices some of whose entries are lambda expressions.  Clearly a
vector or matrix function applied to scalar arguments should return a
vector or matrix with the same shape as the function.

The case of a scalar function applied vector arguments can work if the
multiplication used by the function is of a type compatible with the
arguments.  Inner product is commutative while matrix multiplication
is not.  Another possibility here is to have a mechanism for allowing
lambda expressions to reference elements vector and matrix arguments.

The case of vector or matrix functions applied to vector or matrix
arguments gets stickier.  Allowing only elements of the arguments to
be operated on is one solution; Another is to incorporate the
structure of the arguments inside the structure of the function or
vice versa.

			 DIFFERENTIAL ALGEBRA

These techniques can be extended to differential algebra as well.  In
differential algebra the derivative of a variable, written v', can act
as an variable in polynomials.  Derivatives of derivatives are also
allowed and can be written v'' and so on.

When applying a function, each distinct derivative of a lambda
variable with a corresponding argument requires that an equation be
generated and that derivative variable be eliminated.  We equate the
nth derivative variable with the nth total derivative of its
corresponding argument.  For instance to apply the function @1'/@2' to
(x^3,x) we

	eliminate([@1'/@2',@1'=(x^3)',@2'=(x)'],[@1',@2']);

	   2
	3 x

As illustrated by this example, differential operators are now as
easily expressed as functions.  This worked well for the univariate
case; what about multiple variables?  (@1'/@2')((x+y)^2,x) yields

	2 x x' + 2 x' y + (2 x + 2 y) y'
	--------------------------------
	               x'

We need to set y' to 0 to get the expected answer 2 x + 2 y.  But when
we curry we need to have the differentials remain until all the lambda
variables are consumed. (@1'/@2')((x+y)^2) gives

	2 x x' + 2 x' y + (2 x + 2 y) y'
	--------------------------------
	              @1'

We don't want to set x' and y' to 0 in the numerator because the
result would be 0.  We don't know which differential until @1' is
substituted for.  I think the solution here is to set to zero
differentials occurring only in the numerator and only for those
expressions containing no lambda variables or their derivatives.

			      CONCLUSION

I have shown how to implement functional abstraction (lambda),
application and partial application (currying) in a system built on
variable elimination from polynomials.

			     BIBLIOGRAPHY

[1] Bareiss, E.H.: Sylvester's identity and multistep
    integer-preserving Gaussian elimination. Mathematics of
    Computation 22, 565-578, 1968.

[2] Uspensky, J.V.: Theory of Equations
    McGraw-Hill Book Co., Inc., 1948

[3] Thomas W. Dube: "The Structure of Polynomial Ideals and Groebner
    Bases", SIAM JOURNAL ON COMPUTING, (19,4) (August 1990) pp. 750-773.

[4] Hoffmann, C. M.: Geometric and Solid Modeling: An Introduction.
    Morgan Kaufmann Publishers, Inc. San Mateo, California, 1989

[5] Geddes, K.O., Czapor, S.R., Labahn, G.: Algorithms for Computer
    Algebra. Kluwer Academic Publishers

[6] Hygienic Macro Expansion
    E.E.Kohlbecker, D.P.Friedman, M.Fellinson, and B.Duba
    1986 ACM Conference on Lisp and Functional Programming
    Pages 151-159