n-キューブは、単にn次元ユークリッド空間の標準的なキューブ [0, 1]n のこと。n-キューブを同時に一挙に把握できる幾何学的な空間と捉えるときキャンバスと呼ぶことにする。キャンバス内で時間は流れない。一方、[0, 1]n-1×[0, 1] と分解して、最後の次元を…

射影した図の色塗りに間違いがあるようだ。どっちにしても、射影図のキャンバスと同じ次元の部分は全く当てにならない。余次元が1以上の骨格は、元の空間では余次元2以上だから、ある程度はトポロジーを反映している。

http://tigger.uic.edu/~rgl/shrtknots.pdf を読んだが、定義が細かすぎると思った。次のように簡略化してよいだろう。 基本イベント（elementary event）→基本1-セル 縁付き基本イベント（framed (elementary) event）→縁付き基本1-セル スチル→直列1セル＝…

1次元以上のキャンバスは、[0, 1]n になる。通常のユークリッド空間内の単位矩形だと思ってよい。このキャンバスはn個の軸を持ち、主方向を持つ。 キャンバス次元 軸 主方向 0 なし なし 1 x x方向 2 x,y y方向 3 x,y,z z方向 4 x,y,z,w w方向 n x1,...,xn x…

stricmp問題 - 檜山正幸のキマイラ飼育記 メモ編 の件。共通インクルードファイルのなかで、#include されていた。このため、共通インクルードファイルを直接・間接にインクルードしているファイル（すべてのソースファイル）で、 #include "common.h" // 間…

定理（theorem）は、公理や定義も含む。名前式 の形に対応する。右辺にも名前が出現するが、その名前はセルの名前。右辺に出現する名前のなかでひとつだけが主セルの名前として特定されている。「名前→式」の展開と「式→名前」の縮約がクリック操作で可能だ…

とりあえず2セルに対して縦結合と横結合をやろうと思った。 0セル、1セル、2セルと順に作っていくと、2つの2セルα、βが出来る。 2セルと2セルとの縦結合（1次元接合セルによる結合）は直接出来る。 2セルと2セルとの横結合が出来ない。 2セルと1セルのヒゲ結…

とりあえず試行錯誤だ。 方向は、左から右（これはいい）、下から上（逆だーーー！） アタッチ操作は、「メインの図に、パレットのセルを」アタッチする。今の図にアタッチしたい部品をパレットから選んでクリックする。アタッチャブルかどうかは判定してく…

ムービー変形 - 檜山正幸のキマイラ飼育記 メモ編 で挙げた Moving Knots and Knotted Surfaces http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.49.4021&rep=rep1&type=pdf は非常に良い解説で、3次元の結び目とその2次元表現である結び目図（kn…

初歩的モノイド圏（rudimentary monoidal category）とは、 対象は自然数 モノイド積の対象部分は足し算 である圏。その例： 自然数の順序圏 置換圏（対称圏） 組み紐圏、、トレース付きだとサークル（ループ）を認める。 テンパリー／リーブ圏、、トレース…

過去の記事↓から、アレクサンダー／パヒナー移動（Alexander/Pachner move）、カーター／サイトウ（さいとう・まさひこ）移動に関するものを拾った。 カーター／さいとう移動 - 檜山正幸のキマイラ飼育記 メモ編 Pachner移動 - 檜山正幸のキマイラ飼育記 メ…

<string.h>をインクルードしても、sricmp関数が使えない（見えない）。知らなかったが、ANSIではstricmp, strcmpi関数は廃止されたようだ。次のように __STRICT_ANSI__ 定数を無効化してからインクルードするとstricmpが宣言される。 #ifdef __STRICT_ANSI__ #undef __</string.h>…

https://msdn.microsoft.com/ja-jp/library/cc429748.aspx : GetCurrentTimeこの関数は使われなくなりました。Win32 アプリケーションでは、GetTickCount 関数、または、レジストリの HKEY_PERFORMANCE_DATA 内にあるカウンタを使ってください。ただし、過去…

MSVC /c/Program Files (x86)/Microsoft SDKs/Windows/v7.{0,1}A/Include/ 古いGCC /c/Installed/MinGW/include/ TDM-GCC /c/Installed/TDM-GCC-64/x86_64-w64-mingw32/include/ [追記]gccのパス違った。もっと優先されるパスがある。g++ -v でコンパイルす…

終対象またはモノイド圏の単位対象からの射を「要素」とみなすのは割と自然な発想。デカルト圏なら終対象＝単位対象なので、Cをデカルト圏として、Elt(C) = {e∈Mor(C) | dom(e) = 1 } としてElt(C)を定義する。Elt(C)は単に射の集合で構造を持たない。Cはデ…

豊饒圏をちゃんと定義したい - 檜山正幸のキマイラ飼育記豊饒圏の定義とか、割と詳しく書いている。 関数で関手が表現できるって変でしょ、どういう仕掛けかな？ - 檜山正幸のキマイラ飼育記総称関数が関手の表現に使える事情。 圏論的指数の定義 - 檜山正幸…

結局、自然演繹とはシーケント計算の簡便な別法ってことかと。α = (Γ⇒Δ) が定理シーケント、つまり証明できるシーケントのとき、 Γ ----[α] Δという自然演繹の推論図を使ってイイゾと。また、Γ⇒Δ から Γ'⇒Δ'がシーケント計算で証明できるとき、対応する自然…

「二値変数」と訳されるが、二分変数かな。分類を二値で行う名義（ラベル）変数。

γアノテーションは、束縛子や限量子と似た構文で、γ記号の後に変数を伴いスコープを持つ。γにくっついている変数をγ変数と呼ぶことにする。γアノテーションに変数の束縛作用はなくて、γアノテートされた項（スコープ内部）でγ変数は自由のままである。したが…

CCC計算 - 檜山正幸のキマイラ飼育記 メモ編 で出したγ導入の件。γアノテーションという記法をラムダ計算に追加して、γアノテーションの導入規則も加える。γアノテーションの「γ」には何の意味もない。ギリシャ文字を適当に選んだだけ。ガンマ計算とかガンマ…

本編： 感動か効率性か - 檜山正幸のキマイラ飼育記 オカシイと文句を垂れるなら、修正案を提示しないとね。シーケントの左辺が型宣言の集まり、右辺が型付き代入文の集まりとなる形を仮にCCCシーケントと呼ぶ。CCCシーケントの意味はデカルト閉圏の射だが、…

まずはMSVC2010： #include <time.h> #include <stdio.h> int _tmain(int argc, _TCHAR* argv[]) { printf("sizeof(int):%d\n", sizeof(int)); printf("sizeof(long):%d\n", sizeof(long)); printf("sizeof(time_t):%d\n", sizeof(time_t)); return 0; } sizeof(int):4 sizeof</stdio.h></time.h>…

Continuation Semantics of Expressing Implication by Negation Constructing a small category of setoid / https://www.diva-portal.org/smash/get/diva2:399799/FULLTEXT01.pdf Monads of a Non-Associative Composition / duploids.pdfがローカルにある…

C++で、 throw() 古い noexcept 新しい noexceptは、無例外保証の指定構文。当たり前だが例外について記述してるんではない。

モナドにおける「拡張」の補遺：アンクライスリ化かな - 檜山正幸のキマイラ飼育記 例外モナドのクライスリ圏の話。tryブロックが埋め込みJの随伴であること。これ、アイレンベルク／ムーア圏だとどうなる？ 例外モナドのアイレンベルク／ムーア代数は付点集…

https://msdn.microsoft.com/ja-jp/library/cc448053.aspx https://msdn.microsoft.com/ja-jp/library/cc448089.aspx [追記]詳しいことをシフトJIS文字列とユニコード文字列の変換のときの終端ヌルとかバッファ長とか - 檜山正幸のキマイラ飼育記に書いた。[…

通常のラムダ計算を0-計算とすると、自然演繹が1-計算で、シーケント計算（の証明）が2-計算だろう。各次元のラムダ計算がバラバラで統合されてないのがダメ。大きなラムダ計算は統合の試みだが、ちゃんとやってないな。デカルト閉圏の構造を写し取るのだか…

とあるトラブルで、ビチャビチャになったので捨てる。が、オリジナルのURLを後で探す。 On the Category of PROPs / Hackney & Robertson BASIC CONCEPTS OF ENRICHED CATEGORY THEORY/ Max Kellyhttp://www.tac.mta.ca/tac/reprints/articles/10/tr10.pdfch…

MinGWのgccはWindows.hを備えているので、 #include <Windows.h> #pragma comment(lib, "shlwapi.lib") とかできる。Win32 APIを呼ぶことができる。PowerShellコマンドを真似たヤツ。 bool testPath(const string &path, bool container) { if (container) { return (bo</windows.h>…

本編 随伴のニョロニョロ関係を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>…