[logic-ml] $BCLOC2q$N$40FFb(B [Prof. Yde Venema, 5/25]

[Hasegawa Masahito]

$B3'MM!"(B

$B:#=5$N?eMK!J#57n#2#5F|!K$K!"5~ETBg3X?tM}2r at O8&5f=j$G0J2<$NCLOC2q$,3+:E(B
$B$5$l$^$9!#9V1i<T$O!"8=:_5R0w65<x$H$7$F?tM}8&$KBZ:_$5$l$F$$$k!"%"%`%9%F(B
$B%k%@%`Bg$N(BYde Venema$B$5$s$G$9!#$I$&$>$4MhD0$/$@$5$$!#(B

$BD9C+ at n???M(B
$B5~ETBg3X?tM}2r at O8&5f=j(B
--


                  $BCLOC2q$N$40FFb(B

$BF|;~(B: $B!!(B5$B7n(B 25$BF|(B($B?e(B) 16:30-17:30
$B>l=j(B: $B!!?tM}8&(B110$B9f<<(B  (16:00$B$h$j(B1$B3,%m%S!<$G(Btea)
$B9V1i<T(B: Yde Venema $B;a(B
$B=jB0(B: $B!!5~Bg!&?tM}8&(B & University of Amsterdam

$BBjL\(B:
Coalgebra, its Logic, and some of its Mathematical Environments

Abstract:
Computers and other electronic equipment are becoming more and prominent,
both in our daily life, and in society as a whole. When we are confronted
with undesired or incomprehensible behavior of for instance our mobile
phone, we will naively start reasoning about the system, modelling it as
a state-based evolving system, that we can only observe as a black box.
Clearly,  when it comes to specifying and reasoning about the behavior of
critical software systems, a sophisticated mathematical theory is needed.

The theory of coalgebra, which has emerged from theoretical computer science
in the last two decades, provides a general, mathematical framework for
reasoning about such state-based evolving systems. It combines mathematical
simplicity with wide applicability, due to its categorical foundations: many
features such as input/output, nondeterminism, probability, and interaction
can be encoded in the coalgebraic type which formally is a functor over Set
(or some other base category). Coalgebra allows us to give precise
mathematical definitions of notions such as behavior or observational
equivalence of systems. Logic naturally enters the picture since we want to
specify and reason about behavior in a formal way.

In the talk, we will give a very informal introduction and motivation of
coalgebra and coalgebraic logic. We then briefly explain the dualities
between algebra and coalgebra, and discuss the principle of coinduction.
In the second part of the talk we describe some of the mathematical
environments of the theory, and sketch how ideas from coalgebraic logic
can be used to generalize results in topology (the Vietoris construction)
and automata theory (Rabin's Theorem).

$BCLOC2q$N0FFb!'(B
http://www.kurims.kyoto-u.ac.jp/ja/seminar/danwakai.html

$B?tM}2r at O8&5f=j$X$N%"%/%;%9!'(B
http://www.kurims.kyoto-u.ac.jp/ja/access-01.html

--