2004-05-01 [長年日記]
λ. 萩野先生の授業の補講で学校へ。
λ. 読書
- 『絶滅寸前少女』
- 流星 ひかる [著]
- 『時をかける少女 1』
- ツガノ ガク [著], 筒井 康隆 [原作]
λ. "A denotational semantics of inheritance and its correctness", William Cook and Jens Palsberg
を読んだ。継承の表示的意味論の作り方は自然なのだけど、Domainの構成が気持ち悪かった。
2004-05-02 [長年日記]
λ. Subversion
ディレクトリ構造を決めかねてCVSに突っ込んでいなかったファイル群を、Subversionで管理することにする。なにかと便利なので、これまでCVSで管理していたのも順次Subversionに移行していこう。
2004-05-11 [長年日記]
λ. "Types for Verification"
ワークショップの"Types for Verification"一日目。5時起き。7時半羽田発8時半伊丹。園田駅で反対側の出口に出てしまったりもしたけれど、なんとか始まる前に着くことが出来た。それはそうと、関西ではスイカもパスネットもバスカードも使えないのか……なんかほんと遠くにきたって感じだ。
λ. Per Martin-Löf (Stockholm University, on sabbatical at Sato-Lab, Kyoto U.) "100 years of Zermelo's axiom of choice: what was the problem with it?"
An analysis of Zermelo's axiom of choice in constructive type
theory reveals that the problem with it is not the existence of the
choice function but the extensionality of it, which is not visible
in an extensional framework where all functions are by definition
extensional.
"Intuitionistic Type Theory"にも選択公理の話は少しは出ていたはずなのだけど、すっかり忘れている私。まずいなー。(追記予定)
後で聞いた話によると、この話は3月に三田で話した内容とほぼ同じだとか(Proof Theory and its Applicationsに関する合同セミナーかな)。
【追記】 http://comjnl.oxfordjournals.org/cgi/reprint/49/3/345も参照。というか、後で読む。
λ. Masahiko Sato (佐藤 雅彦) (Kyoto University) "A simple theory of expressions"
We propose a framework called Natural Framework, which is used to
present mathematics in a formal and convenient way. We are
particularly interested in formalizing not only ordinary
mathematics but also metamathematics. In this talk, we present a
simple theory of expressions which we use as the underlying
framework for Natural Framework.
例のCALの内部で使った表現なのかな。どの辺りがうれしいのかいまいちよく分からなかった。(追記予定)
λ. Peter Dybjer (Chalmers University of Technology, visiting AIST CVS) "Martin-LöF type theory and the logic of functional programs"
Martin-Löf type theory is a foundational framework for
constructive mathematics and computer programming which is based on
the Curry-Howard interpretation of propositions as types. This
interpretation can be extended to an interpretation of Heyting
arithmetic can in Martin-Löf type theory. In the opposite direction
we have the interpretation of Martin-Löf type theory in a
first-order theory of combinators given by Aczel 1974. This
interpretation is closely related to the informal meaning
explanations underlying Martin-Löf type theory.
In this talk I will review Aczel's interpretation and discuss its
relevance for the CoVer project (Combining Verification Methods in
Software Developement). The goal of this project is to build a tool
where functional programs can be verified by a combination of
testing and interactive and automatic theorem proving. The
functional programs are written in Haskell and thus the underlying
logic need to contain inference rules for reasoning about general
recursive and lazy programs, and I will discuss some possible
approaches.
λ. John Hughes (Chalmers University of Technology, visiting AIST CVS) "Random Testing with QuickCheck"
One important use of formal specifications is in software testing:
specifications can be used both as test oracles, and also for test
case selection. The latter may require manual analysis of the
specification, though, making this step relatively costly and
indirect.
In this talk I will describe a tool we have developed, which
provides a restricted (but surprisingly powerful) formal
specification language in which specifications can be interpreted
directly as test suites. The key idea is to interpret universal
quantification in properties as random test case generation. The
tool works well in practice, and the ideas have been used to test
functional, imperative, and concurrent code. The original
implementation is now distributed along with the standard Haskell
compilers, and the ideas have been ported to (at least) ML, Scheme,
Erlang, Python, and Mercury.
QuickCheckの紹介。 QuickCheckのアイディア自体は非常に単純。QuickCheckはテストのためのフレームワークなのだけど、個々のテストデータはユーザが記述するのではなく、システムがランダムに自動生成する。そして、ユーザによって記述された性質が、それらのランダムに生成されたテストデータに対して満たされているかをチェックする。もちろん、実際には色々な問題があるのだけど、それらはHaskellらしい方法で解決されてる。(追記予定)
Erlang, C. Scheme, Common Lisp, Python, Mercury, ML, ... に移植されているそうだ。Pythonに負けるのは癪なのでRubyにも移植しよう。
それはそうとプレゼンがとても上手だった。私もこんな発表が出来るようになりたいものだ。(追記予定)
λ. Yoshiki Kinoshita (AIST Research Center for Verification and Semantics) "Is modal mu calculus enough for verifying reactive systems?"
(追記予定)
2004-05-12 [長年日記]
λ. "Types for Verification" 2日目
.
λ. Ken-etsu Fujita (藤田 憲悦) (Shimane University) "Bijective CPS-translations between λμ-calculi and λ-calculi."
I will talk about bijective CPS-translations between λμ-calculi
and λ-calculi.
M.Parigot introduced the λμ-calculus as a formal system
of second order classical logic and investigated the computational
meaning of classical proofs. On the other hand, the term
CPS-translation, in general, denotes a program translation method
into continuation-passing style that is the meaning of the program
as a function taking the rest of the computation. From a
programming point of view, the CPS-translations in this talk make
it possible to simulate computations of call-by-name calculi by
those of call-by-value ones. First, I provide a CPS-translation
from type-free λμ-calculus into λ-calculus. Then
it is briefly shown that the CPS-translation forms a bijection by
defining an inverse translation back to the source calculus (This
result was presented at TLCA'03). Next, in order to carry over the
technique in the type-free case to polymorphic
λμ-calculus, I give technical problems about
- the target calculus corresponding to the source,
- the denotation of λμ-types, and
- the inverse translation and extensionality of the source calculus
together with ideas to solve them. Finally, I discuss by-product of
the main result.
CPS変換の像(とその簡約結果からなる)集合Univと、もとのλμの項全体の集合Sの間に全単射があるのだけど、CPS変換結果を簡約しても問題ないという点に少し驚いた。ただ、僕はλμ計算については「call/ccみたいのを直接扱える体系」くらいの認識しかなくてシンタクスを知らなかったので、いまいちよく分からなかった。けど、結構面白そうな話なので、後でちゃんと調べてみたいところだ。とりあえず、P.Wadlerの"Call-by-value is dual to call-by-name"でもあたってみるか。
λ. QuickCheck再び
QuickCheckについてもう少し詳しい話を John Hughes さんに講義してもらった。Erlangには型が無くてオーバーローディングも無いからErlang版ではちょっとトリッキーなことをする必要があったという話で、急に「Rubyはどう?」と話を振られてしどろもどろになってしまった。英語の出来る人がうらやましいなぁ。
λ. 昼食
に行くときに John Hughes さんに"Generalising Monads to Arrows"に書かれていた type restrictions on datatype
(2004-04-10の日記を参照) について質問した。Haskellの仕様を変更する予定とか可能性はないかと訊いたたら、以前にプロポーザル("Restricted Datatypes in Haskell" かな?)を書いたけどそれには最適化(?)の問題があって、今新しいのを書いてると言っていた。
昼食は近くの豚カツ屋(?)さん。池上さんとJohn Hughes さんと同じテーブルで、今度は日常の話をしてたのだけど、ほとんど聞き役な私。あと、それにしてもワンピースやエヴァンゲリオンの話が出るとは思わなかったYO。
λ. 神戸大へ
佐藤さんの紹介で、神戸大の菊池誠先生を訪ねた。Channel Theory や状況理論の話を色々と教えてもらう。
Channel Theory は(集合論のように)非常に一般的な枠組みだから扱おうと思えば何でも扱えてしまうから、何をトークンとし何をタイプとすべきかを一度状況理論に立ち返って考えているとか。
Goguen の Institution のバックグラウンドに J.Barwise の Abstract Model Theory があるというのも初耳だったので驚いた。Abstract Model Theory というのは、J.Barwiseによる無限個のQuantifierを許すような論理体系の研究がきっかけになって作られた、言語とモデルに関する一般理論……という話だったと思うのだけどちょっと記憶に自信がない。詳しくは、『Model-Theoretic Logics』(Edited by J.Barwise, S.Feferman) や "Axioms for Abstract Model Theory", J.Barwise あたりを読むといいらしい。
それから、Formal Concept AnalysisのグループではLatticeを使って割と似たようなことをしているらしいくて、これも興味をそそられた。『Formal Concept Analysis: Mathematical Foundation』(Bernhard Ganter, Rudolf Wille)という本も出ている。
λ. 帰り
この2日間はすごい充実してたので2日間で帰ってきてしまうのが惜しく感じられてしまう。1月くらい産総研みたいなところに滞在して、彼らと色々議論してみたいものだなぁ。そうすれば、僕みたいなダメ人間にも研究っぽいことが出来そうな気がする ;-)
ともあれ、次にくるときは話を聴きに来るのではなく、発表するために来たいものだ。
2004-05-16 [長年日記]
λ. 小沢一郎氏、民主党代表就任を辞退・年金「未加入」判明
なんか、政治責任とか小泉首相と刺し違える云々よりも、未加入云々は単に口実で、参院選の責任を取らされるのを恐れて日和ったんじゃないか。って印象を受けたんだけど、ひねくれてますかね?
2004-05-22 [長年日記]
λ. Rena (4)
2/19からだいぶ間が開いてしまったが、久しぶりにちょっといじった。Exclusive XML Canonicalization をバータリーで何とかするために、XMLをファイルに落としてlibxml2のおまけのtestC14Nに丸投げしてみる。approved_20031114の関係するテストケースに通った。
一応「<XPath>(//@* | //namespace::* | /*[3]/*[1]/*[1]/descendant::node())</XPath>」みたいなのをファイルに書き出して「testC14N --exc-with-comments XMLファイル名 XPathファイル名」みたいな感じで呼び出してる。XPathについてほとんど知らないのだけど、これであってる?
ホントはこんなバータリーな方法ではなく自前で Exclusive XML Canonicalization の実装を持ちたいところなのだけど、これ以上REXMLに触れたくないし、どうしたものか。
2004-05-23 [長年日記]
λ. "Restricted Datatypes in Haskell", John Hughes (Chalmers University, Sweden)
を読んだ。ここで提案している拡張では、「datatype Eq a => Set a = ...」という型があったときに、「member :: wft (Set a) => a -> Set a -> Bool」のようにwft(well-formed type)を文脈に書くことによって、Set a が制約を満たして構成された型であること(この場合 Eq a であることを意味する)を書く。直感的にはこのwftは不要なように思えるが、確かに無くせないんだよなぁ。うーむ。
それと、ここで書かれている constructor-polymorphic がどういうものなのか良くわからなかった。
【2006-03-26 追記】 constructor-polymorphic は単に型構築子に関して多相的ってだけで、特別な意味はないか。何でこんなのが理解できなかったのか不思議。それはそうと、restricted data types は haskell-prime でも議論されていた(1,2,3)。その中に出てきた Restricted Data Types Now が技巧的でちょっと面白かった。
2004-05-24 [長年日記]
λ. Nullable Types
HaskellでいえばMaybeモナドみたいな感じか。
【追記】 しかし、Nullableよりも、値からNullを除くNonNullableみたいなものの方が、ずっと必要性は大きいと思う。
2004-05-26 [長年日記]
λ. 借りた本
- 『エシュロンと情報戦争 』
- 鍛冶 俊樹 [著]
- 『ブギーポップ・スタッカート—ジンクス・ショップへようこそ』
- 上遠野 浩平[著] 緒方 剛志[イラスト]
- 『第61魔法分隊 (2)』
- 伊都 工平 [著], 水上カオリ [イラスト]
- 『召喚状 (上) 』
- ジョン・グリシャム(John Grisham) [著], 天馬 龍行 [訳]
- 小説すばる 2004年2月号
- -
2004-05-29 [長年日記]
λ. Rena (5)
色々とダメダメだけど、こっそり公開。rena-0.0.1.tar.gz
λ. [ruby-dev:23634] Re: NEWOBJ() in dfree
そういえばRuby-GNOME2もdfree()内でRubyのコードが実行される可能性があるなぁ。というのも、destroyシグナルのようなシグナルにシグナルハンドラを結び付けていると、dfree内でオブジェクトが開放された際にそれが実行されてしまうため。
λ. 某コンサート
気まぐれで、某コンサートのお手伝い。小学校の頃の同級生に会う。
λ. "A New Notation for Arrows", Ross Paterson
を読んだ。「κpat -> cmd」なんてどっかで見たような文法が出てきて、おやっと思ったら、やっぱり"Decomposing Typed Lambda Calculus Into a Couple of Categorical Programming Languages"のκ-calculus 繋がりだった。Arrow とは全然関係ないと思っていたので、こういう繋がりがあるのは意外で面白いな。
[2005-04-30 追記] ArrowZero は zeroArrow >>> f = zeroArrow と f >>> zeroArrow = zeroArrow という強い性質を要求しないため、単に ArrowPlus の <+> の単位元という位置づけでしかない。でも、それならば ArrowZero を ArrowPlus から独立したクラスにすることに何の意味があるのか?
2004-05-30 [長年日記]
λ. tDiary 1.5.7
毎日のようにpstoreのデータファイルが壊れるのにうんざりしたので、tDiaryのバージョンを1.5.7に上げてtDiary2形式にした。データはpstoreのままでRubyを1.8に上げるという手もあったけど、ITCに1.8を入れるようリクエストするのが面倒だったし、1.8.1は[yarv-devel:139]で懲りているので今回は見送り。
