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

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

2016-02-29から1日間の記事一覧

Poly(C)の構成の方法 (5)シーケント推論規則

圏 論理 自己双対コンパクト閉圏 超コンパクト論理 モノイド閉圏 一般コンパクト論理 対称モノイド閉圏 対称コンパクト論理 デカルト閉圏 デカルト・コンパクト論理 デカルト・コンパクト論理が、直観論理の連言・含意フラグメント。超コンパクト論理、×, I …

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

多圏 シーケント計算 ラムダ計算 結合 カット 変数と式の置換(substitution) 全体のモノイド積 マージ なし カリー化 含意導入 ラムダ抽象 アンカリー化 含意消去 評価 部分的モノイド積 連言導入 ペアリング 部分的モノイド積の逆 連言消去 アンペアリン…

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

Seq(C)とPoly(C)はアルファベット(または指標)で相対化する。アルファベットの構成要素は、 |C| の有限部分集合V Mor(C| の有限部分集合E dom, codをE上に制限したときに、(V, E)が有向グラフになることが条件。さらに関係の有限性を入れる。 Cにおいて(V,…

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

記法を変える。PolyFull(C)じゃなくて、Seq(C)にする。 Seq(C)は単なる圏。その対象を列(シーケンス)、その射をシーケントと呼ぶ。 Seq(C)のモノイド積(連接)は、# と書く(++, ##の略記)。 |Seq(C)| = |C|* Seq(C)(Γ, Δ) C(Prod(Γ), Prod(Δ)) シングル…