過去・現在・未来

【「型の理論」入門 (4)  論理的推論（１）-- 判断と論理式を公開しました 】 https://youtu.be/1QnJRWLgOvI?list=PLQIrJ0f9gMcPC8_eEnysTwZm14VRaQWCT スライドのpdf資料は、こちらからアクセスできます。 https://drive.google.com/file/d/1hTC2avZPGWTz4I-uoeliENEBmrW8BEkN/view?usp=sharing 今回の「型の理論入門(4)」から、「論理的推論」のトピックを二回に分けて紹介します。 ここで取り上げるのは、ゲンツェンの Natural Deductionというシステムです。（正確にいうと、30年代半ばのゲンツェンの仕事を、60年代にプラヴィッツが整理したものの、かつ、その命題論理版です） 20世紀に入ってすぐ、ゲンツェンに先立って、ラッセルやヒルベルトが論理的推論の公理化に取り組んでいたのですが、それらのシステムは、必ずしもわかりやすいものではありませんでした。ゲンツェンのシステムは、それらと比して直観的で自然なものでした。このシステムを「自然な演繹」システムと呼んだのには、そうした背景があります。 今回のコンテンツには、「論理的推論」というテーマから少し離れているように感じられるかもしれませんが、重要な論点が含まれています。 それは、「判断」と「命題」の区別という論点です。そうした議論は、数理論理学というより哲学的議論に近いものですが、この議論を展開したのが、「型の理論」の最大の貢献者の一人である、マーティン・レフでした。90年代のことです。 ある命題がある命題を論理的に含意することの基礎に、ある判断からある判断が論理的に導出されるという構造があるという指摘です。 今回は、こうした立場で整理された「命題の構成ルール」を紹介します。ほとんど、自明に思われるかもしれません。しかし、こうしたステップが、論理的推論の前提だと思って見て貰えばいいと思います。 次回、論理的演繹のルールを紹介します。 今回の動画とスライドは、次のページからアクセス出来ます。 https://www.marulabo.net/docs/type-theory-talkie/ ページのリニューアル、少しずつですが進んでいます。

【「認識の理論」関連のポインター・ページを作りました 】 MaruLaboサイトの構造を見やすくするために、関聯したページのポインター・ページを作っています。 今日は、こちら。 https://www.marulabo.net/marulabo-philosophy/ ページを独立したコンテンツにする作業を続けているのですが、YouTubeのコンテンツの説明も、セミナー紹介になっていることに気づきました。YouTubeの方も、できるところから、セミナーから切り離した説明に変えようとしています。 あっちもこっちもで、もぐらたたきのようで、消耗して、肝心のポインター・ページはスケルトンのままです。また手を入れます。ごめんなさい。

【「量子通信入門 -- 量子ゲートで学ぶエンタングルメント」をリニューアルしました 】 2020年の8月のマルゼミの資料として、「量子通信入門 -- 量子テレポーテーションと entanglement swapping」の名前で公開されていたページを、「量子通信入門 -- 量子ゲートで学ぶエンタングルメント」として、かつ、単独のコンテンツとして利用できるようにリニューアルしました 。ご利用ください。 https://www.marulabo.net/docs/teleportation-2 / YouTube版の再生リストはこちらになります。 https://youtu.be/Jn_mKsz9pfk?list=PLQIrJ0f9gMcMbRmR1e02VskbnDz7_NNrS 次の9つのショートムービーから構成されています。 　● Bell State を生成するBell State Gate (1) 　● Bell State を生成するBell State Gate (2)　計算練習編 　● Bell State を計測するBell Measure Gate (1) 　● Bell State を計測するBell Measure Gate (2)　計算練習編 　● Bell State GateとBell Measure Gate 　● 量子回路上での量子状態の「交換」 　● Superdense Coding 　● Entanglement Swapping 　● 量子テレポーテーション 今月、「量子ゲートで学ぶエンタングルメント」というセミナーを開催しようと思っていたのですが、このテーマは以前のこのコンテンツで十分だと判断しました。今月開催予定だったセミナーは中止します。 何回でも再利用可能な内容なのですが、それぞれのビデオの冒頭に「8月のマルゼミの資料です」といったアナウンスが入っているのが、耳障りです。ご容赦ください。 何故、今、MaruLaboサイトのリニューアルに取り組んでいるかについては、前にものべましたが、サイトがが毎月のセミナーの資料置き場になっていて、全体の見通しも悪いし、各ページも独立したコンテンツのかたちになっていないことを改善したいというのが大きな理由です。 今回のビデオを再利用しようとして感じた「今月のセミナーの資料です」という、今

【「型の理論」入門 (3)  -- 型付きラムダ計算 を公開しました 】 https://youtu.be/0b2pHO6RuQQ?list=PLQIrJ0f9gMcPC8_eEnysTwZm14VRaQWCT スライドのpdf資料は、こちらからアクセスできます。 https://drive.google.com/file/d/1hdqE-UCP6hInkntEIgsuvJt0qbfNEwxw/view?usp=sharing 前回の「型のないラムダ計算」では、主に、ラムダ表記を使った「関数の抽象化(abstraction)」と、ラムダ式同士の、変数への代入を引き起こす、「適用(application)」についてみてきました。 今回は、いよいよ、ラムダ式が型を持つ「型付きラムダ計算」の紹介です。 基本的には、型σから型τへの関数は、型 σ → τ を持つと考えます。また、あるラムダ式 e が型 τ を持つことを、e : τ と表します。 この、矢印 → を含んだ型の表現は、関数型言語を知っている人には見慣れたものだと思います。ただ、気がついていない人もおられると思いますが、重要なことは、関数型言語でのこうした型表記は、すべて、チャーチの「型付きラムダ計算」が起源だということです。 以前に行ったセミナー「論理学入門 II — ラムダ計算と関数型言語」 https://www.marulabo.net/docs/logic2/ では、この型付きラムダ計算というアイデアが、現代の関数型言語 　・LISP 　・Haskell 　・OCaml 　・Coq に、どう受け継がれているかを、各言語ごとに詳しく見ています。こちらの資料も、あわせてご利用ください。 「論理学入門 I — 命題論理の演繹ルール」 https://www.marulabo.net/docs/logic1/ は、命題論理の演繹ルールを解説したものです。 「型の理論入門」も、次回の「型の理論入門(4)」から、「論理的推論」のトピックを取り上げます。次回以降は、この「論理学入門 I 」も参照ください。  動画とスライドは、次のページからアクセス出来ます。 https://www.marulabo.net/docs/type-theory-talkie/ ページのリニューアル、少しずつですが進んでいます。

【「量子論と量子コンピュータ関連ページ」を作成しました】 MaruLabo ウェブサイトの改善作業を続けています。 「量子論と量子コンピュータ関連ページ」を作成しました。 https://www.marulabo.net/marulabo-quantum/ ご利用ください。 次の4つのセクションから構成されています。 　● 量子論の基礎を学ぶ 　● 量子コンピュータ入門 　● 量子アルゴリズムを学ぶ 　● 量子情報 このポインター・ページが参照しているページのリニューアル・独立コンテンツ化は、これからです。 手始めに、ページ「量子コンピュータの現在 — 量子優越性のマイルストーンの達成 」を、独立のコンテンツ化してみました。ご利用ください。 https://www.marulabo.net/docs/q-supremacy/ ページ「ケット |k> で理解する量子の世界」も、少し手を入れました。 https://www.marulabo.net/docs/ket-talk/ ここでの「ケットのレシピ」が、僕は気に入っていたことを思い出しました。ご参照ください。

【  12月の丸山の活動について 】 現在、丸山は、MaruLaboページのリニューアルに取り組んでいます。 これまでのMaruLaboページは、毎月告知して開催してきたマルレク・マルゼミの内容に興味を持った人に向けられたものでした。ページは、「今月のマルレク・マルゼミ」というコンテキストの中で、その時々のセミナーの資料を公開する場でした。 ただ、こうしたコンテキストを離れて、以前のセミナー告知の際には興味がなかった人や、初めてMaruLaboサイトを訪問した人が、これまでのMaruLaboのページを見ると、背景説明もなく過去のセミナーのはだかの資料が置かれているだけの無愛想なページに見えたと思います。 MaruLaboページのリニューアルの目標のひとつは、それぞれのMaruLaboページを、セミナーとは独立した、それ自体完結したコンテンツとして、アクセスしたユーザー誰にとっても、読んでもらいやすいようにすることです。 もうひとつ改善したいことがあります。 MaruLaboのセミナーは、毎月様々な異なるテーマで開催されてきました。それ自体は、悪いことではないと思います。ただ、それらの資料ページでMaruLaboのサイトは構成されているのですが、サイトのトップページの印象は、あれもあればこれもあるといった、乱雑なものに見えていたと思います。 MaruLaboは、どのようなテーマに主要に関心を持っているのか、また、あるページと関連するページがどこにあるかは、すぐにはわかりません。内容が難しいページもあれば初心者を念頭に書かれたページもあります。 リニューアルの目標として、これまでのようにセミナーごとに資料を置くだけでなく、それらを横断する構造を示すことができればと考えています。 現在、「エントロピー」「エンタングルメント」「計算科学と計算複雑性」といったMaruLaboの主要な関心に関連するページのポインター・ページを作り始めています。（実は、「量子論と量子コンピュータ」というテーマの関連ページのまとめは、ページの数が一番多くて、まだ手がついていません。ごめんなさい。） MaruLaboのリニューアルには、さらにもうひとつ課題があります。 現在のMaruLaboのもっとも活発なユーザーは、YouTube経由でMaruLaboのコンテンツにアクセスする20代の若者です。た

 【 初めて量子論・量子コンピュータを学ぼうという人に 】 MaruLaboの量子論・量子コンピュータ関連の講座で、もっとも入り口の講座である、「たとえ話で理解する量子の世界 」ページを、全面的に更新しました。 https://www.marulabo.net/docs/quantum-talk-new/ 初めて量子論・量子コンピュータを学ぼうという人に知ってもらいたいことを、数学抜きでまとめたものです。  量子論については、「0 であると同時に 1 でもある不思議な状態」とか、「観測すると状態が変わる奇妙な観測」というように、その「不思議さ」「奇妙さ」を強調した、初心者向けの解説をときおり見かけるのですが、ここでは、そうしたことは私たちがよく知っている日常の中でもあることだということを「たとえ話」で説明しています。 量子論の「奇妙さ」「不思議さ」で足が止まった人もいらっしゃると思います。そうした経験がある人は、是非、お読みください。 確かに、量子の世界は不思議なもので、それを理解するのには「数学」の手助けが必要なのは事実です。ただ、「不思議」からいきなり「数学」にジャンプするのも、不親切な話です。そのスキマを、少しでも埋められたらと考えています。 その取り組みの一環で、次のページを作成しました。今回の「たとえ話で理解する量子の世界 」をお読みになった方は、このページへお進みください。 　「量子の状態をベクトルで表現する — 量子論の三つの原理」 https://www.marulabo.net/docs/q-youtube/#Lesson_0「量子の状態をベクトルで表現する_-_量子論の三つの原理」 このページは、先日作成した「YouTubeで学ぶ量子論の基礎」の先頭に追加したものです。 https://www.marulabo.net/docs/q-youtube/ こちらもご利用ください。 現在、MaruLaboのページの見直しを進めています。まだ、量子論関連のページのリニューアルとまとめページの作成はできていないのですが、年末頑張ろうと思っています。お待ちください。

ペンローズの「皇帝の新しい心」（1989年）の冒頭には、お母さんがコンピュータ科学者、お父さんがコンピュータを破壊しようという、今でいう「テロリスト」を両親に持つ子供が登場する。これって「銀河鉄道999」のメーテルの家庭環境と同じだ。 舞台は、国をあげて開発した、その国の全ての人間のニューロンの数より多い10の17乗個の論理ユニットを持ち、その知能は想像もつかないほど高いと言われている、巨大コンピュータUltronicの火入れとお披露目の場。 その子は、お母さんが有力な開発者だったので、お母さんと一緒にセレモニーの前から三列目にいる。（お父さんは、爆発物が見つかって拘束されている）。司会者が、「誰か、Ultronicに、最初の質問をしてみませんか？」と会場に声をかける。みな、自分の無知を晒されるのがいやと思ったのか、誰も手を上げない。 その子は、Ultronicの開発と一緒に育ったようなものだったので、「彼」が何を感じているのか自分のことのようにわかるように思っているので、臆せず手を挙げる。司会者が彼を指名する。 その時、何かが起きる。 約400ページほど省略すると、あれ、これってネタバレ？　でもネタバレしないと話が進まないな。まあ、いい。会場で起きたことについては、次のポストで書く。 それは、コンピュータによる「意味」の理解に関連した、とても面白い寓話だ。 （ちなみに、ペンローズの次の本「心の影」の冒頭にも寓話が掲げられているのだが、それは、プラトンの「洞窟の喩え」を寓話にしたものだ。彼は、数理哲学的には、プラトン流の「実在論者」なのだ。） ペンローズのこの本は、30年前のものだけど、人工知能論としては、頭三つぐらい飛び抜けている。サールらの「強いAI」論の批判などは、痛快なものだ。 僕は、人工知能論では、「計算主義」の立場に立つのだが、この本は、全力で「計算主義」を批判している。ペンローズの「計算主義」批判は、避けて通れない問題だ。 ある意味皮肉な話だが、個人的には、この本が出た頃、哲学では飯が食えなくて、僕は哲学からITの世界に転進する。この本が扱っている問題は、当時の僕の哲学的関心には、とても身近な話題だったのだが、ITの問題としては僕は真面目に考えてはいなかったと思う。それは、僕の視野の狭さのせいだと思う。 ITの世界に30年いて、最近は、人工知能がある意

【 9/4 マルレク「量子情報とエントロピー」講演ビデオ公開 】 9月4日に開催したマルレク「量子情報とエントロピー」の講演ビデオ公開しました。 解説資料、講演資料、講演ビデオは、次のページからアクセスできます。ご利用ください。 https://www.marulabo.net/docs/info-entropy3/ 【 なぜ、「エントロピー」が重要なのか 】 20世紀は、科学・技術が飛躍的に発展した時代でした。特筆すべきは、20世紀前半の量子論・相対論の成立を画期とした科学的自然認識の拡大と、20世紀後半のコンピュータ・通信技術の成立・発展による、技術的情報世界の拡大です。 自然科学が対象とする「物質の世界」と、IT技術が対象にする「情報の世界」は、異なる世界のように見えます。ただ、21世紀の科学・技術は、この二つの世界の交差するところで発展するだろうと、丸山は考えています。物質の世界と情報の世界という二つの世界を結びつける、重要な概念が「エントロピー」です 【 なぜ、「量子情報」なのか 】 今回のセミナーで伝えたかったことの一つは、「量子の世界」に飛び込んだ時、「物質の世界」と「情報の世界」のつながりが、より一層明確に見え始めるということです。 こうした現象は、20世紀後半から21世紀初頭にかけて、科学・技術の非常に広い分野で確認できることです。 このセミナーの第一部では、20世紀の後半に明らかになった情報の世界は物質の世界とが密接に繋がっていることを示す次のようなエピソード達を紹介しようと思います。 　・エントロピーの再発見 　　　1950年代 -- シャノンの情報理論   　・なぜ、コンピュータは電力を消費し、熱くなるのか 　　　1960年代 -- ランダウアーの原理   　・エントロピー概念の三つ目の起源 　　　1970年代 -- エントロピーとコルモゴロフ複雑性との接点 　・情報過程は物質過程である 　　　1980年代 -- Church-Turing-Deutsch Principle 【 講演ビデオの構成 】 講演ビデオは、次の4つの動画から構成されています。 　● Part 0 「物質の世界」と「情報の世界」 https://youtu.be/xNxVeNTd_Qs?list=PLQIrJ0f9gMcOujPfbCOKdbM1t

<< 4年前のFacebookへの投稿です >> ２ヶ月前に亡くなった数学者のヴォヴォドスキーが、「最後に」、どんなことに興味を持っていたのか調べ始める。 いったん、「晩年のヴォヴォドスキー」と書きかけたのだが、事故やその他の理由で突然死した人に（彼は動脈瘤が破裂して51歳でなくなるのだが）「晩年」というのは、あまり馴染まないなと気になって「最後に」に書き換えた。 ただ、「最後に」は、短い時間しか指し示さない。最後の論文は、最後の一つの論文だ。それに対して、「晩年」には、時間的な幅がある。いくつかの論文を対象にできる。「晩年」でもいいのかな？　 「晩年」には、年齢制限もあるのかも。若くして亡くなった尾崎豊やエイミー・ワインハウスには、「晩年」は、似合わない。（突然死だから？） でも、子規は30代で亡くなっているのに、「晩年」といってもおかしくない気がするのはなぜだろう？（ずっと、病床にあったから？） どうでもいいことで本題から外れたが、ヴォヴォドスキーが最後に取り組んでいたのは、"C-System"という対象のように見える。 "C-System"の'C'は、Contextual Categoryの'C'で、Contextのことだと思っていい。わかりやすい説明は、ここにある。 https://ncatlab.org/nlab/show/context 平たく言えば（そう解釈できるという意味でしかないのだが）、コンテキストの意味論の形式化をやっているのだ。 僕は、現在の人工知能技術が、言語の意味理解と数学的推論能力という二つの点で人間の壁を乗り越えられていないと感じているのだが、それは、「シンボル」レベルの抽象を持たない、べったりした「コネクショニズム」還元論というディープラーニングの方法論自体の限界だと考えている。 グロタンディック＝ローヴェール＝ヴォヴォドスキーという、現代数学の、いわば、極めて抽象的なレベルでの探求が、こうした人工知能技術の具体的な課題と結びつくかもしれないと考えるのは、とても楽しいことだ。 少し、「意味の意味」、あるいは、その数学的把握である「意味の形式的理論」と言われるものを、紹介したいと思う。 ---------------------------

【「型の理論入門」ページのリニューアルを行っています 】 現在、MaruLabo のページのリニューアルを行っています。 その一環として、以前公開した動画には音声が入っていないサイレントなものがあるのですが、そうした動画に音声での解説を入れ始めました。 今回、最初に選んだのは「型の理論入門」のページです。 「型があるウログラム言語」と「型のないプログラム言語」があることを、多くのプログラマーは知っていると思います。また、その「どちらがいいか」という「論争」があることも知っていると思います。自分が、日常的にどの言語を使うかは、自分で決めればいいことだと思います。 ただ、「計算」と「プログラム」の本質的な特徴を知るには、「型の理論」が不可欠だと丸山は考えています。 今回公開したのは、チャーチの「型のないラムダ計算」の前半部分です。 https://youtu.be/s-HrEz8a4B4?list=PLQIrJ0f9gMcPC8_eEnysTwZm14VRaQWCT 今回の話は、けっして難しいものではありません。 これを入口として、多くのプログラマーが「型の理論」を知ることを期待しています。 まとめページは、「型の理論入門 (トーキー版)」 https://www.marulabo.net/docs/type-theory-talkie/ です。まだ、トーキー版完成していません。 少しお待ちください。