Algebra and the Lambda Calculus
The Jacal's tale
Aubrey Jaffer
Aubrey is a programmer and electronic engineer who also serves as board member of the League for Programming Freedom. He can be reached at 84 Pleasant Street, Wakefield, MA 01880.
Some years ago, in order to facilitate the design of constant impedance electrical filters (diplexers), I wrote a symbolic circuit-analysis program. The initial version of the program was written in Lisp over a two-week period. It implemented canonical, rational expressions and was not particularly sophisticated (it used, for example, Euclidean GCD); it worked directly with the small-signal Laplace Transform of currents, voltages, and impedances. After reading further about symbolic manipulation, I became fascinated with the problem of canonical forms. This interest led to Jacal.
Jacal is a symbolic mathematics system for the simplification and manipulation of equations and single- and multiple-valued algebraic expressions constructed of numbers, variables, radicals, and algebraic, differential, and holonomic functions. In addition, Jacal can work with vectors and matrices of the aforementioned mathematical objects.
I wrote Jacal using SCM, my implementation of the Scheme language. Jacal and SCM are both copylefted programs (distributed under the Gnu software license) and are available from various Internet ftp sites. (You can use the Internet "archie" utility to find out which sites; you can also purchase the package from me.) My implementation of Scheme runs on Amiga, Atari-ST, MacOS, MS-DOS, OS/2, NOS/VE, VMS, UNIX, and similar systems, and complies with the IEEE P1178 and R4RS specifications.
This article stems from my work with Jacal. It does not focus on details of Jacal's implementation, but rather, describes an approach--to my knowledge, unique--to implementing the lambda calculus in an algebraic system such as Jacal. This article deals with an issue many programmers face, that of naming conflicts, and shows how a symbolic-mathematics program addresses this problem. In the study of mathematical logic, 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 encoding them by numbers (known as "Godelizing" them, or assigning Godel numbers). Although the notion of Godelized formulas may have been nonintuitive when it was invented 60 years ago, the concept of encoding formulas by integers is stock-in-trade for programmers today.
My approach reverses this connection by implementing the lambda calculus on top of an algebraic system. This approach gives Jacal the ability to represent functions as members of an algebraic system. The resulting benefit is that all of the system's operations (including simplification) can then be applied to functions as easily as to expressions. The system can handle both function application, as well as currying (partial application), and closures, all using variable elimination from polynomials. Listing One, page 92, presents the Scheme code that implements variable elimination. Before discussing how this is done, let's briefly review some basic concepts.
Lambda Calculus and Currying
The lambda calculus, created by logician Alonzo Church in the 1930s, is familiar to most programmers in the form of macros--for C programmers, this means preprocessor #define directives. A lambda expression is similar to a macro definition or a #define directive--all contain a list of symbols which are bound to the arguments when the macro or lambda expression is applied. Those symbols not bound by the macro are called free.
Currying (attributed to logician Haskell B. Curry), which may not be as familiar, is the process of partially applying a function. For instance, if the C macro preprocessor supported currying, then the directives
#define F(x,y,z) x+y*z #define G F(a)
would be equivalent to
#define F(x,y,z) x+y*z #define G(y,z) a+y*z
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 0. 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, consider the following equation: f/(c+d)=(a-b)/g. We can trivially convert this equation to the following equivalent: 0=(a-b)c+(a-b)d-fg.
But how to represent expressions? The usual approach is to use a polynomial or a ratio of polynomials. Instead, we'll 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) can be represented internally as: 0=-1+x+(-1-x)@.
This technique allows us to represent irrational expressions as well. For example, the following expression is the root of a fifth-degree polynomial: 0= -1-y-@-@5.
For the rest of this article, I won't show @ in the examples if the values can be represented in usual mathematical notation without it (as Jacal does).
Substitution
At this level of algebraic abstraction we can accomplish all operations by 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 (see Bareiss, Upsensky, Hoffman, and Geddes et al.) and Groebner Bases (refer to Dube, Hoffman, and Geddes et al.).
For example, given the following Jacal statement: eliminate([a+c2=b,b+c2=2],[c]). After variable elimination, the statement yields: 0=2+a-2b.
Common symbolic transformations can be accomplished 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 the statement: eliminate([g=(a*x+b)2, g+1/g],
[g]). After substition, the statement yields the results in Example 1.
Eliminate deals only with polynomial equations, so remember that g+1/g internally is: 0=1+g2-g@. This is also true for the result.
Functions
Similarly, @ can be used for arguments as well. We'll 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.
An example of a function which ignores its first two arguments is: lambda([x,y,z],1/z-z). This function can be represented using @ notation as: (1-@32)/@3.
Using this scheme, functions can freely mix bound and free variables. Consider the following expression, with free c and bound x and y: f : lambda([x,y],c*(y+x)/(y-x)). This expression can be represented simply as: (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 also apply it to just one. (This is 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: (cx+ @1)/(-x+@1)
If this function is applied to one argument (which is a nonfunction), the result will be a nonfunction. For example g(a+b) yields: ((-a-b)c-cx)/(-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. For example, given the directives:
#define F(z) 1+G(z) #define G(y) y*z
then F(x) expands to (1+z*z) rather than (1+x*z).
The solution to this problem is called "alpha-conversion" in the lambda calculus. It is also termed "Hygenic Macro Expansion" in a paper of that title by Kohlbecker, Friedman et al.
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, of which some 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 to 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 of vector and matrix arguments.
The case of vector or matrix functions applied to vector or matrix arguments is 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 as v', can act as an variable in polynomials. Derivatives of derivatives are also allowed and can be written as 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 (x3,x) we use the following statement: eliminate([@1'/@2',@1'=(x3)',@2'=(x)'],[@1',@2']). This statement yields: 3 x2.
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? Given the function (@1'/@2')((x+y)2,x), the desired result is shown in Example 2(a).
We need to set y' to 0 to get the expected answer. But in currying, we need to have the differentials remain until all the lambda variables are consumed. (@1'/@2')((x+y)2,@1) gives the result in Example 2(b).
The solution here, I suspect, is to remove from an expression not containing lambda variable (@) differentials, the expression differentials which appear in its denominator. However, at this writing, I do not have experience with this solution.
References
Bareiss, E.H. "Sylvester's Identity and Multistep Integer-Preserving Gaussian Elimination." Mathematics of Computation 22, 1968.
Uspensky, J.V. Theory of Equations. New York, N.Y.: McGraw-Hill, 1948.
Thomas W. Dube. "The Structure of Polynomial Ideals and Groebner Bases." SIAM Journal of Computing, August, 1990.
Hoffmann, C. M. Geometric and Solid Modeling: An Introduction. San Mateo, CA.: Morgan Kaufmann Publishers, 1989.
Geddes, K.O., S.R. Czapor, G. Labahn. Algorithms for Computer Algebra. Boston, MA.: Kluwer Academic Publishers, 1992.
Kohlbecker, E.E., D.P. Friedman, M. Fellinson, and B. Duba. "Hygenic Macro Expansion." ACM Conference on Lisp and Functional Programming, 1986.
Example 1: Output from Jacal showing a result of variable elimination and substitution
Example 2: (a) The desired result of a sample differential function application; (b) the actual result.
_ALGEBRA AND THE LAMBDA CALCULUS_ by Aubrey Jaffer [[LISTING ONE] ;;; Excerpt from Jacal: Symbolic Mathematics System, written in Scheme. ;;; Copyright 1989-1993 Aubrey Jaffer. See the file "COPYING" in ;;; the Jacal distribution for terms applying to this program. ;;;; Variable elimination (define (poly:elim poleqns vars) (cond (math:trace (display-diag "eliminating:") (newline-diag) (write-sexp (math->sexp (map var->expl vars)) *output-grammar*) (display-diag " from:") (newline-diag) (write-sexp (math->sexp (poleqns->licits poleqns)) *output-grammar*))) (do ((vs vars (cdr vs)) (polys poleqns) (poly #f)) ((null? vs) (cond (math:trace (display-diag "yielding:") (newline-diag) (write-sexp (math->sexp polys) *output-grammar*))) polys) (do ((var (car vs)) (pl polys (if (null? pl) (math-error "not enough equations" poleqns vars) (cdr pl))) (npl '() (cons (car pl) npl))) ((poly:find-var? (car pl) var) (set! poly (promote var (car pl))) (do ((pls (cdr pl) (cdr pls))) ((null? pls) (set! polys npl)) (if (bunch? (car pls)) (math-error "elim bunch?" (car pls))) (set! npl (cons (poly:resultant poly (car pls) var) npl)))) (if (bunch? (car pl)) (math-error "elim bunch?" (car pl)))))) (define (infinite-list-of . elts) (let ((lst (copy-list elts))) (nconc lst lst))) ;;; This tries to solve the equations no matter what is involved. ;;; It will eliminate variables in vectors of equations. (define (eliminate eqns vars) (bunch:norm (if (some bunch? eqns) (apply map (lambda arglist (eliminate arglist vars)) (map (lambda (x) (if (bunch? x) x (infinite-list-of x))) eqns)) (poly:elim eqns vars)))) (define (elim:test) (define a (sexp->var 'A)) (define x (sexp->var 'X)) (define y (sexp->var 'Y)) (test (list (list a 0 0 124 81 11 3 45)) poly:elim (list (list y (list x (list a 0 0 2) (list a 0 1)) 1) (list y (list x (list a 5 1) 0 -1) 0 1) (list y (list x (list a -1 3) 5) -1)) (list x y))) (define (bunch:map proc b) (cond ((bunch? b) (map (lambda (x) (bunch:map proc x)) b)) (else (proc b)))) (define (licits:for-each proc b) (cond ((bunch? b) (for-each (lambda (x) (licits:for-each proc x)) b)) ((eqn? b) (proc (eqn->poly b))) (else (proc b)))) (define (licits:map proc b) (cond ((bunch? b) (map (lambda (x) (licits:map proc x)) b)) ((eqn? b) (poleqn->licit (proc (eqn->poly b)))) (else (proc b)))) (define (implicits:map proc b) (cond ((bunch? b) (map (lambda (x) (implicits:map proc x)) b)) ((eqn? b) (poleqn->licit (proc (eqn->poly b)))) ((expl? b) (proc (expl->impl b))) (else (proc b)))) ;;; replaces each var in poly with (proc var). ;;; Used for substitutions in clambda and capply. (define (poly:do-vars proc poly) (if (number? poly) poly (univ:demote (cons (proc (car poly)) (map (lambda (b) (poly:do-vars proc b)) (cdr poly)))))) (define (licits:do-vars proc licit) (licits:map (lambda (poly) (poly:do-vars proc poly)) licit)) ;;;; Canonical Lambda ;;;; This needs to handle algebraic extensions as well. (define (clambda symlist body) (let ((num-new-vars (length (remove-if lambdavar? symlist)))) (licits:do-vars (lambda (var) (let ((pos (position (var:nodiffs var) symlist))) (cond (pos (lambda-var (+ 1 pos) (var:diff-depth var))) ((lambdavar? var) (bump-lambda-var var num-new-vars)) ((lambdavarext? var) (bump-lambda-ext)) (else var)))) body))) (define (clambda? cexp) (cond ((number? cexp) #f) ((matrix? cexp) (some (lambda (row) (some clambda? row)) cexp)) ((expr? cexp) (poly:find-var-if? cexp lambdavardep?)) ((eqn? cexp) (poly:find-var-if? (eqn->poly cexp) lambdavardep?)) (else #f))) ;;;In order to keep the lambda application hygenic (in case a function ;;;of a function is called), we need to substitute occurences of ;;;lambda variables in the body with shadowed versions of the ;;;variables before we eliminate them. See: ;;; Technical Report No. 194 ;;; Hygenic Macro Expansion ;;; E.E.Kohlbecker, D.P.Friedman, M.Fellinson, and B.Duba ;;; Indiana University ;;; May, 1986 ;;;currently capply puts the structure of the clambda inside the ;;;structure of the arguments. (define (capply body larglist) (let* ((arglist (licits->poleqns larglist)) (arglist-length (length arglist)) (svlist '()) (dargs '()) (sbody (licits:do-vars (lambda (var) (cond ((lambdavar? var) (let ((lshf (- (min-lambda-position var) arglist-length))) (cond ((< 0 lshf) (bump-lambda-var var (- arglist-length))) (else (set! var (var:shadow var)) (set! svlist (adjoin var svlist)) var)))) ((not (lambdavarext? var)) var) ;; must be some sort of extension ((radicalvar? var) var))) body))) (set! dargs (diffargs svlist arglist)) (implicits:map (lambda (p) (eliminate (cons p dargs) svlist)) sbody))) (define (bump-lambda-var var delta) (lambda-var (+ (lambda-position var) delta) (var:diff-depth var))) (define (diffargs vlist args) (map (lambda (var) (bunch:map (lambda (e) (univ:demote (cons var (cdr (licit->poleqn e))))) (diffarg var args))) vlist)) (define (diffarg var args) (cond ((var:differential? var) (total-differential (diffarg (var:undiff var) args))) (else (list-ref args (- (lambda-position var) 1)))))
Copyright © 1993, Dr. Dobb's Journal
