最近とあるITスタートアップ企業でインターンをしている。
論理学&理論計算機科学を研究するものとしてプログラミングやコンピュータ関係のことは独学していたが、いかんせん理論偏重になってしまいがちだった。ようやく現場で実践する機会に恵まれている。
といってコーディングはしていないのだが、しかしドキュメントを編集してGit/GitHubを使う機会がけっこうある。Git/GitHubもいずれ役に立つかもと思って少し本を読んで触ったことがあったのが助けになった。
自作の大きなプログラムを書いたことはないので、実際のソフトウェア開発に携わって初めてGit/GitHubの偉大さがわかった。ブランチとマージの概念を考えた人は偉い。
具体的なコマンドは都度Geminiに訊ねた。Geminiは正確な答えを返してくれた。ありがとうGemini。本だとサンプルプロジェクトを操作することが多いが、それに沿って流れで覚えるより、実際に必要になったコマンドを逐一Geminiに訊くほうが身に付くなあと感じた。
またいろいろ本を読んだので紹介します。
読書会で読んだ。
ヒース先生は『反逆の神話』と『資本主義が嫌いな人のための経済学』を前に読んだが、本書はもっと専門的な本。たいへん難しい。今まで経済学とかゲーム理論とか進化論とか言語哲学とか倫理学とか細々と勉強してきたけど、本書ではそうした学問の知識が総動員されている。
序盤はゲーム理論を批判し、その背景にある帰結主義とか道具主義を批判する。人間は帰結を良くするために行動するのではなく、ルールに従う生き物なのである。
中盤では、進化論や現代プラグマティズムを援用して、ルールを作ってそれに従うということが人間の認知にとっていかに重要かを論じている。
最終的には規範倫理学全般をディスって終わる。最後の「規範倫理学」という章には感銘を受けた。道徳には「最大多数の最大幸福」とかそういう究極原理などない、エチケットなどと変わらない、と論じている。あくまで実践が大事。倫理学の入門書でも、実践の感覚に合うように理論を説明しているでしょ、と。道徳哲学者のすることは、人々が規範を明示的に語りやすくすることなのである。
経済学や進化論や心理学の研究が多数引かれているが、それ以上にプラグマティズムの応用という面が印象に残った。実践を重視するプラグマティズムは、分析哲学にない良さがあると思う。
最近、Rustというプログラミング言語を勉強したり、メモリ操作を形式的に扱うプログラミング論理を調べたりしていて、そのためにC言語を思い出す必要が出た（ふつうC言語をよく知っている人がRustをやったりプログラム論理をやったりするので順番が逆だが）。
で、前橋和弥『C言語 ポインタ完全制覇』という本を読みはじめたのだが、途中でC言語の初歩を忘れてるなとなったので、昔ある程度読んでいたこの本を再読。
理屈から丁寧に説明されていて良い本でごんす。
著者が提供している学習環境は、古いせいか上手く使えなかったので注意。gccというのでコンパイルしました。
詰将棋の問題集や作品集はたくさん出ているが、本書はそうでない。詰将棋とは何か、どういうルールか、ということから始め、問題の分類や有名な手筋の解説をする本である。私みたいに詰将棋のマニアックな世界に入門したい人には最適な入門書。
詰将棋のルールは明文化されているわけではないが、できる限り論理的に体系化して書いている。著者が数学者だからか、数学の公理を思わせる。
節ごとに実際の詰将棋の問題が載っているのだが、どれも単手数なのにクソ難しい。解けなくて解説を見た問題が多い。解説にその問題のなにがどう凄いのか書いてあるが、そのパズル的な部分に悩むに至る前に諦めてしまった問題も多い。問題の多くは詰将棋専門誌『詰将棋パラダイス』が出典である。詰将棋マニアの世界、恐るべしと思ったが、しかしおかげで私の詰将棋力はだいぶ向上したと思う。
本の後半では、フェアリーというのも解説されている。フェアリーとは変則的なルールの詰将棋の総称である。フェアリーって私は一部のマニアしかやっていないと思っていたが、どうも最近では詰将棋界隈では広く人気らしい。詰将棋もだんだんネタが尽きてくるので、変則ルールも開拓したくなるのだろう。フェアリーのうち「レトロ」というジャンルはチェスの世界では論理学者のレイモンド・スマリヤンが有名な本を書いているとか。私はスマリヤンみたいなパズル作りの才能に憧れる。本当に頭がいい人って感じがする。本書の著者も数学者だし、詰将棋やフェアリーに強くなれば私も論理学者として箔がつくかも。
ジェイムズ・ジョイス『フィネガンズ・ウェイク』の訳者でお馴染み柳瀬尚紀の本。『フィネガンズ・ウェイク』を訳す過程で発表されたエッセイや対談が収められている。
柳瀬訳は訳注をいっさい載せていない。なのだけれど、訳語の選択の意図はいろいろあって、どういうジョイス語にどういう日本語を対応させたのか、隅々まで考えられている。本書は、そういう翻訳意図の一端が垣間見える。全体にはナンセンスな文章が多くてやはりわかりづらいが。
最近OCamlという言語でプログラミングの勉強をしている。↓の素晴らしい本を読んでいる。
日本はOCamlほかML系言語の研究者がけっこういて、本やネット上の解説が充実している。助かる。MLというのはMeta Languageの略で、大計算機科学者のロビン・ミルナーの研究に端を発する言語である。OCamlもこの流れに位置する。
MLは多相型システムというのを持っている。これはジラール先生が開発したシステムFという論理体系とカリー=ハワード的な対応を持っている、とごく大雑把には言える。なのでジラール主義者たるわたし的には興味深い。
OCamlはフランスの研究所発祥なのでジラール主義者の私にはさらに興味深い。OCamlはObjective Camlの略で、Camlという言語にオブジェクト指向を搭載したものという意味を持つ。Camlの部分はCategorical Abstract Machine Languageに由来するとか（なのでCamlの"ml"の部分はMeta Languageではないらしい）。Categorical Abstract Machineはフランスの論理学者・計算機科学者たちが提唱した圏論を使った計算モデルである。
これを言語として実装したのがCamlらしい。↓の本やWikipedia情報。
Categorical Abstract Machineにはラフォンという人が開発した線形バージョンもある。ラフォン先生はジラール先生の高弟である。このLinear Abstract Machineについては↓の本に解説がある（まだちゃんと読んでない）。
こうしたフランスの研究の流れのなかでCoqも生まれている。Coqの処理系はOCamlで書かれていてOCamlと関係が深いらしい。
フランスの論理学・計算機科学現代史はなかなかおもしろく、もっとちゃんと調べたいところ。フランス語の勉強も頑張ります。
最近読んだ本を紹介するぜ！
人生の意味の哲学の入門書。
私はデイヴィッド・ベネター先生のファンなので、ベネター先生が登場する3章と6章がおもしろかった。
そもそも人生の意味を(分析)哲学的に論じることなんて可能なのか？ と迫るような論考も多かった。それじゃあダメじゃんとも思うが、そうだとしたらそれがわかっただけでも大いなる前進かもしれない。
本書を読んでも人生の意味がわかるようになるわけではない、と何度か書かれているのだけど、人生の意味の哲学を研究しても人生の意味がわかるようにはならないのか？ というのも人生の意味の哲学的な難問のような気がする。
たいへん勉強になる本です。
HTML、CSS、Bootstrap、JavaScript、Node.js、SQL、なんかを統一的に扱ってちょっとしたものを作っていく本。
掌田先生の本はどれもわかりやすく、また別の本も読み始めている。
本書の最後の章の最後の方はなんか書いたものが動かなくなってしまって挫折したのだが、まあまあまあ、大部分はちゃんと動きました。
これタイトルは「意味がわかる「AI入門」」と「「意味がわかるAI」入門」と二重の意味になっているのだろうか。意味について研究する哲学者が、AIは言語の意味を理解しているのかという観点からAIの歴史と仕組みを解説した本。
殆どがAIの入門書として読めるのだが、最後の方で「現在の大規模言語モデルによるAIは意味を理解しているとは言えない」という哲学者ならではの批判が提示されて終る。非常におもしろい本でした。
最新の研究が取り上げられているが、これもすぐ古くなりそうだ、と書かれていた。ホンマに怖いですな。
今後も参照していく本になりそうです。
アニメーターが書いた絵の教本。世の中イラストの教本やガチのデッサンの教本は多いが、アニメーターの視点で人体の描き方を解説した本はなかなかないので良いです。
といっても絵の描き方というより、どうすれば気楽に絵がたくさん描けるかという精神を解説した本という感じで、私みたいな絵を描くとなると躊躇しちゃう人間には啓蒙的な本でした。
とある論文を読んでいて余帰納法の知識が必要になったので調べた。その論文ではJacobs & Rutten "A tutorial on (co)algebras and (co)induction"で入門するとよいとあったのだが、同論文のような圏と関手を使った議論はそんなに必要そうではなかった。
で、いろいろ検索した結果、TaPLことBenjamin C. Pierce『型システム入門』にちょっと載ってる議論が役に立った。
同書の監訳者の住井英二郎先生はブログでもいろいろ書いておられる。
また住井先生が著者の一人である『プログラム意味論の基礎』(小林直樹共著・サイエンス社)でも簡単に触れられている。
圏と関手を使った議論もちょっと調べた。Jacobs & Ruttenの論文の改訂版が"Introduction to (co)algebra and (co)induction"というタイトルで↓の本に入っている。これを見た。
その辺を読んで学んだ事を纏めておく。
集合 の冪集合
を考える。
は包含関係
で順序集合となる。この順序についての単調関数
を用意する。で、
で
となるものを考える。このような
のうち包含関係について最大のものが、余帰納的に定義される集合なのである。しかもこの最大のもの
は以下のように具体的に得られる。
この はさらに、
を満す最大の
、すなわち
の最大不動点となっている。
帰納的定義ではBNFが使われるが、余帰納的定義でも使える。
というBNFで余帰納的に定義される集合というのは、
によって定義される単調関数 によって余帰納的に定義される集合の事である。例えば、
というBNFで余帰納的に定義される集合は、
という単調関数で余帰納的に定義される集合で、これは実のところ長さ 以上の
の有限列・無限列すべての集合となる。
余帰納法による証明は、 が単調関数
から余帰納的に定義されているとき、
を示すことで
を示すものである。例は『プログラム意味論の基礎』28ページを見てね。
以上のような議論は圏と関手を使ってもっと一般化できる。圏 とその自己関手
があったとき、
の対象
と射
の組
を
-余代数という（"Introduction to (co)algebra and (co)induction"ではすべて
で議論しているが、圏一般に拡張してもよいらしい）。
-余代数を対象とした圏を作れる。射は次のように作る。
を
-余代数とする。もとの圏
において射
があり、
を満すとき（可換図式を描くとわかりやすいのだけど省略）、この
を射とするのである。
こうして得られた -余代数の圏の終対象を
-終余代数と呼ぶ。これが余帰納的定義になっている。
は包含関係
で順序集合となるが、この
を射とみなすとこれは圏になる。すると単調関数
は自己関手である。なので
となるとき
は
-余代数となる。
も
-余代数のとき、
となれば、またそのときのみ
-余代数の圏で
と
の間には射がある（示すのは簡単）。ということは
-終余代数は
となる
のうち包含関係について最大のもの（から得られた余代数）であると言える。
余帰納法について考えているうち「余帰納京子」というフレーズを閃いた。『ゆるゆり』の登場人物「歳納京子(としのうきょうこ)」とのダジャレである。歳納京子のことを常にフルネームで呼ぶキャラがいるので歳納京子のフルネームは頭に残りやすい。
驚くべきことにトゥイッターで「余帰納京子」で検索したら何件かヒットする。私みたいな阿呆が何人もいる。
※この記事はエイプリルフールのビッグウェーブに乗り遅れないように焦って書いたので、内容が凄くテキトーです。のちのちちゃんと勉強して推敲してアップデートします。
「私は嘘つきです」というやつです。論理学っぽく書くと「この文は偽である」。
(1)「この文は偽である」は真であると仮定すると、この文は偽であることになる。ここでいうこの文というのは当の「この文は偽である」という文のことである。すると「この文は偽である」は真であり、かつ「この文は偽である」は偽であることになって矛盾。
(2)「この文は偽である」は偽であると仮定すると、この文は真であることとなる。ここでいうこの文というのは当の「この文は偽である」という文のことである。すると「この文は偽である」は偽であり、かつ「この文は偽である」は真であることになって矛盾。
というように「この文は偽である」という文は真だとしても偽だとしても矛盾を導く。
この議論に問題があるとしたら何か。
まず「すべての文は、真か偽である」という隠れた前提がある。これは当然のようだけれど非古典論理はこういうのを拒否する。真でも偽でもない文を許す論理体系を作ることもできる。
また「この文」について言及するような文を許してよいのか、という反論もできる。自己言及を禁止するわけだ。そもそも自己とは限らずなんらかの文について言及する文というのは、自然言語というか日常会話ではよく出てくるが、形式論理でどう作ればよいかというのは自明ではない。
もっとすごい反論もある。そもそも矛盾してもいいじゃないか、ということである。
これらは論理体系に制限を加えたり真理の定義を与えたりして数理論理学的に解決されるのだが、その背景には「そもそも真理とは？」という永く問われてきた深遠な問いがある。哲学と数理論理学の両面からこれを探究する分野はいまでもそれなりに盛んなようで、これを真理理論という。
というようなことをいちおう書いておきました。
嘘つきのパラドクスについて勉強してエイプリルフールに合わせて記事を投稿すればアクセス数が稼げるかな〜と思ったけど、他のことをやっていたらぜんぜん進みませんでした。
いちおう以下の動画を見ました。（動画を見て学んだことのメモは何度も見返して徐々に充実させていきたい。）
京都大学が毎年やっている講義で、昨年からはYouTubeで公開されている。矢田部先生の今年のテーマが嘘つきのパラドクスだった。その1動画ではパラドクス解決のための4つの方針とそのメリット・デメリットが述べられている。
⚫︎古典論理を保持する
・階層的理論：タルスキらの方針。嘘つき文を禁止する。自然言語からかけ離れたものになる。
・ギャップ主義：クリプキらの方針。嘘つき文は真偽が決まらないとする。アドホックな感じ。
⚫︎古典論理を捨てる
・グラット主義：プリーストらの方針。嘘つき文は同時に真でも偽でもある。真矛盾主義という哲学的立場が背景にある。矛盾許容論理というのもあるのでわりといける。そんなのありかよ、という感じは否めない。
・多値論理：多値論理はもともとウカシェヴィッチ。真偽以外に中間的な真理値を導入。ファジイ論理みたいに連続的な真理値を持つのもある。これも、そんなのありかよ感がある。
個人的に印象に残ったことを書き残す。
つづいてその2。
これはたいへん勉強になった。タルスキのテクニカルな議論をちゃんと踏まえてデイヴィッドソンの真理理論を見るとその方針と問題点がよくわかる。
タルスキの真理定義であるT-図式と真理述語と階層的意味論の解説がある。それだけにとどまらず「そもそもどういうものが真理定義とみなしうるのか」という哲学面の解説も詳しい。意味論的解決と公理論的解決があって、タルスキによる階層を使った意味論的解決が取り上げられている。これはモデルによって相対的なので実は万能ではない。
徒然なるままに
その3。
その2から連続で見ていて、これを見ているときは疲れてきていたのであんまり理解できていません。
とりあえず徒然なるままに。
その4。
これはかなりおもしろかった。あまり形式的な話は出てこない回なので。ヤブローのパラドクスは本当に見事な議論である。
余帰納法と(強)双模倣性はミルナーらのプロセス代数において重要で、しかし計算機科学でなく哲学的な(邪な)関心から興味を持った私にはよくわからなかったのだけど、少しわかった。強双模倣性は余帰納的に構成されたものの同一性をあらわすのによいとか。また余帰納法がω矛盾を持ち込みがちというのは雰囲気だけはわかったかも。
徒然
また、『数学における証明と真理：様相論理と数学基礎論*1』という本のなかに黒川英徳先生の「真理と様相」というパートがあって、ここで嘘つきのパラドクスと真理理論のことが解説されている。けどちょっとしか読めなかった。これからです。矢田部先生の講義ではちょっとしか触れられていなかった様相論理を使ったアプローチが紹介されている。本書は様相論理をテーマにした数学基礎論サマースクールの講義録なので。
この本の最初の「様相論理入門」というパートは佐野勝彦先生が書いている。佐野先生は様相論理と余帰納法と双模倣の関係の研究をされていて、ここにも双模倣の話が出てくる。可能世界意味論はオートマトンみたいなものなので。ただし黒川先生のほうに出てくる様相論理と双模倣にどういう関係があるのかはわからない。
必然性オペレータ□は、真理の無限性みたいなものを持ち込むものだとかいうことをジラール先生が書いていた。その一端がちょっと見えたような見えないような。
ロジックを勉強していたら誰もが(?)出くわす束縛変数の名前の付け替えのやつをまとめたいのよ。
以下のことを書いていて気づいたのだが、"Basic Proof Theory*1"（以下：BPT）には式 expressions や論理式 formulas の定義がない。subformulas の定義はあるので論理式の定義は暗になされているのだろうが、式はどうだろう。論理式を式に含めてよいのかどうか今のところハッキリとはわからない。もうちょっとちゃんと読み進めないと。しかしどうも含めていそうなので、以下では式の例として論理式を使っています。論理式や項 term の総称が式じゃないかなと。
BPSの3ページにこんなお約束が出てくる。
式
と
が束縛変数の名前のみで異なるならば、これらを同一視する。
例えば と
は同じということである。ではここで言っている同じとはどういう同じなのか。
と
は見るからに同じであるが、この同じを literal identity といって
と書きましょうというのがBPTのいちばん最初に出てくるお約束のうちのひとつである（2ページ）。
と
の同じはα同値(α-equivalence)という。literal identity よりもおおらかな同じである*2が、議論をしやすくするためにここまでを同じとしようということである。ある式の束縛変数の名前を付け替えて別の式を作る操作は二項関係とみなせるし同値関係である。α同値を同じとみなすというのことは、我々はα同値による式の同値類およびそれらの集合である商集合に着目するというわけだ。上の例の同値類は
となる。ただしアルゴリズムの実行とかそういう立場で考えると名前の付け替えを無視できない、という注意も書かれている。
この同じを認めると代入の議論がしやすくなる。代入というのは基本的には
式
に式
なのだが、条件として
もしくは
代入の定義に束縛変数の名前の付け替え操作も加える。
というのが必要となる（このあたりはBPSからの正確な引用ではないです。こちらでかなりイジってます）。式の意味(?)が変ってきてしまうからである。前者の条件が満たされれば後者は必要ないし後者が満たされれば前者は必要ない。しかしBPSの定義では束縛変数の名前の付け替えをしても式は変わらないので、前者の条件を満たすように適当に名前を付け替えればよいわけである。なので一般性を失わず*4代入はいつでも可能。
例。 の
に
を代入する。しかしこのまま
を
で置き換えてしまうと
となり
の
が束縛されてしまって話が違う*5。なので予め束縛変数の名前を付け替えて
とする。こうしても同じである。これに代入を実行すると
となって事なきを得る。
また、この他の効能として、量化子のすぐ後の変数を量化子の出現ごとに変えられたりとか*6、束縛変数の集合と自由変数の集合を互いに素にできるというのも挙げられている（4ページ）。これらはメタ定理の証明やそれを使った証明の分析をする際に便利であると思われる。前者の例はたとえば と
は同じということ。後者の例としては、
という論理式の束縛変数を見ても自由変数を見てもどちらにも
が入っていてややこしいがこれと同じである
にすれば束縛変数と自由変数に被りはない、というのが挙げられる。
*1
