日々の流転

λ. CATS & DOGS

CATS & DOGS っていう映画を茅ヶ崎のマイカルで見て来た。前回の失敗を鑑みて海岸沿いを通ってたんだけど、こんどは早く着きすぎた。映画の出来はなかなかだと思う。僕は吹き替えよりも字幕がよかったな。ケシゴムは辛口の意見だけど、¥1400分の価値はあったと思うので、今日は満足。

λ. 情報数学ⅠのSAに

情報数学ⅠのSAに登録しました。正直僕なんかでつとまるのか不安なのですが、精一杯がんばりたいと思います。お給料も貰えるようですし… (^^;;

λ. SWI Prolog に戻った

というわけで、GNU Prolog はちょっと不便だったので SWI Prolog に戻った。

んで、某先生の昔のコードの解読に苦しむ。Prologって型無し言語な上に入力と出力の区別がないからなぁ。無愛想な変数が多量に並んでるとちょっとお手上げ気味。

λ. EXTERN

まつもとさんは「ruby_errinfoの値を参照するのは許されています」と言うけど、ruby_errinfoのようなEXTERN無しで宣言されている変数を拡張ライブラリから参照して、Windows版でまずくないのかなぁ。逆にEXTERNの付いていない変数を拡張ライブラリから参照できるとしたら、EXTERNの意味って何?

λ. 明日

晴れると良いな。とはいっても返さなくちゃいけない本があるので、どっちにしても学校にいかなきゃいけないんですが…

λ. コンパイラ構成論

lex

λ. 知的財産権論

著作隣接権の続き。

λ. 企業会計論

1. 複式簿記の手続き
   複式簿記カッコいいー
2. 会計ビッグバンと日本的経営
   • 連結会計 (改訂)
     支配力基準の導入
   • 時価会計 (新設)
   • 年金会計 (新設)

一般に取引と見なされていないもので簿記上の「取引」になるものの例としては盗難や災害があるそうだ。逆に、一般に取引と見なされているもので簿記上の取引と見なされないものの例は「契約」そのもの等が有るらしい。(後者は議論もあるらしいが)

デリバティブ取引は昔は決済まで簿記上の取引とは認められていなかったが、最近はオンバランス化されるようになったらしい。

λ. Professor Robert Kowalski's lecture

論理プログラミングの偉い人である Robert Kowalski 教授の講演会があったのだけど、同じ時間だった企業会計論の方に出ていたので出れなかった。もったいない事をした。

Title:

Can Computational Logic teach people how to think?

Abstract:

Symbolic logic was originally developed as a tool to improve human reasoning. In the first half of the twentieth century, it made important contributions to the foundations of mathematics. In the second half of the century, it was further developed and greatly extended for computing applications, including databases, programs, program specifications and artificial intelligence.

In this talk, I will argue that the resulting, enhanced and extended computational logic can also be used directly by people to improve their own communication and reasoning abilities.

Computational logic extends classical symbolic logic in a number of important ways. It incorporates default reasoning, which allows general rules to be defeated by evidence to the contrary, as in the case of the rule that a person is innocent unless proven guilty. It also incorporates meta-level reasoning, which allows rules that reason about rules, as in the case of acquisition of citizenship by adoption, which states of itself that it continues to apply even if the adoption order later ceases to have effect.

The tools and techniques of computational logic can be described and applied informally, and do not need to be expressed in symbolic, mathematical or computer-oriented form. In my talk, I will illustrate some of the applications of informal computational logic in such areas as legal reasoning and human-to-human communication. I will argue, in particular, that people can use the principles of computational logic to express themselves more clearly, more coherently and more effectively in natural languages such as English. In doing so, because human language is intimately associated with human thought, they can not only improve their ability to communicate, but can also improve their ability to think.

λ. 論文読み会 "Java 2 Platform Micro Edition"

個人的には "JDK 1.2 Security Architecture"の部分をもう少し丁寧に説明して欲しかったかも。

参考: Java仮想マシン入門： ベリファイ編(3)

λ. 夕食

バーミヤン。

λ. net stumbler

というツールが面白いらしい。

λ. 温COM知新 (おんこむちしん)

某日記(2002-10-28)より。

λ. 読書

『オフィス北極星 3』

『オフィス北極星 4』

『オフィス北極星 5』

真刈信二[著], 中山 昌亮[イラスト]

λ. RSS 2.0

LtUを見ていて、RSSに2.0が有るのを知った。しかも「RDF Site Summary」ではなく「Really Simple Syndication」らしい。

"What's Wrong with RSS 1.0?"

λ. 某所のダメな会話のサマリ

問題意識

「K君はボンデージとかは嫌いなんだろうなぁ」

研究

「ボンデージにヒラヒラとかがついていたらどうだろう?」

λ. 第三十四回圏論勉強会

今日は圏論勉強会だった。 “Categories, Types and Structures” Section 2.3.6 Propositionより

写真

【2007-11-13追記】 Proposition 2.3.6 では reflexisive object V に V×V を埋め込めることを示すために、非常に面倒くさい計算をした。 CCCの射として明示的に書き下しているので煩雑すぎて本質が見えにくかったが、落ち着いて考えてみれば簡単で、CCCのinternal languageとしてラムダ計算を使うならば、単に直積型のチャーチエンコーディングに過ぎない。

関連

• 圏論勉強会 - たけをの日記＠天竺から帰ってきたよ
• デカルト閉圏におけるお絵描き計算の基礎 - 檜山正幸のキマイラ飼育記

λ. seqはHaskellの意味論では扱えない?

• <URL:http://alohakun.blog7.fc2.com/blog-entry-812.html#comment1712>
• Haskell: seqってよくわからない - lethevert is a programmer

seqの意味がHaskellの標準的な意味論で扱えないかのように思われがちなのは何故だろうかと思った。

【追記】 lethervertさんの場合は、Haskellの公式の意味論でseqの操作的意味を確定出来るかという疑問だったので、実際には違う話ではあったけど。

λ. Seven Trees やっと解けた

一部で流行っていた Seven Trees の問題。 乗り遅れてしまって、等式変形をどうやるのか一人寂しく悩んでいたのだけど、Tⁿ + Tⁿ⁺³ = T^m + T^m+3 が成り立つことに気づいて、ようやく等式変形が出来た。

• 1 + T³ = 1 + T² + T⁴ = T + T⁴ = T(1 + T³)
• 帰納法により 1 + T³ = Tⁿ + Tⁿ⁺³
• よって Tⁿ + Tⁿ⁺³ = 1 + T³ = T^m + T^m+3 for all n, m
• ゆえに T = T⁰+T² = T⁰+(T¹+T³) = T¹+(T⁰+T³) = T¹+(T⁴+T⁷) = (T¹+T⁴)+T⁷ = (T⁶+T⁹)+T⁷ = T⁶+(T⁷+T⁹) = T⁶+T⁸ = T⁷

等式変形が出来たら、同型の証明をAgdaで書こうと思ってたのだけど、関数として書くのが案外面倒そうなので、なんだかもういいやという気分になってしまった。 しかし、中野さんの5種類のパターンの分岐で定義ってのは分からなくて、気になるなぁ。

関連

• Seven Trees：解答のトラックバック受け付け所