このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

ラムダ計算

面白いラムダ式やオペレーター

関数化マクロオペレーター ?(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 含意の言い換え(古典)…

Poly(C)の構成の方法 (4)

多圏 シーケント計算 ラムダ計算 結合 カット 変数と式の置換(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シーケントと呼ぶ。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>…