京都大学人間・環境学研究科の立木です。
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.