「チャットAIで形式証明も自然言語混じりで書ける（はず）」と「自然言語証明から形式証明を抽出できる（はず）」で述べたように、自然言語を使って形式証明が書けるようになるだろうと予測（むしろ期待）してます。しかし、自然言語であろうが形式言語であ…

コンテナ＝1-コンテナ という概念の次元を1つ上げて2-コンテナを定義します。取り急ぎ。$`\newcommand{\s}[1]{\mathrm{s}{#1} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\In}{\text{ in }} \newcommand{\hyp}{…

記号の乱用〈記法の{乱用 | 濫用} | abuse of notation〉は、ものごとを分かりにくくして誤解と混乱のもとになります。しかし、非常に広く使われていて、使わないで済ますことが困難です。人間にとってだけではなく、プログラミング言語や証明支援系などのソ…

不満があっても、「言ってもどうせ何も変わりはしない」という諦めがあればあえて不満を口に出すことはないでしょう。願望があっても、「どうせ叶わぬ夢だし、言ったところで虚しくなるだけ」と断念しているなら語ることはないでしょう。僕は今から不満と願…

「チャットAIで形式証明も自然言語混じりで書ける（はず）」と「自然言語証明から形式証明を抽出できる（はず）」において、形式証明と自然言語証明はかなりの程度相互翻訳可能になるはず、という予測（というか期待・願い）を述べたのですが、自然言語ヒン…

「チャットAIで形式証明も自然言語混じりで書ける（はず）」において、形式証明のなかに自然言語によるヒント／キューが書けたら証明記述作業が格段に楽になる、と書きました。この方法を少し推し進めれば、書籍や論文の自然言語証明から形式証明を生成でき…

ChatGPT-xのような、チャット方式の対話型AIが世間を騒がしています。確かに、現代社会に大きなインパクトを与えそうです。僕も期待に胸を躍らせているのですが、だいぶニッチな方面への期待です。今までとても困難だった“機械可読形式証明〈machine-readabl…

帰納的に定義された型〈inductively defined type | inductive type〉では帰納原理〈induction principle〉が働きます。帰納原理を関数として表現したものがリカーサー〈recursor〉です。リカーサーについては「帰納的型とリカーサー」で述べました。以前の…

昨日の記事「ヤシコフスキ／カリシュ／モンタギュー形式の証明： 人間可読・将来的機械可読」に挙げたヤシコフスキ／カリシュ／モンタギュー流証明の例題をもう一度載せます。$`\newcommand{\mrm}[1]{\mathrm{#1}} \require{color} \newcommand{\Keyword}[1]…

世間では、自然言語で会話できるチャットAI／大規模言語モデルの話題が盛り上がってますが、僕にとっての当面の期待は、人間可読でありながら機械可読でもある形式的証明記述の可能性です。長年のストレスであった次のジレンマが解決するかも知れません。 機…

前回の記事「近未来の証明ソフトウェアは‥‥」で、次のように書きました。 もう楽観的な気分にはなりにくいのですが、自然言語で対話できるAIが評判になっているご時世だし、「2年後にはグランディ／センタのサンプルをそのまま理解する証明ソフトウェアが実…

twitterで昔の論文に言及したのですが、出版年をえらく間違えてました → https://twitter.com/m_hiyama/status/1635154485101359104 「53年前」と言ってますが、実際は27年前でした。 Title: A Browsable Format for Proof Presentation Date: June 1996 Aut…

カリー／ハワード／ランベック対応の話を何度かしました。「カリー／ハワード／ランベック対応の辞書」の最後に、最近のカリー／ハワード／ランベック対応関連の記事をまとめてあります。最近に限らないなら： ブログ内検索： 「ハワード」の検索結果 さて、…

型付きラムダ計算の意味論はデカルト閉圏で展開できます。したがって、型付きラムダ計算はデカルト閉圏に対する計算系だとみなしてかまいません。しかしながら、関数型プログラミング言語やその処理系は、デカルト閉圏を直接的に扱っているわけではありませ…

TypeScript 4.9.5 での話です。例えば次のようなコードを試してみます。 type Foo<X> = X extends (0 | 1) ? number : string; var x: Foo<null> = 1; // NG var y: Foo<null> = ""; // OK これは、null extends (0 |1)ではないことを意味します。型を集合と解釈して*1 $`\{</null></null></x>…