[logic-ml] JAIST Logic Seminar Series

[Hajime Ishihara]

皆様

ルートヴィヒ・マクシミリアン大学ミュンヘンのJosef Berger先生、および
スワンジー大学のAnton Setzer先生・Bashar Igriedさんの講演のお知らせです。
どうぞふるってご参加ください。

問合せ先：
石原　哉
北陸先端科学技術大学院大学 情報科学系
e-mail: ishihara at jaist.ac.jp
-----------------------------------------------

* 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.