[FOM] Computer Scientists visa vie Mathematicians

[Dennis E. Hamilton]

-----Original Message-----
From: fom-bounces at cs.nyu.edu <fom-bounces at cs.nyu.edu> On Behalf Of Patrik 
Eklund
Sent: Saturday, January 18, 2020 01:37
To: Foundations of Mathematics <fom at cs.nyu.edu>
Cc: hmflogic at gmail.com; p.b.levy at cs.bham.ac.uk
Subject: Re: [FOM] Foundational Challenge

 [ ... ]
 > Computer scientists accept that the "elegant definition" of a lambda term 
should not be modified, even if, when eventually dealing with substitution, it 
leads to having "undesirable terms" which need to be handle by "renaming". 
Computer scientists simply find ways to code one thing in terms of another. 
"Free and bound variables" is an awful concept, since some symbols, in fact 
the informal ones, possess a capacity to "bind", a notion which seemingly is 
not describable in any language but the natural one.
 [ ... ]


I find this attribution to computer scientists to be awkward.  It strikes me 
as a misunderstanding of the matter, the origin of which is not in computer 
science at all.

The idea of scopes and whether occurrences of variables in a text are free or 
bound is a syntactic/grammatical matter.  It is easy to illustrate.  I 
hesitate to offer this to a mathematical audience where I expect it is already 
recognizable.  I do so to establish a shared context.

The TL;DR: All of this predates computer science.  It goes back to the work of 
Church and others.  My first exposure, around 1961, was in the account of 
[Rosenbloom, Paul C.  The Elements of Mathematical Logic.  Dover (New York: 
1950).  ISBN 0-486-60227-3 pbk.]  The free-bound distinction is found in 
[Church, Alonzo.  The Calculi of Lambda-Conversion.  Annals of Mathematical 
Studies 6.  Princeton University Press (Princeton NJ: 1941).  ISBN 
0-691-08394-0 pbk.]

AN ACCOUNT OF FREE, BOUND, AND BINDING

In the (applicative) expression  f(z, g(z)) the symbols f, g, and z occur 
"free."  We say they are not bound to anything there.  They may be bound to 
something in a wider context but we don't know what.  This idea of free and 
bound is about the formula texts.

In the expression ?z.( f(z, g(z)) ) we say that f and g occur "free" and z is 
bound, signifying any operand (?z.( f(z, g(z)) ) is applied to.  We might 
(informally) say z is bound to the ?z there.  It is a harmless informality 
that does leak some understanding of how that might be managed in the 
operation of a computer program.

Similarly, ?g?z.( f(z, g(z)) ) has only f occurring free, and ?f?g?z.( f(z, 
g(z)) ) has no free occurrences of (variable) symbols.

This is not particularly computer science, although computer scientists are 
sometimes interested in this kind of situation in symbolic notations employed 
in the expression of computational procedures.

The business about renaming arises if one engages in rewriting expressions by 
making symbolic substitutions that involve free occurrences of symbols that 
collide with the symbols that are bound in the place of substitution.  For a 
(contrived) example, if I wanted to inject ?n.f(n) with f occurring free in 
place of g in my example, to have f still occur free I must do some renaming, 
to something like

       ?h?z.( h(z, (?n.f(n)) (z)) ), and from there to ?h?z.( h(z, f(z)) ),

In computer science, these notions of free and bound (variables) are employed 
more widely than expressions like this.  Ultimately, in a computer program, 
there are no free occurrences -- everything is bound, and we mean variable in 
the sense of application to different operands (including input operations) or 
alteration by change of state (such as altering an element of storage). 
Application of different operands taken as functions (i.e., the procedures 
that represent them computationally) is included, as for ?f and ?g in my 
examples.

Generally, rewriting is not done although if I was editing expressions like 
that, I would have to pay attention to collisions of already-bound and free 
occurrences, just as in this message.  In turning notations like this into 
computer programs, rewriting is not a problem, lexical scoping (what the 
free-bound rules are about) is extended to dynamic cases without difficulty in 
various processing models.  The tendency, at the next level inward, is to use 
indirect addressing techniques to achieve/preserve binding without rewriting. 
The mechanisms for this are quite marvelous.  They are engineered in such a 
way as to preserve mathematical assurances to the extent that can be done with 
engineered artifacts (i.e., to within contingent reality).

 - Dennis