あ、そうか。グラフのある点から、n本以下の辺をたどっていける頂点＋辺のスター状近傍をn-近傍と呼ぶことにする。0-近傍、1-近傍、2-近傍、と定義できる。半整数に関しても近傍を考えればいいんだな。特に、1/2-近傍＝半近傍が大事だ。1/2の意味は、辺を真…

idA : A→A literalx : void→sngleton(x) literalvoid = idvoid : void→void discA : A→void copyA : A→A×A tupleA,B : A, B→A×B detupleA,B : A×B→A, B chooseA : A→A, A mergeA,B : A, B→A∪B branchA,B : A+B→A, B 以下に描画用のソース。

http://d.hatena.ne.jp/m-hiyama-memo/20120104/1325638861 : いずれ説明する。 今日説明する。絵に基づいて説明する。 原寸大これがコマンドなわけだが： command body とはPythonコード、またはCatyScriptコードで、コマンドの本体となる定義体（definitio…

例えば、この図のソースは次。 // -*- coding: utf-8 -*- // sequent[ gv:node --shapa=point --style=invis sin1, gv:node --shape=point --style=invis sin2, gv:node --shape=point --style=invis sin3, gv:node --label="> *" --shape=diamond --style=f…

集合圏で考えると、!A : A → 1 があるから、これでデータを捨てることになる。しかし、1は「無」ではないから存在がなくなったわけではない。単に縮めただけ、あるいは要素の区別をなくしただけで、捨てたことになってないような気がする。だが、集合圏では…