慶應義塾大学三田キャンパス東館（東門の建物）4階オープンラボ
At the Open-Lab, 4th floor of the East (Research) Building at the East Gate of Mita-Campus of Keio University

キャンパスマップ 4番の建物: 三田キャンパス：アクセス
Campus Map Building #4: Mita Campus: Keio University

Speaker: Thomas Seiller -（CNRS-LIPN, IHPST）

Title of the Talk:
« Defining "program", "algorithm", and "model of computation" — including a discussion on how models of linear logic emerge by generalizing geometry of interaction and transcendental syntax constructions »

Abstract:
What is a model of computation? What is a program, an algorithm? While theoretical computer science has been founded on computability theory, the latter does not answer these questions. Indeed, it is a mathematical theory of computable functions, and does not account for computation itself. A symptomatic consequence is the notion of Turing-completeness. This standard (sole?) equivalence between models of computation is purely extensional: it does only care about what is computed and not how, blind to complexity aspects and the question of algorithmic completeness. More importantly, the theory of computation is continuously growing further from how actual machines compute.

I will present a proposal for alternative foundations more faithful to computer science practice and interests. This mathematisation of computer science is grounded within the theory of dynamical systems, focussing on how computation is performed rather than only on what is computed. I will argue that it generalises computability theory while still allowing to recover standard results.

This point of view can be used to:
provide a uniform account of several lower bounds from algebraic complexity and strengthen them
define static analysis methods which can be implemented in usable tools
define families of linear realisability models (realisability models for linear logic)
lead to a semantic approach of implicit computational complexity
propose a formal definition of the notion of algorithm

In this talk, I will focus on two aspects from this list, namely points 3 and 5: First, I will explain how abstract programs give rise to models of (fragments of) linear logic, generalising Jean-Yves Girard’s geometry of interaction (or more recent transcendental syntax) constructions. I will also explain how these technical developments shed a new light on the question of defining logical constants.
Second, I will present the formal definition of algorithm that stems from the approach, discuss its properties and provide a few examples.

Logic-Computation-Philosophy Group, Dept. Philoophy Keio Univ
logic[At]abelard.flet.keio.ac.jp　岡田光弘　峯島宏次