The logic as well as the evolutionary programming paradigm can be
described in a C
-algebraic framework. Therefore, the relation between
logic programs and neural networks will be investigated based on this
uniform model. For example: On one side, there is Girard's
representation of (liner) proofs as C
-operators and his Execution
Formula corresponding to proof normalization [Girard, 1995].
On the other side, we have an operator algebraic model of neural networks,
where (in simple examples) encoding of patterns is achieved by
computing the so called Moore-Penrose Pseudo-Inverse [Kohonen, 1989].
But both procedures are just an application of the so
called Neumann series computing the inverse of an C
-operator
[Murphy, 1990].
The time schedule for the project (as sketched below) divides the work into roughly two 12 month phases, the first one will concentrate on the development of an intermediate operator algebraic model, the second one will exploit and apply this approach to develop efficient translation and comparison methods between logic and evolutionary computing.
Phase 1 (Modelling) -- following an initial start up period --
is devoted to the development of a coherent C
-algebraic bridge between
logic and evolutionary programming. First investigating C
-models for
both frameworks; from (constraint) logic programs to C
-operators --
starting point would be Girard's Geometry of Interaction -- and --
based on our own work -- from neural networks to C
-algebras.
This modelling phase is accompanied by the comparison of the different
objects: logic programs (proofs), C
-algebras, and neural networks.
How do certain characteristics translate? What notions correspond to
each other? For example: Girard's Execution Formula, Neumann Series,
and the Moore-Penrose Pseudo-Inverse are all related entities,
corresponding to proof normalization, operator inversion and pattern
encoding, respectively; or: how do the Apt-Pedereschi-Bezem level
mapping for proofing termination of prolog programs [Apt, 1995],
the Ljapunov function to characterize stability of dynamical
systems[Hirsch and Smale, 1974], and the energy function for investigating
the convergence in neural networks [Aarts and Korst, 1989] related?
Phase 2 (Translation), will concentrate on the transformation
between neural networks and logic computing (via C
-algebras) and vice
versa. First, the the theoretic foundations of such translations are
investigated, after that the practical implementation of automated
translation will follow.
The final task is to develop a prototypical system for automated translation of logic programs (or proofs) into neural networks. In linear logic that would be the passage from proof nets to neural nets. In the neural network world this can be interpreted as an initialization method; from the point of computational logic this means integrating optimization algorithms into the resolution mechanism, of which a special case, namely the translations to Boltzmann Machines (i.e. simulated annealing or combinatorial optimization) could be of special interest.