ラムダ計算
関数化マクロオペレーター ?(E) Eをユニット定数を渡して評価する関数に変える ?(E) := λu:I.E 定数化マクロオペレーター !(E) 引数0個の関数を定数にする。 !(E) := E・! デカルトペア・マクロオペレータ λt:T.(E・t F・t) セルフ・シミュレーター 外部圏の…
0引数関数と定数は同じなのか? :圏的ラムダ計算の立場から考える 我ながら、めちゃくちゃチャンと書いてある。
モノイド圏上の加群圏の実例 - 檜山正幸のキマイラ飼育記 僕が加群圏にちょっと興味をいだいたのは、変則的なラムダ計算のモデルとして加群圏が使えないかな? と思ったからです。思っただけで、よく分かってません。 よく分かったぞ。少なくとも「積分を入…
生成元が6つ ニョロニョロ関係式が4つ マル関係式が2つ 生成元: ↑, ↓, ∩→, ←∩, ∪→, ←∪ 関係:□は単位対象Iの恒等を表すとする。 ニョロニョロは割愛 マル関係式 時計回り: ∩→;←∪ = □, マル関係式 反時計回り: ←∩;∪→ = □ [追記]TeX記法で書くと多少はマシ…
命題論理の範囲内で、 古典論理 モノイド閉圏 真偽値 圏の対象 T, ⊥ I ∧, ∨ × ¬ ¬ ⊃ , ≦ 圏の射 ブール束 圏 モノイド閉圏そのものの議論は、ブール束の議論に対応する。ブール束だけだと、構文論は出てこないから、証明可能性(|-)とかモデルに対する妥当…
演繹定理 A |- B ⇔ |- A⊃B 演繹定理、少し一般化 A, B |- C ⇔ A |- B⊃C モーダスポネンス A, A⊃B |- B 連言の原理 A |- B かつ C |- D ⇒ A, C |- B∧D 否定を含むもの。 二重否定(古典) ¬¬A = A 待遇の原理の半分 |- A⊃B ⇒ |- ¬B⊃¬A 含意の言い換え(古典)…
多圏 シーケント計算 ラムダ計算 結合 カット 変数と式の置換(substitution) 全体のモノイド積 マージ なし カリー化 含意導入 ラムダ抽象 アンカリー化 含意消去 評価 部分的モノイド積 連言導入 ペアリング 部分的モノイド積の逆 連言消去 アンペアリン…
圏 積 指数 双対 テンパリー/リーブ圏 釘列の併置 積に同じ 自己双対 符号付きテンパリー/リーブ圏 釘列の併置 双対との積 符号の反転 関係圏 集合の直積 積に同じ 自己双対 ベクトル空間の圏 テンソル積 双対との積 双対空間 集合圏 直積 関数集合 なし …
次を読めば参考になるはず。 Title: Quasistrict symmetric monoidal 2-categories via wire diagrams Author: Bruce Bartlett URL: http://arxiv.org/abs/1409.2148 Pages: 18p. Title: Polycategories via pseudo-distributive laws Author: Richard Garne…
ラムダ計算の重箱の隅(?):タプルと成分 - 檜山正幸のキマイラ飼育記 メモ編 : やっぱり多圏の議論をしないとどうにもならない、と感じる。 ... 重箱の隅でもないな、これは。 難しい問題が持ち上げる。Cが厳密モノイド圏のとき、それから厳密多圏Poly(C)を…
やっぱり多圏の議論をしないとどうにもならない、と感じる。ラムダ計算は、「タプルを出さないのが粋」みたいな風潮にもウンザリ。タプルを扱うなら、項レベルでペア構文 (E, F) は必要だ。これを、カンマが二項演算子と解釈する。ただし、カンマは左結合的…
バエズの留め金の応用 - 檜山正幸のキマイラ飼育記 メモ編 バエズの留め金(クラスプ)を使って、ベータ変換とエータ(イータ)変換の絵を書いた。恒等射のラムダ抽象のベータ変換は随伴の余単位、エータ変換が随伴の単位を与える。バエズの留め金を使うと、…
バエズの留め金(クラスプ)を使って、ベータ変換とエータ(イータ)変換の絵を書いた。恒等射のラムダ抽象のベータ変換は随伴の余単位、エータ変換が随伴の単位を与える。バエズの留め金を使うと、ニョロニョロ関係式が比較的自然に描ける。後日、スキャン…
クックの三角形=ディラックのブラケットの採用 バエズのクラスプを積極的に利用 クラスプと極性と線形含意記号(指数の記法)の統合 evを台形にした。 描画方向を示す旗記号 極性の印はプラスが○、マイナスが●で、マイナスからプラスが矢印の方向。だから、…
A×(B + C) = (A×B) + C これは分合律(dissociative law, linearly distributive law)。 A×(B×C) = (A×B)×C なら通常の結合律。別な演算*があって、 A * (B×C) = (A * B) * C ならなんと呼ぶか? * を含意=指数だと思うと、これはカリー同型。分合律やカリ…
https://www.cs.cmu.edu/~fp/courses/linear/handouts/lnd.pdf からの引用(画像としてコピー)線形含意の記号は 。ラムダ絵算で使おうと思っている。
クラスプ(clasp; 留め金)の絵。モノイド閉圏、オダンゴ、留め金、池袋 - 檜山正幸のキマイラ飼育記の図: 方向の取り方: カリー化: 左右のカリー化: この絵法を最初に見たオリジナル論文: Title: Computation and the Periodic Table (ATMCS 2008) Aut…
終対象またはモノイド圏の単位対象からの射を「要素」とみなすのは割と自然な発想。デカルト圏なら終対象=単位対象なので、Cをデカルト圏として、Elt(C) = {e∈Mor(C) | dom(e) = 1 } としてElt(C)を定義する。Elt(C)は単に射の集合で構造を持たない。Cはデ…
豊饒圏をちゃんと定義したい - 檜山正幸のキマイラ飼育記豊饒圏の定義とか、割と詳しく書いている。 関数で関手が表現できるって変でしょ、どういう仕掛けかな? - 檜山正幸のキマイラ飼育記総称関数が関手の表現に使える事情。 圏論的指数の定義 - 檜山正幸…
結局、自然演繹とはシーケント計算の簡便な別法ってことかと。α = (Γ⇒Δ) が定理シーケント、つまり証明できるシーケントのとき、 Γ ----[α] Δという自然演繹の推論図を使ってイイゾと。また、Γ⇒Δ から Γ'⇒Δ'がシーケント計算で証明できるとき、対応する自然…
γアノテーションは、束縛子や限量子と似た構文で、γ記号の後に変数を伴いスコープを持つ。γにくっついている変数をγ変数と呼ぶことにする。γアノテーションに変数の束縛作用はなくて、γアノテートされた項(スコープ内部)でγ変数は自由のままである。したが…
CCC計算 - 檜山正幸のキマイラ飼育記 メモ編 で出したγ導入の件。γアノテーションという記法をラムダ計算に追加して、γアノテーションの導入規則も加える。γアノテーションの「γ」には何の意味もない。ギリシャ文字を適当に選んだだけ。ガンマ計算とかガンマ…
本編: 感動か効率性か - 檜山正幸のキマイラ飼育記 オカシイと文句を垂れるなら、修正案を提示しないとね。シーケントの左辺が型宣言の集まり、右辺が型付き代入文の集まりとなる形を仮にCCCシーケントと呼ぶ。CCCシーケントの意味はデカルト閉圏の射だが、…
通常のラムダ計算を0-計算とすると、自然演繹が1-計算で、シーケント計算(の証明)が2-計算だろう。各次元のラムダ計算がバラバラで統合されてないのがダメ。大きなラムダ計算は統合の試みだが、ちゃんとやってないな。デカルト閉圏の構造を写し取るのだか…
本編 随伴のニョロニョロ関係をTypeScriptで確認する - 檜山正幸のキマイラ飼育記 の手計算 εP(X) P(ηX) = idP(X) まず定義: A:Type; η<X> :: X => A->X×A := x:X => λa:A.(x, a); ε<X> :: (A->X)×A => X := (f, a):(A->X)×A => (f a);ηとεはラムダ項じゃなくて射</x></x>…