過去・現在・未来

Coecke（ケックとよむのかしら？）とKissingerのこの本が、抜群に面白い。"Picturing Quantum Processes" 「量子過程を絵解きする」 https://goo.gl/hmRkKy Google Booksが、珍しく、ほぼ全文を公開している。円高なので本を買おうと思ったのだが、ほとんど見えないところがないことがわかって、僕はこっちで間に合わせた。 https://goo.gl/nhrKrB とおもったら、見えたのは昨日読んだ最初の100ページほどだった。しょうがない。本を買った。 少し前に、「15歳の時の自分に向けて書いた」というTerry Rudolphの"Q is for Quantum"  https://goo.gl/4ACBFm  を紹介したのだが、ケックとキッシンジャーのこの本も、難しい数学を使わなくても、量子論は理解できるという立場に立った本だ。 ケックには「幼稚園の量子力学」"Kindergarten Quantum Mechanics"  https://goo.gl/P4mGbn  という論文がある。さすがに幼稚園児には無理かもしれないのだが、その論文から10年以上かけて初志貫徹で、直観的で誰にでも理解できる量子論の立派な「体系」を作り上げた。立派なものだ。 「量子過程を絵解きする」の副題に、"A First Course in Quantum Theory and Diagrammatic Reasoning" とあるのだが、彼の方法のポイントは、「絵解き Picturing」「図解による推論 Diagrammatic Reasoning」である。 数学もプログラミングも、キーボードで「一次元」に論理を組み立てていく。そうではなく「二次元」の図形で考えてみようよということだ。 というと、なんか怪しく感じる人もいるかもしれないが、数学的にはしっかりしたものだ。カテゴリー論のみんなが大好きな"string diagrams" そのものだ。（このstring diagramは、Super string理論のstringとは直接の関係はない。いろいろ「因縁」があるので、そのことについては

1月29日、丸山の連続セミナー「楽しい数学」で「「同じ」を考える 」というテーマでセミナーを開催します。 https://mathnight4.peatix.com/ 日常のあたり前に見えることにも、すこし考えると当たり前ではないことが潜んでいます。今回は、「同じ」の数理を考えます。皆さんの参加をお待ちしています。 ---------------- セミナー概要 ---------------- 数学では、「同じ」「等しい」というのは、もっとも基本的な概念の一つです。 　「2 x 3 は、3 x 2 と同じである」 　「2辺とその狭角が等しい三角形は、同じ三角形である」 　「自然数と有理数は、同じ数だけ存在する」 　「ドーナツとコーヒーカップは、実は、同じ形である」 ただ、これらの例での「同じ」は、全く「同じ」ではありません。 日常でも、「同じ」という言葉は、よく使われます。 　「彼と僕の身長は同じです」 　「同じ時間、同じ場所で、共に過ごした仲間」 　「みな、同じ気持ちです」 　「この英語と日本語の文章は同じ意味です」 ここでも、「同じ」という言葉は、全く「同じ」ではありません。 これらの表現を、「同じ」という言葉を使わない表現で言い換えてみようとすると、とても難しいことに気づきます。それは、「同じ」という概念が、他の言い換えができないほど基本的な概念であることを意味しています。 セミナーでは、自明なように見えるが、多様さも併せ持つ、「同じ」の数理を探ります。セミナーでは、また、一昨年急逝した数学者のVoevodskyの「同一性」をキーコンセプトにした数学の基礎づけの試みを紹介します。

1/8マルレク「意味の形式的理論」と懇親会の様子です。資料のURL改めておしらせします。不都合がありましたら教えてください。 https://goo.gl/CPXndH

明日のマルレクの講演資料です。 https://goo.gl/CPXndH 　ご利用ください。資料長いのですが、背景がピンクのスライドをザッピングすれば、大まかな流れは伝わると思います。 ---------------- 「はじめに」 ---------------- 人工知能技術にとって、自然言語の意味の理解は、重要な課題である。小論は、自然言語の意味を形式的に把握しようという試みを概観したものである。 第一部では、まず、現在の主要な三つの自然言語処理技術の現状を紹介し、あわせて、言語の意味理解にフォーカスして、様々な取り組みを取り上げた。 こうした技術を評価する上で、筆者の取っている基本的な視点は、次のようなものである。 　　文と意味の「構成性（compositionality）」 　　意味の「同一性」 / 意味の共通表現の存在 残念ながら、文が語から文法に基づいて構成されることは、現在主流の自然言語処理技術では、ほとんど考慮されていない。文法性の認識がないのでは、文の意味の構成性の認識を持つことは難しい。 ただ、文の意味の構成性の認識なしにでも、意味については考えることができる。一つには文を構成する「語の意味」、もう一つには「意味の同一性」に基づく「意味の共通表現」の模索である。第一部の後半では、これらの取り組みを取り上げた。 「語の意味」の表現では、その客観性・共通性を「実在」の関係に基礎をもつOntology、語の利用の頻度の統計的分析に帰着させるWord2Vec的「分散表現」、辞書項目に諸特徴を枚挙するスタイル、 conceptual spacesを構成するアプローチ等多様な試みが行われている。 「文の意味」の表現については、論理式（あるいは、ラムダ式）による表現と多次元ベクトルによる分散表現の二つがある。後者は、実装者にはそういうものとしては、あまり自覚されていないようにみえるのだが。 機械翻訳技術の成功は、二つの言語の意味の「共通表現」を多次元ベクトルによる分散表現として抽出しているところにあると筆者は考えている。もっとも、語の意味も、文の文法性も、このアプローチでは、直接には考慮されていない。 筆者は、論理式による表現が「好み」なのだが、文から論理式への還元は、文法に応じて様々の流儀がある。この点

「アリー　スター誕生」みてきました。稚内で映画見たの初めてです。 稚内に映画館がなかった時には、映画が見たくて見たくて、東京に行くと一日三館はしごしたりしていたのですが、東京にいるといつでも見れると思うせいか、むしろ映画見る回数減りました。軟弱な映画ファンです。 主題歌の Shallow とてもDeepなこと歌っていることに気づきました。 　Tell me somethin', girl 　Are you happy in this modern world? 　Or do you need more? 　Is there somethin' else you're searchin' for? 　I'm falling 　In all the good times I find myself 　Longin' for change 　And in the bad times I fear myself ブラッドリー・クーパー演ずるアリーの夫の姿が、エイミー・ワインハウスのことを思い出させて悲しくなりました。（ホイットニー・ヒューストンでもいいのでしょうが、僕はエイミーが好きなんです）

あけまして、おめでとうございます。 今年もよろしくお願いします。 そのうち、僕は、あたまもおめでたい人になるのでしょうね。 その時は、よろしくお願いします。 浅知恵で、そうなる前にと考えて、昨年はやることを変えました。やりたいことをやれるうちに、できることをできるうちにやるのが、一番いいと思ったからです。残っている時間は自分ではわかりませんからね。それは若い人も一緒なのですが。 それまで何年かディープラーニング技術にフォーカスしていたのですが、関心を、量子情報理論・言語理論・数学の基礎の三つに切り替えました。三つの関心には脈絡がないように見えますが、僕の中では繋がっています。人工知能への関心は、結局、我々自身 -- 人間 -- の認識能力への関心に他ならないと考えています。 この30年間、IT技術の「ちょっと先の未来」について語ってきました。くじ運だけは強いので、クラウドでもモバイルでもAIでも、短期の予想は外れたことはありません。ただ、これからは、いろんな機会にいろんな形で、もう少し長いスパンで、人間と科学の未来について語ることができればと思っています。 なんの根拠もないのですが、21世紀の科学は、産業革命を準備した「科学革命」以来の大きな変革期に入るだろうという「予感」が僕にはあります。僕は自分の「予感」を信じています。 僕は、人間は、様々な危機を乗り越えて進むことができるという「希望」を持っています。「失望」には理由が必要ですが（例えば、「GoogleやFacebookには失望した」というような場合）、希望を持つのに理由は必要ではありません。絶望だって希望の十分な理由になります。 もちろん、未来を作るのは、僕ら古い世代の仕事ではなく若い世代の仕事です。僕らは、いずれこの世からいなくなります。 といっても、悲しいことに、若くてもなくなる人はいます。 僕が一番注目していた数学者Voevodskyは、一昨年、9月に51才で突然なくなりました。 昨年3月、僕の6つ下の弟がなくなりました。 昨年6月、20才で殺されたXXXTentacionの"Skins"を、この冬休み聴きました。前作のアルバム "？" を、僕は毎日聴いて泣いていました（嘘かも）。やはり、死んじゃいけないんですね。

先に、「同じ」型A に属する二つの項 aとb（a : A かつb : A）が「同じ」だという a = b : A で表現される「同じ」さと、二つの型AとB（A : Type かつB : Type）が同じだという A = B : Type で表現される「同じ」さは、同じ「同じ」でも、違う「同じ」であるという話をした。 前者は、例えば、Aを「三角形」という型だとして、三角形a と三角形b が「同じ」だと言っているのだが、後者は、例えば、Aを{異なる三つの点を結んでできる図形}、Bを{平行でない三つの直線で囲まれた図形}とした時、AとBは、同じ型の図形であることを主張している。 型を持つプログラミング言語の場合、あるインスタンスがどの型に属するかを意識することは大事なことだ。面倒と言えば面倒なのだが、そのことがプログラムの誤りを少なくするのに効果的なのだ。 型を持つプログラミング言語のうちのいくつかは（例えば、COQ, Agda, Haskell, 部分的にはScalaも）は、不思議な型 dependent type をサポートしている。dependent type は、パラメータによって（パラメータにdepend して）、型が変わる型だ。 パラメータxが型Bを持つなら、このdependent type E(x)を次のように表す。 　　　(x : B) E(x) また、あるsが、dependent type Eを持つことを、次のように表す。 　　　(x : B)  s(x) : E(x) あまり正確ではないが、B={ 整数、実数、複素数 }として x : B なるパラメータ x によって、dependent type E(x)は、整数型、実数型、複素数型 に型が変わるのだ。 昔のwakhok時代、同僚の浅見さんから、dependent type がすごいことはよく聞いていた。ただその頃、僕はそれをよく理解できなかったのだと思う。僕が、その重要性に気づいたのは、だいぶ後になってからだ。 5年前の2013年のマルレク「「型の理論」と証明支援システム — Coqの世界」で、ようやく後追いを始めることになる。 https://www.marulabo.net/docs/typetheory-coq/