日々の流転

λ. 買った本

• 「魔術士オーフェンはぐれ旅　我が運命導け魔剣」秋田禎信
• 「国際情勢の見えない動きが見える本」田中宇
• 「新しい歴史教科書」
• ダ・ヴィンチ　7月号

λ. 借りた本

• 「ドクター・ハマー　私はなぜ米ソ首脳を動かすのか」　アーマンド・ハマー(Armand Hammer)[著]　広瀬隆[訳]
• 小説すばる　2000年11月号
• 「MISERY」　スティーヴン・キング(Stephen King)[著]　矢野浩三郎[訳]
• 「現代思想の冒険者たち 24　クーン　パラダイム」　野家啓一[著]
• AERA　No.22

λ. tDiary

「<」で始まるHTML直書きの段落にサブタイトルを付けると、bodyの各行がPエレメントに含まれてしまう。例えば、こんな風に書いても意図したようには展開されない。

サブタイトル
<ul>
<li>その1
<li>その2
</ul>

ので、rhtmlを適当に直した。後でただただしさんに報告しとこ。ああ、eRubyって素晴らしい。

λ. Definite Clause Grammar

論理プログラミングの前回の授業の演習問題を今頃になって解いている。差分リストの嬉しさはまだ良くわからないけど、DCGはPrologの真骨頂って感じで感動。

λ. ふう

と、ここまでで今日は時間切れ。いっちーさんに頼まれていたお仕事とかは仕方無いので土日に持ち越し。あとは、データ分析の宿題だけ処理してもう寝よう。お休みなさい。

λ. アルゴリズム論のレポート

BとCを選択したのだけど、結局Bしか間に合わなかった。Bの方を書いているうちに、せっかくなのでこの機会にLaTeXを勉強してLaTeXで書いてやろうじゃないかとか思い出したのが間違いだった。阿保すぎる。

それにしても、LaTeXのようなシステムを世界中の人が使っているというのは、何だかおぞましい。

λ. 語種選択

落としたままというのは悔しいので、また朝鮮語を選択してしまったよ。

λ. 読書

『吸血姫夕維　香音抄　一』

垣野内成美[画]

λ. λ in C++

• Lambda Abstractions and Currying in C++
• The Super Programming Technique - ラムダ式をC++で実現する

楽しげ。

mots quotidiens. (2002-06-05) より

λ. 夕食

豊田さんと中村さんと。しそラーメン。

λ. 今日のITシステム

• -
• -
• A Diagrammatic Inference System for the Web

僕は参加しなかったが、今日のITシステム後には人生ゲームをしていたらしい。人工知能学会創設20周年記念の「Happy Academic Life 2006: 研究者の人生ゲーム」というやつ。

λ. CCC と *-autonomy

先日のIntroducing categories to the practicing physicistに以下のようにあったが、これはどう示すのだろう?

Proposition. A symmetric monoidal category which is both cartesian closed and *-autonomous can only be a preordered set.

まず、hom(A,B) ≅ hom(1,A⇒B) ≅ hom((A⇒B)*, 1*) ≅ hom((A⇒B)*, 0) 。 一方、CCCは分配的な圏なので 0≅0×0 であり、hom(A,B) ≅ hom((A⇒B)*, 0) ≅ hom((A⇒B)*, 0×0) ≅ hom((A⇒B)*, 0) × hom((A⇒B)*, 0) ≅ hom(A,B) × hom(A,B) となる。 ここから、hom(A,B) は空集合か一点集合か無限集合であることがわかる。 あとは無限集合でないことを言えばよいのだけど、これをどう示したらよいかわからない。

【追記】 もっと単純な話だった。 もし、f: X→0 が存在すれば、 <id, f>: X→X×0 と p: X×0→X が inverse になっている。 p ∘ <id, f> = id は明らかで、 <id, f> ∘ p = id は X×0 ≅ 0 が始対象であることから言える。 なので、X ≅ X×0 ≅ 0 。 したがって、hom(A,B) ≅ hom((A⇒B)*, 0) は空集合か一点集合。

【追記】 ところで、A⇒0 を ¬A と書くことにすると、これは CCC に A≅¬¬A を加えると縮退してしまうということを言っていていて、古典論理に対応する圏を作ることの難しさを示している。 そういえば、古典論理に対応する圏を作ることが難しいことは、檜山さんの「論理とはなにか？ (4:完) -- 論理から圏へ」のところでも言及されていた。

λ. 『λに歯がない』 森 博嗣

を読んだ。 Gシリーズは正直微妙だと思ってたけど、今回のは結構好みの話だった。 この傾向が続くといいなぁ。

λ. 計算と論理のための自然枠組NF/CAL by 佐藤 雅彦

本論文では，計算機上での証明記述および検証を支援するシステムNF/CALを紹介する．NF/CALの設計はフレーゲによる判断の分析の影響を受けており，人間が自然言語を用いて日常的に行う判断活動を自然に形式化したものになっている．

ずっと積読中だったものを消化。ワークショップの“Types for Verification”で“A simple theory of expressions”という講演を聴いたときには何が嬉しいのかよく分からなかったが、以下に引用する部分を読んでようやく動機が理解できた。

これらのシステムの多くは型理論に基づいており，もっぱら専門家による使用を前提としている．そのためシステムの利用には型理論の知識が必要となり，学部で計算や論理を教育するためのシステムとしては不適当である．本稿で紹介した式の理論は，計算や論理の基礎的事項を，最初から説明するための必要性から考案したものであるが，同時に我々が日常的に用いる自然言語が本来持っている構造を自然に反映したものになっている．

しかし、NF/CAL面白そうだな。 CALは昔使わせてもらったことがあって、そのときには挫折してしまったのだけど、出来たらまた試してみたいものだ。

λ. 数学基礎論の考え方・学び方

講師

田中 一之 （東北大学大学院理学研究科数学専攻教授）

題目

数学基礎論の考え方・学び方

内容

ゲーデル以降，数学基礎論は何をしてきたか？ この講演では，論理，ゲーム，超限帰納法，不完全性などの基本概念を軸にして，数学基礎論の深化発展を振り返り，さらに最近の研究動向の例として私と仲間たちの研究も紹介する．

ポスター

これを聞きに行ってきた。

メモ

書きかけ。

• 数学基礎論とは何か?
  • 欧米ではロジックという呼び方が普及している。そのなかで数学の基礎を研究している人がいる。
• 現代論理学の始まりは不完全性定理を発見したとき。
  • 1930年9月5日 精密科学認識論会議 初日 各1時間の講演
    • カルナップ 論理主義
    • ハイティング 直観主義
    • フォンノイマン 形式主義
  • 翌日ゲーデルが完全性定理に関して20分の講演をし、(第一)不完全性定理についても簡単に触れた。
• 中世の普遍論争と比較すると
  • クワイン「何が存在するかについて」
  • 論理主義 = 実在論(realism) … プラトニズム
    • 普遍者は心の外に存在し、発見される
  • 直観主義 = 概念論(cenceptualism)
    • 普遍者は心の構成物として発明される
  • 形式主義 = 唯名論(nominalism) … オッカム
    • 普遍者は個物を抽象化した名前に過ぎない
  • ウンベルト・エーコ「薔薇の名前」
• 数学の思想対立の流れ
  • いろんな直観主義がある
  • カントル集合論 vs. クロネッカー算術化
  • ラッセル論理主義 vs. ポアンカレ直観主義
    • ポアンカレは数学的帰納法の論理的明証性を主張、非可述的定義を禁止
  • ヒルベルト形式主義 vs. ブラウワー直観主義
• 不完全性定理とヒルベルトのプログラム
  • イデアルな数学 … 無限とかを含む
  • リアルな数学 … 写実的な数学。有限記号列を有限に扱う
  • 記号化還元 : イデアルな数学→リアルな数学
  • コード化/算術化 : リアルな数学→イデアルな数学
  • HP1 : イデアルな数学からリアルな数学への還元
  • HP2a : リアルな数学の無矛盾性 x ← 第二不完全性定理
  • HP2b : リアルな数学の決定可能性 x ← 第一不完全性定理
• 不完全性定理
  • 第一不完全性定理から導かれる重要な結論は、再帰的でない集合の存在。たとえば、PAの定理のゲーデル数の集合 { ⌜A⌝ : PA ⊢ A } は再帰的でない。
• 再帰理論の点からの発展
  • Church
    • Kleene
      • Addison
    • Rosser
      • Sacks
        • Friedman
        • Simpson
        • Harrington
    • Turing
      • Gandy
        • Paris
  • KleeneとAddisonによるeffective記述集合論
  • Kreisel, Kripke, Sacks らによる admissible集合論
  • Friedmanが2階算術と逆数学について研究
  • ParisとHarringtonが新しい独立命題を発見
• 再帰理論はなぜロジックか?
  • ホップス … 唯名論、唯物論
    • 「あらゆる推論は、加算と減算に還元される」
  • ライプニッツ
    • 「ペンを持ち、机に向かい、計算しよう」
  • ブール
    • 「論理の計算」
  • ド・モルガン
    • 「形式論理学あるいは必然と可能の推論計算」
  • ヒルベルト
    • 「決定問題が数学論理学の中心問題である」
• 余談・集合論の誕生
  • 三角級数の一意性の問題
  • 加算順序数であれば実数に埋め込める
  • カントル・ベンディクソンの定理
• 公理的集合論のモデル
  • 1930 ツェルメロは集合論の累積階層モデルVを提唱
  • 1938 ゲーデルは集合論の構成可能モデルLを発明
• ゲーデルの重要コメント集
  • 「構成可能」という語は、非可述的方法を遮断する直観主義的意味に理解されたい。
  • 構成可能集合とは、ラッセルの分岐型理論を超限順序を含むように拡張して得られる集合である
  • 集合論は、それ自体で閉じた公理系をなしているのではなく、新しい公理によって拡張を行うように促している。そうした公理は、非常におおきな基数の存在を示す公理として形式化できる
• 余談. 連続体仮説の独立性
• 2階算術 = Hilbert-Bernays算術
  • 実連続関数は、可算個の有理数上の値で決定されているので、自然数の集合で表せる
  • RCA₀ は計算機の扱える数学
  • WKL₀ は RCA₀ に弱Königの補題を追加したもの
  • Π¹₁式で定義される集合の存在を要請する公理をRCA₀に加えたものがΠ¹₁-CA₀である。無限ゲームの決定性はこれをすぐ超える。
• ゲームの理論について
• ヒンティッカ・ゲーム 197?
• メタ・ヒンティッカ・ゲーム (T 1986)
  • Player I: 論理式φを選ぶ
  • Player II: 真か偽を選ぶ
  • 補題. I は必勝法を持たない
  • 補題. II が必勝法をもてば真偽が定義できる
  • 系. Δ⁰₁ゲームの決定性はPAでは証明できない
• 無限ゲーム
  • 注: Δ¹₁の決定性はZFC集合論で証明可能であり、その必勝法はΔ¹₂集合で見つけられる
• 二階算術と無限ゲーム
  • Δ¹₁の決定性は Z₂ でも証明できない
  • Δ⁰₂の決定性は Δ¹₂内包公理から証明できない
  • アプローチ (注: メモしそこなってそう)
    • Δ⁰₂ 決定性を証明するために、Π¹₁超限再帰公理を導入 (Weak axioms of determinacy and subsystems of second order arithmetic の話?)
    • Σ⁰₂ 決定性を証明するために、Σ¹₁ 単調帰納的定義を導入 (〃 の話?)
    • Δ⁰₃ 決定性を証明するために、Σ¹₁ ……を導入 (Weak determinacy and iterations of inductive definitionsの話?)
  • 二階算術の命題として簡単に書けるのに、二階算術の普通の公理からはなかなか出てこないのが面白い
• 超限帰納的定義
• 参考文献
  • 数の体系と超準モデル
  • 確かさを求めて
  • 数学の基礎をめぐる論争
  • 逆数学と二階算術
  • ゲーデルと20世紀の論理学
• 逆数学
  • 定理の方が自明であって、公理の方を探す
  • 数学基礎論というと基礎付けるということに重点が置かれてしまうが、それが中心的テーマだったのはデーデル以前。ゲーデル以降はむしろ考え方を反対にしている。
  • 基礎付けられないものをもってきて、それに還元するよりも、複雑なものをもってきてそれがどれくらい複雑化をみている(⇒ 逆数学)。
  • 代数と幾何のように、どっちが基礎かというのは今はもう意味はない。両方から見れるのが面白い。

関連

• 非専門家向け数学基礎論の考え方・学び方 - かがみさんの日記(2009-06-06)

λ. STモナドとSTRefをHaskell上で実装する

[FAQ]Haskellには副作用があるのか、ないのか の話。 kazu-yamamotoさんはSTモナドを、「処理系の力を借りないといけないモナド」で、副作用や参照透明性の観点からはStateモナドと本質的に違うものだと主張している。 だけど、STモナドが処理系に組み込まれている理由は効率のためであって、意味的にはStateモナドと大差ないし、効率とあと細かい点を気にしなければHaskellレベルでも実装できるはず。 というわけで書いてみたのが以下のコード。

{-# LANGUAGE Rank2Types, ExistentialQuantification #-}
import Control.Monad.State
import qualified Data.IntMap as IntMap
import Unsafe.Coerce

type ST s a = State (IntMap.IntMap U) a
data U = forall a. U a
newtype STRef s a = STRef Int

runST :: (forall s. ST s a) -> a
runST m = evalState m IntMap.empty

newSTRef :: a -> ST s (STRef s a)
newSTRef x = do
  h <- get
  let key = IntMap.size h
  put (IntMap.insert key (U x) h)
  return (STRef key)

readSTRef :: STRef s a -> ST s a
readSTRef (STRef key) = do
  h <- get
  case h IntMap.! key of
    U x -> return (unsafeCoerce x)

writeSTRef :: STRef s a -> a -> ST s ()
writeSTRef (STRef key) x = modify (IntMap.insert key (U x))

あくまで proof of concept なので、コードを単純にするためにIntが溢れることとかは無視している。 それから、細かい点と書いたのは反則技である unsafeCoerce を使ってしまっているところ。ここでは等しい型と分かっている型の間でしか変換しないので、安全ではあるんだけれどね。

関連

• 関数型プログラマにとっての副作用
• Referential transparency, definiteness and unfoldability