このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

線形論理 の検索結果:

人名の発音: Girard, Guiraud, Giraud

…で話題にしたのは、 線形論理の創始者である Jean-Yves Girard 高次元の証明論をやっている Yves Guiraud 同一人物かと思ったが別人で、名前の読み(カタカナ表記)は「ジラー」「ギロー」がよいかな、と。そんなことでした。実はもうひとり似た名前の人がいて、 グロタンディークの弟子の Jean Giraud 線形論理の創始者とは別人です。姓の綴りもちょっと違います。最近は、人名の発音が調べやすくなりました。調べてカタカナ表記してみます。Girard ジラード…

フィードバック付きモノイド圏とその周辺

…afl08.pdf 線形論理と証明ネットに興味があるなら: Title: Proof nets for unit-free multiplicative-additive linear logic Authors: Dominic J. D. Hughes and Rob J. van Glabbeek Year: 2005 Pages: 72p URL: http://boole.stanford.edu/~dominic/papers/mallnets/journal/m…

さまざまなモナド類似物とベックの分配法則

…書いたバーの動機は、線形論理に出てくる自然変換 δA,B,C:A(BC) → (AB)C が、ベックの分配法則として説明出来ないか? というものです。結果的に、線形論理のδはベックの分配法則の事例になっています。そのことを示すためにバーは、分配法則を一般化しています。現在、よく知られている分配法則のタイプは: 2つのモナドのあいだの分配法則 2つのコモナドのあいだの分配法則 モナドとコモナドのあいだの分配法則(混合分配法則〈mixed distributive law〉) バ…

圏論的モダリティ:圏上の非自然な構造達

…いかも知れませんが、線形論理の意味論や微分圏では、"exponential modality", "storage modality", "resource modality", "coalgebra modality" といった言葉を使います*1。ここでは、線形論理特有のニュアンスは取り除いて、一般的な広い意味で「モダリティ」を使います*2。僕がモダリティに興味を持つ動機については最後の節に書いてあります。内容: 集合圏の付点モダリティ ユークリッド空間のあいだのなめらかな…

コンピュータ科学や組み合わせ論を“微分幾何”とみなす:CADGの夢

…s Girard)の線形論理の影がちらついているので、両者の類似性に気付いていた人はいたでしょう。が、リソース・ラムダ計算と微分ラムダ計算の関係に決着が付くのはさらに10年ほど(ボードルからは20年ほど)たってからです。 Title: What is a Categorical Model of the Differential and the Resource λ-Calculi? (2012) Author: Giulio Manzonetto Pages: 41p UR…

無料で入手できる本格的(紙なら高額)な理数系専門書15選

…sang.html 線形論理のジラールによる論理の講義です。圧縮された7つのPDFファイルに分かれています。統計/機械学習 Bayesian Reasoning and Machine Learning Bayesian Reasoning and Machine Learning作者: David Barber出版社/メーカー: Cambridge University Press発売日: 2012/02/02メディア: ハードカバー クリック: 4回この商品を含むブログを…

データの性質について考える

…破棄可能性は、終対象への唯一射!AがDに入っていることです; !A∈D(A, 1)。複製可能性や破棄可能性が、圏論や線形論理をベースにした計算科学で重要な概念であることは、例えば次の検索をして確認できます。 google: copyable discardable 日常的なデータ処理でも、変更可能性・複製可能性・破棄可能性という3つの性質を意識して、「できるだけ変更不可(イミュータブル)に」「要らないモノはサッサと捨てる」のようなエチケットを守るとトラブルを少なくできますよ。

論理的であるかのごとくに装って、根拠のないイチャモンをつける 13+2 の方法

…ついてある程度は知っておく必要があります。このブログ内に、論理の概念/用語の断片的な解説はけっこうありますから、ご興味があれば検索で拾ってみてください。 検索キーワード:古典 論理 検索キーワード:述語 論理 検索キーワード:線形論理 *1:マジメな注:「問題点を他の事情により帳消しにする」のは、現実の世界ではある程度許容されると思います。「遅刻はするが、仕事ができるから許す」とかは普通ですね。「仕事はカラッキシできないが、笑顔が可愛いから許す」となると、微妙な判断ですけど。

コンパクト閉圏と絵算で理解する線形代数とシーケント計算(入り口だけ)

…ト コンパクト論理(線形論理のサブシステム)と線形代数の関係、その概略は次に書きました。 コンパクト閉圏と奇妙な論理 f, ∩f, f∪ という記法は絵にあわせているのですが、絵の描き方における上下左右の問題は次で議論して(愚痴って)います。 モノイド閉圏、オダンゴ、留め金、池袋 非対称閉圏のカリー化:記号法を工夫すれば、右と左の混乱も解消 自画自賛:右と左が気持ちよくなった件 双対と随伴、そして左と右 シーケント計算とソフトウェアの関係は: ポートベース・コンポネント:ケー…

こんな簡単なトレース付きモノイド圏があったなんて

…とを言い出したのは、線形論理の創始者ジラール(J.-Y. Girard)だと思います。GoI構成とは、トレース付きモノイド圏からコンパクト閉圏を作り出す操作です。GoI構成は別名Int構成とも呼びます。ジラールとは独立に同じ方法が発見され、Int構成と名付けられたのだと思います。Int構成の起源が誰なのかは知りません*1。GoIは"Geometry of Interaction"の略記ですが、Intの語源はなんでしょう? Integer -- 整数です。自然数から整数を構成す…

圏のクリーネスター構成 もっと -- エフイチに触発されっぱなし

…ジツマが合うかどうかは知らんけど)。 *1:代数系の指標はモナドでうまく定義できますが、代数系の法則をどうすれば表現できるのか分からないでいます。等式や同型は高次のセルなので、高次のモナドで表現できる気もしますが、、、 *2:「同じモノ2つ」とは面妖な言い方だ、同じなら1つだろうよ。で、線形論理。 *3:双デカルト圏とは、対角/余対角/余単位/単位を使って、すべての対象に双代数の構造が入るような圏です。通常の意味のデカルト圏になっており、双対的に余デカルト圏にもなっています。

圏のクリーネスター構成 -- エフイチに触発されて

…ce)も同じ形です。線形論理の線形モダリティ(linear modality)の構成にもこの形を使います。1 + X + X2 + ... が、ベキ等な世界における指数関数のテーラー展開である状況証拠がいくつかあります。最初に挙げた教訓「まったく異なった分野・領域でも類似の現象があれば、それは偶然ではないかもしれない」によれば、これらの類似は偶然ではなく、なにかの必然かもしれません。 *1:F1を集合論的な構造として見てもしょうがなくて、世界を下支えするナニモノカとしての役割…

バエズ、アブラムスキー、ジラール等が描くビッグピクチャー:分野を貫く不思議な共通性

…のジョーンズ多項式、線形論理のカット消去、平面内でお絵描きする平面ラムダ計算(planar lambda calculus)などの不思議な対応を述べています。Esfandiar Haghverdiのプレゼン(現状、インターネットで見つからないみたいです)によると、線形論理の創始者ジラール(J.-Y. Girard)は次のような対応を考えているようです。 ジラールの用語 手続き的解釈 関数的解釈 論理的解釈 アルゴリズム(algorithm) プログラム 式 証明 計算(com…

演繹系とお絵描き圏論

…ことになり、量子系や線形論理のシステムになるでしょう(たぶん)。さらに、構造規則は回路図(ボックス&ワイヤー図、ストリング図)と相性がいいのです。一般的な「n-入力 m-出力」の回路図の全体は、圏というより多圏(polycategory)という構造を作るのですが、お絵描き計算には非常に都合がいい舞台です。僕が想定しているシナリオでは、ラムダ計算も命題論理もお絵描き(回路図)ありきなので、絵が描きやすいことが最優先の定式化になっているのです。 *1:セミナーで提示した系では、破…

カリー/ハワード(Curry-Howard)の対応を知らない子ども達および大人達へ

…1+1ができない子と線形論理 計算のエコロジーを目指して -- 資源消費量を計測する どこが面白いの?可逆計算 -- コンピューティングと北極グマ 構造規則に関してもっと色々入れ替えは、ワイヤーで描けばこんな感じ(↓)。 \ / \/ /\ / \2回続けて入れ替えるともとに戻ります。 \ / \/ /\ / \ \ / \/ /\ / \これは証明図 A B -------[Exch] B A -------[Exch] A Bしかし、入れ替えの交差(X形)が、\が上のヤツ…

ジラーとギロー

線形論理の創始者は Jean-Yves Girard氏ですが、この名前はなんて読むのだろう?と話題にしたことがあります。sumiiさんのエントリーを参考に、カタカナ書きするなら「ジャン・イヴ・ジラール」、あるいは「ル」を抜かした「ジラー」あたりではないか、ということで一段落。さて、1月11日の圏論勉強会で少し話題にした、次の論文(バエズの2008年セミナーから参照されている): Yves Guiraud, The three dimensions of proofs, Ann…

コンパクト閉圏と奇妙な論理

…えればコンパクト閉圏の定義になります。[追記]線形論理の創始者ジラール(J.-Y. Girard)が、compact linear logic って言葉を確かに使っています。「コンパクト」の意味は、論理記号/論理法則が少なくて簡略化された、ということでしょう。[/追記] *1:演繹定理が古典論理でしか成立しない、というわけではありません。 *2:×が非可換のケースも考えるなら、¬(A×B) ≡ ¬B׬A とすべきです。 *3:A --o B は指数対象です。BAと同じです。

どこが面白いの?可逆計算 -- コンピューティングと北極グマ

…回路)に対して、その一部をヒープとゴミに割り当てれば、どんな非可逆計算でも作れるのです。そういう意味では、可逆計算の計算能力は十分です。我々は非可逆計算(例えば足し算や論理AND)に慣らされているので、可逆計算によるアルゴリズムをイメージしにくいのですが、ヒープやゴミをできるでけ減らしたアルゴリズムを考えることは、ひょっとして北極グマを救うことにつながるのかも知れません。関連するエントリー: 1+1ができない子と線形論理 計算のエコロジーを目指して -- 資源消費量を計測する

計算のエコロジーを目指して -- 資源消費量を計測する

…1+1ができない子と線形論理」で、リソースに敏感な態度を紹介したのですけど、リソースに敏感になるためには、リソースの勘定ができないといけません。ごく普通の計算式のなかに、どのくらい計算リソースが含まれているか勘定する練習をしてみましょう。ここでは、計算リソースとして次の6種類を考えます。 可算器 -- 2つの入力の足し算を実行して出力する。 減算器 -- 2つの入力の引き算を実行して出力する。 複製器 -- 1つの入力をコピーして2つの出力に出す。 交差器 -- 2つの入力の…

なぜ「光が影を作ること」と「主張の一部を再主張すること」が関係するのか;あるいは、デカルト圏入門

…1+1ができない子と線形論理」のコメント欄で田辺さんから質問をいただきました。よい質問だと思いますが、それに答えるのはけっこう手間がかかります。ですが、この際(どの際?)だから、ある程度は納得していただけるような説明を試みてみましょう。[追記 date="翌日"]細かい修正をしました。[/追記]今回も、プログラミング課題とプログラミングではない課題(「考える課題」と表記)を入れています。課題番号は全部通しでふってあります。課題をやらなくても差し障りはありませんが、問題文に目を…

1+1ができない子と線形論理

…ソースに敏感な論理は線形論理(linear logic)と呼ぶので、この言葉を使えば、「線形論理は異常だ、奇妙だ、変態だ」というわけです。実際僕はそう思っていました。しかし、先日の「ボブ・クックの『物理系実務者のための圏論入門』」で紹介した圏論的量子力学/量子情報学の基礎的前提を眺めていると、量子情報(量子的真偽値、量子的命題と言ってもいい)は完全に複製することも、破棄することも許されていません。これは、人為的な仮定ではなくて、物理的な法則がそうなっているようです。となると、…

閉圏、弱いラムダ計算、弱い論理

…”は、乗法的直観主義線形論理(Multiplicative Intuitionistic Linear Logic; MILL)というものらしい。MILLの論理計算とラムダ計算はめっかった(↓)んですが、なんかピンとこないなぁ、僕は。 Nick Benton他 A Term calculus for Intuitionistic Linear Logic →http://research.microsoft.com/~nick/tlca93.ps 三位一体を確認する方針として…

論理とはなにか? (4:完) -- 論理から圏へ

…よく分かってないが)線形論理とスター自立圏(*-autonomous category)のあいだにもキレイな関係があるそうです。ここでも、証明を、標準的な形にして整理しないとうまい対応は作れません。余談ですが、デカルト閉圏もスター自立圏もラムダ計算のモデルに使われています -- ようするに、論理計算も関数計算も同じようなもの(カリー・ハワード対応)ってことですね。さてそれでは、我々にとって一番お馴染みで一番基本的な古典論理はどんな圏と対応しているのでしょうか? ストラスバーガ…

ポートベース・コンポネント:ケーススタディ

…パクト閉圏は、乗法的線形論理(multiplicative linear logic)の簡略版を解釈する場にもなっています。結果的に、線形論理風のシーケント計算が、コンポネントの計算とうまく対応するわけです。ウヒョヒョヒョヒョ(謎の笑い)。 2つのコンポネント(箱)が結合できたときは、ワイヤーを描かずに、ピタッと箱をくっつけてしまいましょう -- レゴ方式の図示。レイアウトの都合で、箱から出ているポート(の棒)の長さは適当に伸縮させてもかまいません。 事例:Lexerのコンポ…

この名前はなんて読むのだろう?

…スが多そう。例えば、線形論理の創始者Girard(Jean-Yves Girard; http://iml.univ-mrs.fr/~girard/)を、「ギラード」かと思ってましたが、「ジラー」のようです。これは、竹内外史さんがそう表記していたので間違いないでしょう。でも、時計のブランドGirard-Perregaux(http://www.girard-perregaux.ch/index_ja.aspx)だと「ジラール・ペルゴ」なんだよな(Perregauxが「ベルゴ」…

多値関数の話をもう少し -- 課題を3つ

…初から入れてしまう、とか、タプルを通常のラムダ式でエミュレートする方法はあるでしょうが、それはつまらない。「複数引数と複数戻り値を対等に扱おうよ」スタイルのラムダ計算は構成できるのでしょうか。すでに計算体系がありそうですが、僕は知りません。なお、ここでいうラムダ計算とは、ラムダ風の構文(あまりうるさいことは言わない)を持った形式計算系で、ラムダ抽象を備え、納得のいくdenotationを持つものです。※ アリティの計算が、線形論理のシーケント計算と似てる気がする、これはなに?