「チャット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>…
ラムダ計算の意味論においては、カリー同型が中心的な概念です。となると、依存ラムダ計算の意味論には依存カリー同型が必要になります。とりあえずは一番具体的なデカルト閉圏である集合圏において依存カリー同型を考えてみます。$`\newcommand{\id}{\mathr…
状態モナド変換子〈state monad transformer〉は、「状態モナド・変換子」ではなくて「状態・モナド変換子」です。モナド変換子の目的はモナドの変換ですが、定義上はモナドじゃなくても関手を変換できるので、「状態をひっ付ける変換子〈state attachment t…
TypeScriptで、アロー（二重矢印「=>」〉で関数や型を書けるのはとても便利です。Lean 4では、アロー（一重矢印「→」）により依存関数空間型〈パイ型〉も記述できます。さらに便利です。内容： TypeScriptのアロー関数 Lean 4の場合 パイ型〈依存関数空間型…
プログラミング言語や証明支援系において、既存の型を組み合わせるのではなくて、まったく新しい型（値の集合）を定義する場合は、帰納的型〈inductive type〉として定義することになります。帰納的型の上の関数は、帰納的に定義できます。このことを帰納原…
「外部バージョンの依存カリー同型」にて： 外部バージョンの依存カリー同型は、極限の定義をなぞっているだけなので、内部化しないと面白くはありません。面白くすることは、今考え中です。 集合圏とは限らない圏 $`\mathcal{C}`$ に対して依存カリー同型を…
「カリー／ハワード／ランベック対応の辞書： 推論規則再論」で次のように書いています。 $`A, B, X, Y`$ などは圏 $`\mathcal{C}`$ の対象を表します。$`I, J`$ なども $`\mathcal{C}`$ の対象ですが、これらを“集合とみなす方法”〈dereification〉があると…
「カリー／ハワード／ランベック対応の辞書」を皮切りにカリー／ハワード／ランベック対応に関して幾つかの記事を書きました。 カリー／ハワード／ランベック対応の辞書（最初の記事） 続・カリー／ハワード／ランベック対応の辞書 論理と圏論： 導入規則と…
こんな感じです。 円： $`\text{for }x, y\in {\bf R}\\ x^2 + y^2 = r^2`$ 内容： ステップ 1： SVG要素を置くだけ ステップ 2： 数式が表示されることを確認 ステップ 3： SVG foreignObject内にXHTMLフラグメントを書く ステップ 4： さらにラップして段…
JSON形式で表現されるデータがあったとして、データの型付け〈typing〉をTypeScriptで記述するとしましょう。インターフェイスやクラスを使わずに、次のように型定義するとお手軽です。 type A = { "type" : "a", // A specific } type B = { "type" : "b", …
続・カリー／ハワード／ランベック対応の辞書 矢印の混乱に対処する： デカルト閉圏のための記法 上記2つの記事で述べた内容を組み合わせて、記述を追加します。論理でいう「推論規則」は種類が違うものをゴッチャにしています。導入規則〈introduction rule…
「矢印の混乱に対処する： デカルト閉圏のための記法」より： 一番ポピュラーな矢印記号である「$`\to`$」は、圏の射のプロファイル（域と余域の仕様）の区切り記号に独占的に使わせていただきます。 これはもちろん、僕の私的提案、つうか願望であって、矢…
2023-02-09の僕のツイート： 矢印「→」が異なる意味でオーバーロードされているのは相当に深刻な問題だなー。 これで混乱したり挫折する人がいるから、弊害とても大きい。 十数年前からカリー／ハワード対応のセミナーとかやっているわけです。複数の分野に…
関数のファミリー〈族〉からタプル関数を作る操作とコタプル関数を作る操作は双対〈dual〉で、圏論の極限と余極限の双対性に対応します。しかし、型理論やプログラミング言語のなかでは、この双対性が見えにくくなっています。タプル構成は、λΠ計算〈ラムダ…
将来書かれるかも知れない（書かれないかも知れない）記事から参照される具体例を先に書いておきます。内容としては、関数達のタプル構成とコタプル構成です。タプル構成とコタプル構成がひとつの設定内で出てくる例題になっています。タプル構成とは、キー…
カリー／ハワード／ランベック対応の辞書 続・カリー／ハワード／ランベック対応の辞書 まだあるの？ まだあります！カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、「型理論（ラムダ計算を含む）」「論理」「圏論」の三分野の…
