過去・現在・未来

【「型の理論」入門 (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のページの見直しを進めています。まだ、量子論関連のページのリニューアルとまとめページの作成はできていないのですが、年末頑張ろうと思っています。お待ちください。