「アロケーションの基本」では、予約済み区間のリストAと全体区間[s, t]を与えて、(d, x)を残りの部分からアロケートする方法を説明した。ここでは、リストに空き区間が保持されている状況でのアロケートを考える。包含（inclusion）関係α=[a, b;x]、β=[c, d…

基本的な定義以下、a, b, cなどは任意の実数（+∞、-∞を含むかも知れない）、x, y, zなどは0以上1以下の実数だとする。[a, b;x]のような形式を考える。これは、aとbを端点とする区間を表し、それに実数xが付随している。[a, b;x]で表現される対象を重み付き区…

トラス（truss）圏構成 http://d.hatena.ne.jp/m-hiyama-memo/20070117/1168993359 この定義を拡張できるかも。ブレイドとか、その他、なんらかの複体とみなせる図形的対象の圏または複圏、またはマグマを考える。これはシェープの集合だが、なんらかの結合…

僕が知る限り、自然演繹（他のシステムでもいいのだが）の証明過程を証明図のアニメーションだという説明を見たことがない。証明図が静的な図形のように語っている。これはいけない、これでは本質がわからない。計算も動的（時間的な推移）だし、証明も動的…

ゲンツェンが構造規則と論理規則を分けた理由がサッパリわからなかったが、ハロ多圏とコア圏で考えてはじめて納得がいった。しかし、エライ人は、50年も100年も先を見られるんだな。なんでシーケントを考えついたのだろう？ 奇跡に思えるよ。ハーフツイスト…

結局、ハロ多圏の多射が項であって、コア圏の射が値だな。多射は図形だが、それは構文的な存在でもあり、項書き換えの対象となる。つまり、書き換え操作が計算であり2-多射でもある。計算の結果を対応さると、式と計算の意味論ができて、多圏のほうには、2-…

ゲルハルト・マック http://d.hatena.ne.jp/m-hiyama-memo/20080207/1202355931 を見よ。

Oが基本対象の集合として、Pは、O*にdom/codを持つ多射からなる多圏とする。多射の合成は2種類あり、f: Γ ⇒ Δ,Δ' と g:Δ',Ψ ⇒ Φ に対する f[;Δ']g と、 f:Γ ⇒ Δ',Δ と g:Ψ,Δ' ⇒ Φ に対する f[Δ';]g の2種。適当な公理は満たす。それとは別に、並置によるモノ…

ひたすら計算とは違った感じで合成（結合）を扱ってみる。(f;g)(x) = g^・(f^・x) が成立することを示す。まず、を考える。正確には、<f, g, x| Exec(g^, Exec(f^, x))> だが略記した。これをフルカリー化すると <|λf.λg.λx.(g^・(f^・x) >、この引数なし関数（値はコンビネータ）をcとする。</f,>…

ラムダバブルを二重丸、三重丸で描くと少し図が簡略になる。そのとき、もとの（カリー化する前の）関数のアリティ（引数の個数）を知りたいなら、丸の数を0, 1, 2, ... と勘定し、それと、上に出ている線の本数を足す。丸の数は0から勘定する、なぜなら一番…

備忘。

まず、コンパクトシーケントとは、コンパクト論理のシーケントで、左辺と右辺のカンマの解釈が同じもの。古典論理のシーケントとは違う。次のような規則を使う。 Γ ⇒ Δ,Δ' Δ',Ψ ⇒ Φ ----------------------------[右Cut] Γ,Ψ ⇒ Δ,Φ Γ ⇒ Δ',Δ Ψ,Δ' ⇒ Φ ------…

自然演繹とシーケント計算の関係は圏の圏化になっているような気がする。圏化とは、イコールを同型で置き換えることだが、一般化すると、nセルのイコールを(n+1)の可逆セルで置き換えることだ。書き換えルールや書き換え系が重要な例。書き換えルールの適用…

表記のような計算はまったく触れないことにした（http://d.hatena.ne.jp/m-hiyama/20090109/1231481303参照）。が、ネタは考えていたので後日の為列挙しておく。 λ(f, g).λx.g(fx) 合成 λx.λy.λz.x(yz) 同じく合成 チャーチの数と掛け算（足し算は難しすぎ）…

Tクリップファイル ￥630 コクヨ クリップホルダー ￥966

本編のhttp://d.hatena.ne.jp/m-hiyama/20070813/1186984585 「圏論的指数の周辺：ラムダ計算、デカルト閉圏、ノイマン型コンピュータ」とか、http://d.hatena.ne.jp/m-hiyama/20070816/1187250855「圏論的指数の定義」とかで述べているが、「fのラムダ抽象f…

土曜日の目標を、ベータ変換だけでなくイータ変換までにしようかと、もし可能ならだが。ガンマオペレーション＝脱抽象が、ラムダオベレーション＝抽象の逆であることを理解する。背景となる意味的な法則は： Exec(λt.(φ・t), a) = Exec(φ, a) である。ここで…

ちょっと忘れたが： http://d.hatena.ne.jp/m-hiyama-memo/20071231/1199053530

本編に書くつもりだ。

http://math.ucr.edu/home/baez/week136.html より： Now, strict ω-categories are great, but we need to weaken this notion. So, first Penon defines an "ω-magma" to be something exactly like a strict ω-category but without the axioms of type B…

イオンのプライベートブランド「トップバリュ」に『ヒートファクト』つうのがあるらしい。汗かいても冷えにくい。 男用のワコール『クロスウォーカー』 -- 歩行時の歩幅を拡げ運動になると。 赤めだか 本 買うか ← 買った。 キーワード 整理[できない]／片づ…

とりあえず、紙にメモすると散らばるから。 絵の描き方 上から下 f x と、左から右 抽象は右抽象 f^ タプリングは白丸 λも白丸（バブル） Applyは黒丸 タプルの抽象は、白丸と白丸を結ぶ ベキ（指数型）は二本線、逆向きの対 タプルのアリティ（項数）は、白…

http://www.megasoft.co.jp/mifes8/

自由変数 - 大域変数とは限らない。相対的な概念。PerlやJavaScriptでは？ 束縛変数（ラムダ変数） -- 位置引数であること、本質的に無名 大域環境、局所環境 -- ようするに環境、細かいこと言わなければ同じ。 PerlやJavaScriptでの実例を考える。あと、物…

圏で定義されて圏に値を取るコチェーンを考えている。しかし、定義域が圏である必要はないと思われる。高次グラフ、またはフーティアのいうマグマが適切ではないか？

横内さんの本にあったからメモ。対象Aが has enough points または is well-pointed とは、任意のf, g:A→A に対して、f ≠ g ⇒ ∃a:1→A.( a;f ≠ a;g)。「任意のf, g:A→A」を「任意のXと、任意のf, g:A→X」にしても同じ。

自己適用の分析のために、確か適用構造だか適用代数だかという概念があったと思う。適用に相当する二項演算・があって、それがナニガシかの公理を満たすようなものだったと思うのだけど、あんまり憶えてない。とりあえず、横内さんの『プログラム意味論』を…

カウフマンのこれ： Title: Teleportation Topology (28 Jul 2004, 17 Apr 2005) Author: Louis H. Kauffman URL: http://arxiv.org/abs/quant-ph/0407224 Pages: 17 短いから読みたい。カウフマンのあの独特の感性、よくわからんのだが魅力的。語り口はわか…

圏的オペレータを考えるといいことのひとつが、シーケントの（とりあえずの）意味論ができることだ。シーケントを射と思うと、基本推論は、0個、1個、2個のホムセットの直積から1個のホムセットへの写像と考えることができる。ホムセットを(a, b)のように書…

言葉、立場、見方の多様性を強調 単眼と複眼、投影図と立体視 上江州流の紹介 絵算入門