Continued from:
4. A mathematical overview
The following is quite technical, although it contains no equations (they are linked to in papers, for the curious). If you are not from a mathematics, computer science or physics background, I suggest proceeding to the next section, where the key points are summarised.
In the last few years have been speculations around the importance of concepts like:
- Differentiable programming
- Mathematical symmetries between neurons and genomes
Let’s try and embody these constructs within a mathematical formalism, similar to the Lambda Calculus.
1) Implies a link between lambda calculus and differentiation. 2) Requires constructing vector spaces, and consequently Tensors, from lambda calculus terms
The Lambda Calculus in its classical formalism contains no such constructs.
However, the Lambda Calculus through its history has regularly been extended, and not just with different type systems. In a breakthrough paper, Erhard and Regnier showed that we can extend the Lambda Calculus with differential constructs, and also that this new Calculus obeys a form of Taylor power series. Lambda calculus terms can be summed, with coefficient terms forming a ring. Erhard’s calculus showed constructs such as non-determinism that hinted at deep links with process calculi and parallel computation.
Many extensions have been built on this, including the construction of basic vector spaces and other algebraic structures. Some derive Lambda calculi find uses as programming models for quantum computation.
The analytical properties of the Lambda Calculus have not been fully explored. As yet, integration has not been defined, and we’ve only scratched the surface of possible topological constructs.
My research
Summary: I am designing a Differentiable & Integrable Lambda Calculus over which we can define certain Topological Spaces (A Hausdorff space), through which we can define Lie Algebras and Lie Groups.
It is possible, I believe to construct Lie algebras from the Lambda Calculus vector spaces, built using the linear models derived from Erhard and Regnier’s seminal work.
This is what my work is focused on. The following are conjectures, assuming such constructions are possible.
-
Applying the machinery of Lie Algebras and Lie Groups to Lambda calculus functions may provide further insights into information theory, by examining the symmetry properties of function transformations.
-
Constructing a metric space out of Lambda Calculus terms is also a natural domain in which to explore computational complexity. Currently, the Lambda calculus is not a useful construction for this field, as Beta-reduction within classical Lambda calculus does not have a well-developed, generally accepted computational cost model. However, the linear-logic inspired resource calculi are good candidates for developing this.
-
I believe this program will provide deep links with Geometric Complexity Theory (which employs symmetry tools from Algebraic Geometry) but also Homotopy Type Theory (this was originally formulated as a ‘Homotopy Lambda Calculus’ by its late founder, Vladimir Voedevsky).
-
I believe this extended calculus would present a powerful framework to analyse non-linear models of computation, such as Artificial Neural Networks. Neural networks rely on differentiating vector spaces. Their output though is a ‘black box’ of Tensors/Arrays. What if we could peer inside the box, and assign Lambda Calculus terms to these Tensors? We would in effect have a means of generating a functional program from the multi-dimenional arrays. These programs would be much more susceptible to human understanding, as they would more closely resemble the programming languages we attribute semantics too, like Haskell.