Formalizing variable binding

John Harrison (John.Harrison@cl.cam.ac.uk)
Wed, 15 Jun 94 22:36:29 +0100

John Staples writes:

[Good summary of QED workshop deleted]

I do believe that as QED gains experience with supporting mathematics,
the benefit of formalising more of ordinary mathematical discourse
will become clear. For example, mathematical logic has so far
largely ignored the formalisations of:

* the bindings involved in definite and indefinite integral
notations;

* the introduction of such bindings as defined notation;

* proofs of correctness of such definition mechanisms.

I agree with your general points, but I'd say that mathematical logic
has completely solved the problem of formalizing variable binding
operations, in the shape of lambda calculus. (If you don't like higher
order formalisms you may have cause to dispute this.)

For example in HOL, lambda abstraction is the only variable binding
operation. One of the four term constructors is lambda abstraction, written
in ASCII as "\x. t[x]", and meaning `that function of "x" returning "t[x]"'.

Quantifiers are merely higher-order constants. For example the universal
quantifier has (polymorphic) type ":(* -> bool) -> bool". The visible term
"!x. P[x]" (for all "x", "P[x]") is a syntactic sugaring of the application
of the universal quantifier constant to a lambda abstraction: "! (\x. P[x])".

Other binders, including the derivative of a function, are defined in the
same way. With a more elaborate parser for the introduction of additional
parameters like upper and lower limits, this extends easily to notions like
integration and summation.

The approach sits comfortably with the view of differentiation and
integration as higher order function(al)s. It localizes the complexity of
variable bindings in a single term constructor, and requires no complex
definitional support. (I am not sure where this approach to variable
binding operations originates, but I suspect it is from Church.)

I would say that the most important feature neglected in many presentations
of logic is some sort of description operator: "the x such that ..." or
"some x such that ...". I believe Bourbaki postulate such a feature in their
notional logical foundation. Without it, there seems to be a real reliance
on nontrivial metatheory (introducing Skolem functions or getting rid of
existential quantifiers in an elaborate way). If you don't like the Axiom of
Choice you need to be careful about allowing free variables in the "..."s
in the introduction rule.

John.