Colloquium in Honour of Erwin Engeler's 80th Birthday and SSLPS Annual Meeting 2010
Program
Thursday, March 4, 2010
- 14.00 – 14.15 Opening
- 14.15 – 15.15 Henk Barendregt: Reminiscences and Predictions
Reminiscences and Predictions
Henk Barendregt, Radboud University, Nijmegen
Abstract tba
- 15.15 – 15.45 Coffee
- 15.45 – 16.45 Giuseppe Rosolini: A Category-Theoretic Point of View of Engeler's Models of the Untyped Lambda-Calculus
A Category-Theoretic Point of View of Engeler's Models of the Untyped Lambda-Calculus
Giuseppe Rosolini, Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova, Genova
Following an approach of Dana Scott, it has become common to view a model of the untyped lambda-calculus as a reflexive object in a abstract cartesian closed category, i.e. an object M together with a retraction of its endofuction object [M->M] into M. Thus any Engeler's model can be viewed in such way. But this dodges the question of the existence of a natural cartesian closed category where to view such a lambda-algebra as a object with its endofunction space as a retract. We present such a possibility and discuss the intution that such a natural model may provide. This is joint work with Martin Hyland, Misao Nagayama, and John Power.
- 16.45 – 17.15 Coffee
- 17.15 – 18.15 Giuseppe Longo: Randomness and Organisation, as Anti-entropy, in Darwin's Evolution
Randomness and Organisation, as Anti-entropy, in Darwin's Evolution
Giuseppe Longo, CNRS & Département. d'Informatique, Ecole Normale Supérieure, Paris
By a remarkable analysis spanning many articles and two books, J.S. Gould stresses the role of randomness in Evolution. In particular, we, the humans, are the random complexification of a bacterial world, along a contingent and possible diffusive path. In order to set these remarks and the associated paleontological evidence on mathematical grounds, the notion of anti-entropy, as formalized biological complexity, is presented (a quantification of cellular, functional and phenotypical differentiation). Then Gould's phylogenetic curb is derived as a diffusion equation of biomass over anti-entropy. The analogies and differences will be mentioned with Shannon's and Brillouin's negentropy and to (algorithmic) information and randomness.
F. Bailly, G. Longo. Biological Organization and Anti-Entropy. In J. Biological Systems, Vol. 17, No. 1, pp. 63-96, 2009. (downloadable)
- 18.15 – 19.00 Apero
Friday, March 5, 2010
- 09.30 – 10.30 Johann A. Makowsky: Application of Logic to Combinatorial Functions
Application of Logic to Combinatorial Functions
Johann A. Makowsky, Faculty of Computer Science, Technion - Israel Institute of Technology, Haifa
We discuss variations of theorems due to I. Gessel and the C. Blatter and E. Specker concerning modular linear recurrence relations with constant coefficients for the densities of graph properties. We then discuss combinatorial interpretations of sequences of natural numbers satisfying various linear recurrence relations with constant or polynomial coefficents over the integers, and give characterizations of these. These characterizations are reminiscent of the Chomsky-Schuetzenberger Theorem counting the number of words of length n of regular languages. (Joint nwork with E. Fischer and T. Kotek)
- 10.30 – 11.00 Coffee
- 11.00 – 12.00 Bruno Buchberger: Algorithmic Algorithm Synthesis by the Lazy Thinking Approach
Algorithmic Algorithm Synthesis by the Lazy Thinking Approach
Bruno Buchberger, Research Institute for Symbolic Computation, Johannes Kepler University, Linz
In the Theorema Project, we attempt to computer-support (semi-automate) the exploration of mathematical theories (invention of concepts by definition, invention and proof of propositions, invention of problems, invention and verification of algorithms for solving problems). The speaker's "Lazy Thinking" approach is a general heuristics for inventing (and proving) theorems and inventing (and proving) algorithms. It combines the use of formulae schemes (for proposing potential theorems and algorithms), the automated analysis of failures in (automated) proof attempts (for proving the appropriateness of the schemes), and the automated generation of lemmata and subalgorithms from the failing proofs.
In the talk, we explain Lazy Thinking by first giving a simple example. We will then show that an algorithm for a problem as difficult as Groebner bases construction (a fundamental problem in computer algebra) can be synthesized, completely automatically, by this method.
The talk illustrates the power of formal methods in software science as advocated by the work of Professor Engeler.