mathematical foundations of programming languages
Author Message
mathematical foundations of programming languages

Several years ago I read either a book or a paper in which the
of programming languages.  Unfortunately I cannot remember exactly
what was said, nor can I remember either the name of the author
or of the book!

What I vaguely remember is as follows (not quoted nor even
accurately paraphrased, but just what I think I remember):

Several different varieties of mathematical logic have
been used as the foundations of programming languages.
For example, Prolog is based on first-order predicate
logic, together with the observation that the list of
conditions which must be met to satisfy a predicate can
be regarded as a recipe for computation.  Functional
languages are based on equality logic, which introduces
the idea that equals can be substituted for equals.
In functional languages, computation is modeled as a
series of substitutions.

The one phrase that really sticks in my memory is "equality
logic."  I have never heard this term before or since, and
I am not sure what flavor of formal logic the author was
referring to.

Anyway, I'd appreciate it if anyone can tell me who wrote this,
what they really said, and where I can find it.

Mike
(who really wishes he could run "grep" on the
local library...)

Thu, 09 Nov 1995 11:42:33 GMT
mathematical foundations of programming languages

Quote:
Mike Haertel writes:
> The one phrase that really sticks in my memory is "equality
> logic."  I have never heard this term before or since, and
> I am not sure what flavor of formal logic the author was
> referring to.

There are at least two "equational logics" that functional languages can be
based on

(1) The lambda calculus. This was developed by Alonzo Church (who
supervised Alan Turing at some point I seem to recall). in the late
1930's, early 1940's. In the printed typographic form, "lambda" is the
greek letter. The expressions of the language are formed from:

(a) variables.
(b) lambda abstractions  lambda x. E means "that function which maps
x to E (e.g. lambda x. (+ x 3) is the function "add 3").
(c) Applications  E1 E2 means "apply the expression E1 (considered as a
function) to the expression E2.

The rule which permits the lambda calculus to be a model for computation is
*beta-reduction*, which says that any expression of the form
(lambda x. E1) E2
can be reduced to "E1 with E2 substituted for x". The definition of
substitution is somewhat complicated by the handling of "free variables".

Additional rules are required for proving things, e.g. alpha-reduction
which says in effect that lambda x. E is the same as lambda y. E as long as
you don't confuse free variables. Also, for practical computing, you
introduce delta-rules, which introduce constants like 0,1,2,3, etc. (you
can in fact model these in the restricted "pure" calculus, but it is a pain
for practical purposes).

LISP is based loosely on the lambda calculus (it does not give the proper
meaning to the expression (+ 3) for instance, which means "add 3", i.e. it
should have the same meaning as the lambda expression given above.
More modern functional languages (ML, Haskell) are based much more exactly
on the lambda calculus, despite their different appearance, which arises
from the application of "syntactic sugar" to taste (not everbody has the
same taste in sweeteners...)

(2) Combinatorial logic. This was developed in the 1920's by Schonfinkel.
It is ingeniously simple, requiring only two "combinators" S and K,
together with application, with the reduction, for all f g x y:

S f g x -> f x (g x)
K x y   ->  x

No variables are required in the language (f, g, x, y in the above are META
variables which serve to define the reduction). Thus expressions need only
contain S and K, and still form a complete basis for computation and proof.
In particular, there are no hassles with free variables.

Alas this elegant simplicity is bought at a price - Combinatorial logic can
easily be shown to be equivalent to the lambda calculus, BUT a lambda
calculus expression of size O(n) is equivalent to a combinatorial
expression of size O(n^2). More practical combinatorial logics have
additional combinators (I,B,C,B',C'), but have not won mainstream support.

The lambda calculus is powerful and elegant. It embodies *abstraction*
(i.e. lambda abstraction) as one of 2 primary constructs, which renders it
much more suitable than Turing machines to form a basis for a theory of
computation. Imperative languages can be modelled EITHER in an extended
lamdba calculus (see Landin's paper "A Correspondence between Algol 60 the
Church's Lambda Notation"[1965], CACM 8 pp89-101 and 158-165, or (better)
by modelling the mutable store within the lambda calculus.

Robin Popplestone.

Fri, 10 Nov 1995 21:24:52 GMT
mathematical foundations of programming languages
There is at least one other definition of "equational logic": that of
FIRST-ORDER equational logic (quantifier-free terms of ordinary first-order
logic, with equality as the only predicate symbol).  The model theory of this
logic was developed into what's called universal algebra by Birkhoff et al.
See the texts by Birkhoff, Gratzer, or Cohn.  It was later made into a branch
of category theory by Lawvere ("algebraic theories").

This (along with various extensions) served as the basis for the treatment of
algebraic specification of data types in the early 70's by Guttag-Zilles,
Goguen-Thatcher-Wagner-Wright, and others too numerous to name here.  This
remains an active research community.

On the implementation side, these ideas formed the basis for the
transformational programming paradigm of Burstall-Darlington et al, and
probably for Backus's FP languages.

I've mentioned only a few of the many contributors to this approach; apologies
to all whom I've omitted.

--Mitch

--
Mitchell Wand
College of Computer Science, Northeastern University
360 Huntington Avenue #161CN, Boston, MA 02115     Phone: (617) 437 2072

Sat, 11 Nov 1995 00:23:29 GMT
mathematical foundations of programming languages

Quote:

> LISP is based loosely on the lambda calculus (it does not give the proper
> meaning to the expression (+ 3) for instance, which means "add 3", i.e. it
> should have the same meaning as the lambda expression given above.

When getting into functional languages it quickly occurred to me that LISP
bore no real relation to the lambda calculus at all - apart from nasties
like SETQ etc., it also treats program *text* as indistinguishable from
data - great for AI heads, but definitely not kosher. This was confirmed
when John McCarthy visited Trinity College last year (our 400th birthday)
and gave our department a brief talk on the history of LISP. He confirmed
that they never considered it based on lambda calculus at all, but simply
adopted the *lambda NOTATION* to denote anonymous functions.

Dept. of Computer Science, Trinity College, Dublin 2, IRELAND

Sat, 11 Nov 1995 19:10:19 GMT
mathematical foundations of programming languages
: Several years ago I read either a book or a paper in which the
: of programming languages.  Unfortunately I cannot remember exactly
: [...elided...]
: The one phrase that really sticks in my memory is "equality
: logic."  I have never heard this term before or since, and
: I am not sure what flavor of formal logic the author was
: referring to.
:
: Anyway, I'd appreciate it if anyone can tell me who wrote this,
: what they really said, and where I can find it.
:
I haven't heard that term "equality logic" either, but a good book on
the subject is *Introduction to the Theory of Programming Languages*,
Bertrand Meyer, Prentice Hall 1990. Unfortunately it has several typos,
but if you catch the typos, it probably means you're understanding the
material.

Sat, 11 Nov 1995 23:45:08 GMT
mathematical foundations of programming languages
two questions:

what is an equational language? how does it differ from a term rewriting
system?

i have read that some functional languages are implemented in a term
rewriting system. is there some relationship between functional languages
and term rewriting systems in general?

"if you're not programming functionally, then you must be programming
dysfunctionally"

Sun, 12 Nov 1995 17:18:01 GMT
mathematical foundations of programming languages

Quote:
>(2) Combinatorial logic. This was developed in the 1920's by Schonfinkel.

Historical Note:  It is combinatory logic, not combinatorial logic.
~                      ~~~
Also, although Schoenfinkel introduced it in the early 1920's, he
did nothing to develop it.  It was re-introduced independently by
H. B. Curry in the late 1920's (who quickly learned of
Schoenfinkel's work after he had the idea), who is really
responsible for most of the development, at least until the
1950's.  Curry also contributed in a number of ways to
lambda-calculus, including the use of Greek letters for the names
of reduction rules (alpha, beta, eta, etc).  (Church's original
name for alpha reduction (change of bound variables) was "Rule of
procedure I", and for beta reduction was "Rule of procedure II".
--
Jonathan P. Seldin

7141 Sherbrooke Street West, Montreal, Quebec, Canada, H4B 1R6

Tue, 14 Nov 1995 02:25:13 GMT

 Page 1 of 1 [ 7 post ]

Relevant Pages