[logic-ml] Klaus Keime 教授講演会

[Hideki Tsuiki]

京都大学人間・環境学研究科の立木です。

7 月 3 日 (LICS サテライト Workshop の前日) に、Darmstadt 工科大学の Klaus Keimel
先生による講演会を京都大学で行います。どうぞ、お気軽にお越しください。

講演会の後に、一緒にお食事に行こうと考えています。
人数を把握しておきたいので、お食事に来られる方は、あらかじめ
メールでご連絡頂けると幸いです。

多くの方のご参加をお待ちしております。

立木

------------------------------------------------------------

           講演会のお知らせ

日時：    7月3日（金） 16:30 より
場所：京都大学 総合人間学部棟 1401 教室  
 (吉田南キャンパスに入って左側の建物の４Fです）
講演者： Klaus Keimel     (Darmstadt 工科大学名誉教授)
題目：     On the equivalence of state transformer semantics  
             and predicate transformer semantics

The meaning of a program may be modeled by the input-output behavior,
we call it 'state transformer semantics'. Alternatively, for verifying
programs one will be interested in properties A of the output and one
wants to find conditions on the input that guarantee property A for
the output. One will work with the transformation that assigns to
property A of the output the weakest precondition p(A) on the input
that guarantees property A for the output; let us call it 'predicate
transformer semantics'.

In the presence of computational effects like nondeterministic or
probabilistic choice, a computation will not be modeled by a function
that transforms inputs from a input domain X to an output domain Y but
by a state transformer t:X --> T(Y), where T is an appropriate
computational monad. The corresponding predicate transformer p
associates predicates on Y to predicates on X. Not all predicate
transformers will correspond to state transformers, and one looks for
necessary and, if possible, sufficient conditions for predicate
transformers to correspond to state transformers t:X --> T(Y). Such
conditions are sometimes called 'healthiness' conditions.

Most examples in the literature dealing with the equivalence of the
two semantics can be seen to be based on a domain R of 'observations'
and a monad T 'subordinate' to the continuation monad [[(-) --> R] -->
R]. For the continuation monad predicates on objects X take values in
R. For the continuation monad the state transformers t and the
predicate transformers p corresponding to another are related by
'swapping arguments': t(x)(A)= p(A)(x) for x in X and predicates A on
Y.  It is the aim of this paper to describe a framework of an
algebraic/order theoretical nature for the monad T so that the
equivalence between state and predicate transformer semantics
described above for the continuation monad can be carried over.  This
framework always yields necessary healthiness conditions. The
sufficiency criterion has to be verified in each special situation
separately.

We illustrate our methods by several examples. As semantic domains we
use dcpos (directed complete partially ordered sets). But the same
methods can be applied to other Cartesian closed categories and
beyond, as we indicate in the concluding remarks.