研究集会
科学的実在論者でありながら、数学的対象に関するフィクショナリストであるにはどうしたらよいのか。 通常、科学的実在論者は下記のパットナム流 indespensability argument によって数学的対象の実在論にたどり着く 電子などの理論的対象は、自然現象を説明…
ワークショップ二日目。なぜか、教室に張ってあるワークショップ名の張り紙が、昨日アナウンスのあった公式タイトルとは違っていた。謎だ。印象に残った講演は以下の通り。内容については、昨日と同様、近いうちに、講演のスライドが公式web siteで更新され…
本日から開始＠数理解析研究所。印象に残った講演は以下の通り。内容については、近いうちに、講演のスライドが公式web siteで更新されるようなので、それから紹介します。 "Inductive Cyclic Sharing Data Structures" （浜名 誠）
16時より17時半まで、出席者は10人程度。（内容については後日追加します）
先週月曜日の講演会の内容紹介。当エントリーは、まだまだ暫定版で、これから修正が必要です。内容について、ご意見／誤解のご指摘をいただければ幸いです。 (1)数学の論理的基礎(logical foundation) v.s. 認識論的基礎(epistemological foundation) 数学の…
談話会で発表、参加者8名、16:00-16:45。情報処理学会での発表の内容増補版、タイトルに「、」が増えている点がその増補っぷりを物語る（寒）。 （内容は後で追加します） これで、地獄の発表シーズンもやっと幕。この6週間の間に、論文締め切り1、3カ所に出…
＠京都大学文学部。座長は Graham Priest、講演者は Bob Hale という超豪華メンバーの講演会。要旨は以下の通り（参考のために転載いたします、問題がある場合はご連絡ください）。 In seeking a foundation for mathematics, one may be looking for a sing…
業務研究の内容（Agdaで知識様相論理の体系を実装する）について発表しました。発表の出来はそれなり、会場の受けは一応好評でした。要旨は以下の通りです。 目的: 知識様相論理の意味論を証明支援系に実装 二つの問題点 多変数述語を持つ型のデータ型の定義…
16:50-17:50。講演の要旨とスライドはここより入手可能。 "Mas problem"とは、Medvedevによって始められた一般化された決定問題である。この問題を考えることで、最終的には決定不可能な問題を分類することを目的としている。 通常のTuring degreeでは、で、…
15時より15時半まで。発表の出来そのものは普通でしたが、はい、久しぶりに失敗したという感じがしました。 というのも、今回の発表の骨組みは昨年夏イギリスで発表したときのものだったのですが、非古典論理の代数的意味論の専門家たち向けでした。今回は聴…
午前の部では座長、複素解析についての逆数学と部分的ランダム性について。Lさんの講演が時間オーバーしかかってヒヤヒヤする。午後はゲームの決定性とマス問題に付いて。
14時より17時まで。二階算術における強制法をsyntacticalにやる方法についてと、マーティン=レフ-ランダム性とチャイティン-ランダム性の同値性について。Simpson氏も盛んに質問していた。
2月21日に、Stephen G. Simpson 氏の訪問にあわせて開かれる仙台ロジックセミナーにおいて、発表をすることになりました。内容は昨年夏イギリスで発表した内容の補足です。ご興味のある方はお越し下さい。
コードをコンパイルするとき、実行ファイルを効率化して実行時間などを最小化するコンパイラ最適化にはいくつもの方法がありますが、今回はSSA形式の話です。SSA ではまずファイルを各変数への代入が一箇所だけで行われる形に変換し、最適化（余計なコードの…
ポインターに関するプログラムで、同じ意味だろうと思って下手に書き換えると、実は文脈によって違った挙動を示してしまうことがあります。では、安全(safe)な書き換えとは何か？西村氏はそれをプログラムをseparation logicの論理式の predicate transforme…
東北大の富山先生による、項書き換え系の有名な定理：二つのconfluentな項書き換え系で、関数記号や定数記号を共有しないものは modularity を持つ、の前提条件を減らして証明した、という話。Terminationする場合は簡単だが、もちろんTerminationしない場合…
物理ではシミュレーションはもはや不可欠な道具だが、シミュレーションに関して 定量的な議論はできるが、定性的な議論はできない モデルの妥当性を問うことが難しい（シミュレーションが変な数字を出してきて初めて前提のおかしさに気づく） という問題があ…
MLLの proof net の集合上に、error-correcting コードでよく使われるやり方を応用して距離を定義する。今回はアイディアのみ。T氏曰く「Linear Logicへの愛を感じる講演」でした。
アセンブラで書かれたプログラムをモデル検査した事例の報告。モデル化するだけで見つかるエラーは少なくないが、一方で、状態爆発が起こるため実際のモデルを動かすのは大変らしい。
東大のS氏と共同のワークショップ。司会は世話人のAr氏、観客は6人で論理関係者が多い。私が集合の境界不在性と縮約規則、外延性の関係について。私の話は、θの定式化が不自然とMn氏から指摘を受ける。返答の際は頭がボケていて、答えるべき二つのこと（θと…
「2007年度 哲学若手研究者フォーラム」（＠代々木・オリンピック記念青少年総合センター）の場をお借りして、東大のS氏と共同で、ワークショップを開かせて頂くことになりました。7月22日（日）12:30-14:30の予定です。この場を借りて宣伝させて頂きます。…
セキュリティ・プロトコルについて概説。BAN Logicを中心とした歴史の説明。次回はPCL。 Needham-Shroeder公開鍵認証プロトコルは、BAN Logicで安全性が証明されたにもかかわらず、実はアタックがありうることがLoweによって示された（PCLに拡張するとこのア…
関数型言語に対応する計算はλ計算、それに対応するのは Cartesian closed category。プロセスに対応する計算といえばCCSやπ算法、それではそのカテゴリー的対応物は？ 一応、Abramskyの interaction categories が提案されているが、ちゃんと定義が与えられ…
16:00-17:00 0とsuccessorとrecursorを持つsimple typed calculusをprimitive recursive functionalの中に埋め込むGandy translationを使って、strong normalizationの証明においてnormal formにいきつくまでのreductionの列の長さのupper boundを求める。up…
談話会*1、1階述語様相μ計算の通常の公理系は「一般モデル」に関して完全となるという話。古典2階論理とのanalogyで証明がうまくいく。とても面白かったです。 その後飲食、阪急線の終電に乗り、駅から歩いて家まで帰る。帰宅後Cと録画した「らき☆すた」を見…
Distributed conflict resolution problems （ネットワークに繋いである一台のプリンターを複数のPCで使うとき、みんなが一斉にプリントしようとすると困るので交通整理が必要という話）についての Quorum system によるアプローチ。中央に司令塔があるToken…
過去のエントリーを見てみると、学会や研究集会に参加して、他の人の発表の内容を記録したりしなかったり、いまいち基準が不明確に見えます。自分なりの基準として 自分の発表はここにメモっておく（あとで出張報告を書くときなど便利） 発表者が1-2人ぐらい…
16:00-17:00 線形時間論理の2つのシーケント計算体系の同等性およびcut除去の概要、また分岐時間論理の拡張 4CTL*（4-valued CTL）、 4LCTL* （4CTL+場所）の紹介。背景説明が主。 17:00-18:00 プログラム更新システムのプロトコルの、 信念を表すBAN logic…
産総研CLC、16:00-17:30。最近はやりの SaaS (Software as a Service)などを裏で支える、個別サーバーの故障やネットワークの断絶を乗り越えて複数のサーバーを安定的にサービスを維持する（sustainする）システムの開発。ネットワーク障害からの復旧後の「…
産総研CLC、13:30-15:00。様相論理KTBを含む normal modal logic の生成する latticeの、Splittingに関する構造について、他の体系の結果と比較しつつ。KTBのlatticeはかなり他と似ているらしい。難しかったけど、面白かったです。
