The Foundations
The right understanding (and the proper knowledge) begins with very strange
questions, which most people would never ask.
Following the purely theoretical (but absolutely fundamental) result of Alonzo
Church, that his Lambda Calculus is a universal language – absolutely minimal
but yet good enough to compute any commutable mathematical function, the
question is – Why? Why just these three forms are enough for everything. This
is not an easy question to approach.
Lambda Calculus
In its canonical form the whole calculi consist of a set of terms, and a set of
reduction rules.
It has just 3 syntactic forms:
- a variable binding (a convenience for the Mind)
- a [Lambda]-abstraction (a capture)
- an application (a single step)
and just 1 reduction rule:
- [beta]-reduction (a uniform substation of a value for a bound variable)
There are a few often overlooked subtleties here:
- there is an implicit environment, which remembers the immutable bindings
- there is the substitution model, which is implicitly used in all mathematics
- there is an interpreter (which uses the substitution model), and this is you
- the process of reduction (simplification) stops when a normal form is reached
Currying is an extension for uniformly implementing a multi-argument functions.
Partial application “naturally follows”.
The Universal Machine
The crucial part of the Classic MIT Culture is recognition (and subsequent
studying) of an interpreter as a Universal Machine.
Generalized patterns of What Is.
Now why. The way to at least some answers is not toward abstract concepts, but
towards molecular and biological processes from which some fundamental
abstractions have been captured and properly generalized.
An Environment
The environment is a membrane-separated distinct partition of a single cell,
which, in turn, has an enclosing environment.
A Closure
This gives us both nesting of environments (and nesting in general) and a
“closure” (a distinct partition) which “captures” (holds) all its “stuff”
inside.
A Universal Pattern
These closures are not just physical, but also “logical” and “mathematical”
patterns. It is, thus, a Universal Pattern, indeed, the most general and the
most fundamental one – the pattern of capturing something distinct within an
environment.
At all levels
We have an environment of a shared (agreed upon) concepts, expressed in a shared
(common) human language.
A definition captures the meaning. A concept captures a generalized notion, etc.
Again, distinct “closures” (partitions) within some environment. It becomes an
environment for its “internals”.
The definitive property of a “closure” is that everything necessary (being used
inside) is captured (held) within. Ideally, it has to be eternal (indestructible).
The Lambda-abstraction
And this is, of course, what the Lambda-abstraction corresponds to – what
notion it, as a minimal abstraction, captures.
A single step
What universal notion the application of lambda terms (to one another) captures?
It captures the notion of creating a process, which performs at least one
single step.
Again, application implicitly creates a process which performs at least one
single step. This is corresponds to an enzyme within a cell.
Even more generally, to a simple chemical reaction, when a single required
condition has been meet (a process notion).
At the level of the Mind we have a single step of reasoning (deductive or
inductive), and the process in implicit withing the brain.
Cool, isn’t it? This is why the Curry-Howard isomorphism is possible – there are
the same fundamental notions being captured by “different observers”.
Abstraction by parameterization
There is another connection, this time to the Barbara Liskov’s fundamental notion of
abstraction by parameterization.
Closures which capture and do noting
