次のご案内をさせていただけると幸いです。
慶應大 岡田光弘 峯島宏次
ーーーーーーーーーーーーーーーーーーー
論理―計A算―哲学セミナーLogic-Computation-Philosophy Seminar
「プログラム」「アルゴリズム」「計算モデル」を「定義する」ことに関する
Prof. Thomas Seillerの講義をご案内させていただきます。
ハイブリッド形式
講義Title« 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 »
We will put updated information in any, here.最新情報URL
https://abelard.flet.keio.ac.jp/2024/seminar_talk_202405 https://abelard.flet.keio.ac.jp/satellite-workshop_202406/poster_ja.pdf
5月２８日火曜日 １7:30-19:00 May 28 Thuesday
慶應義塾大学三田キャンパス東館（東門の建物）4階オープンラボ
三田キャンパス：アクセス：[慶應義塾] (keio.ac.jp) https://www.keio.ac.jp/ja/maps/mita.html
キャンパスマップ13番
At the Open-Lab, 4th floor of the East (Research) Building at the East Gate of Mita-Campus of Keio University
Mita Campus: Keio University https://www.keio.ac.jp/en/maps/mita.html
Building # 13 on the Campus Map
要事前登録・Preregistration required
登録用のリンク Hybrid Meeting https://forms.gle/cbPr2vQrJA4haVFW7
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 岡田光弘 峯島宏次