皆様
ルートヴィヒ・マクシミリアン大学ミュンヘンのJosef Berger先生、および スワンジー大学のAnton Setzer先生・Bashar Igriedさんの講演のお知らせです。 どうぞふるってご参加ください。
問合せ先： 石原 哉 北陸先端科学技術大学院大学 情報科学系 e-mail: [email protected] -----------------------------------------------
* JAIST Logic Seminar Series *
* The lectures below are held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project CORCON. (http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/)
Date: Tuesday 6 September, 2016, 13:30-17:00
Place: JAIST, Lecture room I2 (Access: http://www.jaist.ac.jp/english/location/access.html)
*LECTURE 1*
Speaker: Josef Berger (Ludwig-Maximilians-Universität München)
Title: The fan theorem and convexity (joint work with Gregor Svindland)
Abstract: The fan theorem is the following statement:
(FAN) Let B be a decidable set of finite binary sequences. Assume that every infinite binary sequence has an initial part that belongs to B. Then there exist an N such that every infinite binary sequence has an initial part of length smaller than N that belongs to B.
This axiom plays an important role in Intuitionism, a philosophy of mathematics that was introduced by the Dutch mathematician L.E.J. Brouwer. We work in constructive mathematics in the tradition of Errett Bishop. Here, the fan theorem is neither provable nor falsifiable. Many theorems of analysis are equivalent to the fan theorem. One example for such a theorem is:
(POS) Every positive-valued uniformly continuous function on the unit interval has positive infimum.
In our paper 'Convexity and constructive infamy’ we have shown that, under the additional condition of convexity of the function, POS is constructively valid.
In this talk, we discuss to which extent this gives rise to a notion of 'convex bars' and a corresponding constructively valid 'convex fan theorem'.
*LECTURE 2*
Speaker: Anton Setzer and Bashar Igried (Swansea University)
Title: Coinductive Reasoning in Dependent Type Theory - Copatterns, Objects, Processes (part on Processes joint work with Bashar Igried)
Abstract: When working in logic in computer science, one is very often confronted with bisimulation. The reason for its importance is that in computer science, one often reasons about interactive or concurrent programs. Such programs can have infinite execution paths, and therefore correspond to coinductive data types. The natural equality on coinductive data types is bisimulation. Proofs of bisimulation form one of the main principles for reasoning about coinductive data types.
However, bisimulation is often very difficult to understand and to teach. This is in contrast to the principle of induction, where there exists a well established tradition of carrying out proofs by induction. One goal of this talk is to demonstrate that one can reason about coinductive data types in a similar way as one can reason inductively about inductive data types.
Reasoning about inductive data types can be done by pattern matching. For instance for reasoning about natural numbers one makes a case distinction on whether the argument is 0 or a successor. For coinductive data types the dual is copattern matching, which is essentially a case distinction on the observations one can make for a coinductively defined set. For instance, streams have observations head and tail, and one can introduce a stream by determining its head and its tail.
We then look at examples of the use of coinductive data types. One is the notion of an object, as it occurs in object-oriented program. Objects are defined by their method calls, which are observations, so they are defined coinductively. The final example will be the representation of processes in dependent type theory, where we will refer to the process algebra CSP.