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

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

プログラム意味論

メイヤー系とコ/モナド

記法: コ/モナド : モナドまたはコモナド A∨ : 上付きのチェックマーク(のつもり)は、文字修飾子。使い途はボールドなどと同じ。Aに対する演算子ではない。コモナドを表す文字・語への文字修飾に使う。 ベックの分配系は4種類あって、 モナド・モナド分…

インデックス付き圏のフビニの定理

関連しそうな自分のエントリー。ウヘー、我ながらいっぱいあるなー。ざっと読んでいこう。読んだら、感想を一言ずつ書いていこう。 述語論理とインデックス付き圏と限量随伴性 20170824 テンソル積の作り方 20160829 中学レベル代入計算からカリー/ハワード…

機械の種類と実行時間

現実機械、理想機械、超越機械がある。現実機械は無視、理想機械と超越機械の実行時間を考える。 命題Pに対して、超越機械による実行時間τ(P)は、τ(P) = 0 超越機械=神 なので、あらゆる命題を瞬時に確定的に判断する。理想機械は、次の特徴を持つ。 メモリ…

関数の意味

関数名=関数記号=関数インデックス=エントリーポイント 関数=関数実体=関数名の意味=写像 関数定義=関数の定義体=関数のソースコード=関数のテキスト=関数の式 関数コード=コンパイルされた関数=バイナリの関数=関数のオブジェクトコード 関数…

プログラマへの注意とチューリング対象

計算的な万能性で、 選択肢1: 万能対象=万能コード領域 選択肢2: 万能対象=万能データ領域 が考えられるが、ノイマン方式の原理により コード領域=データ領域なので、通常は万能コード領域と万能データ領域は区別しない。Uが万能データ領域であることは、…

ベキク〈bekic〉の公式

まず、Bekicの発音、 https://www.howtopronounce.com/bekic/ ベキクでいいようだ。関連する記事は、 http://d.hatena.ne.jp/m-hiyama-memo/20131001/1380609526 双コンウェイ圏の構造を探る http://d.hatena.ne.jp/m-hiyama-memo/20080527/1211875554 注目…

Moflのキーワード

Minimum and Optimistic Functional Language はやめて、 Multi-Objective Fragile Languate にするか。手続き的機能 while, for, 破壊的代入 とかも入れたいから。fragileの解釈は「イイカゲンでチャンとしてない」。 if -- if式 then else end find -- fin…

Mofl(モフる)

Moflの背景圏Moflの背景圏はMofCatとする。MofCatはPtSet上の具象圏。PtSetnonsの部分圏とみなす。ただし、PtSetnons全体は必要なくて、PtSetnons≦ω内で議論する。 MofCatは、デカルト半環圏である。×, 1, + 0, <, >, [, ] MofCatは、クリーネスターを備えて…

帰納構造、帰納代数

帰納的構成はよく使うが、構成(生成)された後にできる構造の話。Xが生成された集合、Aが初期集合、ciがコンストラクタだとする。これらを、(X, A, c1, ..., cn) という構造だと考える。次の記法を使う。 X0 := A X+ := X\A 定義より、X = X0 + X+。X0の要…

同義語になる

n-セオリーの立場からは、次は、次元や具体的状況が違うだけで同義になる。 変数状態 値割り当て 評価環境 リテラル(定数)解釈 データベース状態 データベースインスタンス 代数セオリーのモデル=代数 基本命題の真偽値割り当て なんらかの意味のモデルイ…

n-タイプの基本構図

まず、同義語のまとめ。 指標⊆仕様=セオリー=プレゼンテーション=コンピュータッド=ポリグラフ=グラフ=箙 モデル=構造=代数=加群=表現 基本構図は: A ∈0 n-AlgD(τ, A) これの文脈は、 τ ∈0 n-Thy D ∈0 (n+1)-Thy A ∈0 (n+1)-AlgD'(τ', A') 文脈内…

異なる台のモナドのあいだの変換

C上のモナドとD上のモナドのあいだの変換を考えたい。一番有望そうなのは、弱2-関手のあいだの弱2-自然変換だろう。

論理におけるrecursion-capable

だんだん思い出した:指標=インターフェイスの理論 - 檜山正幸のキマイラ飼育記 メモ編 Lがrecursion-capable ⇔ ImplLがweakly trace-admissible Lが、構造に対する制約・条件を記述する論理言語(命題言語/証明言語)を備えているとする。このとき、Lの指…

だんだん思い出した:指標=インターフェイスの理論

あああああー、そうか。それをjanus〈ヤヌス〉と呼んでいたのだ。 指標=インターフェイスの理論 - 檜山正幸のキマイラ飼育記 メモ編 双面神Janus プログラミング言語Lを、指標の圏Sigとその上のモナド L = (L, μ, η) と同一視する。つまり、プログラミング…

指標=インターフェイスの理論

[追記]いいこと気付いたと思ったが、ずっと昔に同じこと書いてたわ。アジャー。「だんだん思い出した:指標=インターフェイスの理論 - 檜山正幸のキマイラ飼育記 メモ編」参照。[/追記]パラメータ付きのインターフェイスが難しいのは、それがプリミティブで…

米田カン拡張とエルブランモデル族

Σを指標として、SをΣから生成された自由圏とする。SからSetへの関手をモデルと呼ぶ。モデルは前層だから、モデルの全体は前層圏PSh(S)と同じ: PSh(S) = Mod[Σ] 。米田埋め込み よ:S→PSh(S) が考えられる。この米田埋め込みは、Σのエルブランモデルの族と同…

インスティチューション、マルチ・インスティチューション、マンダラ

最近、マンダラの精神を忘れていたかも知れない。「この世はマンダラだ」 マンダラ→ http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?word=%2A%5B%A5%DE%A5%F3%A5%C0%A5%E9%5D ミニマンダラ→ http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?word=%2A%5B…

ローヴェア・セオリーの操作

L, L', Mなどはローヴェア・セオリーとする。 ローヴェア・セオリーの直和 L + M ローヴェア・セオリーのテンソル積 LM テンソル積はどの程度存在するかよくわからんが、次が成立する。 Mod(L, Mod(M, C) Mod(LM, C) この同型は(それが存在するなら)超便利…

ローヴェル・セオリー関係の文献。

ステイ/メレディス(↓)から辿って、主にローヴェル・セオリー関係の文献。 Logic as a distributive law Mike Stay, Lucius Gregory Meredith 17p https://arxiv.org/abs/1610.02247 ステイ/メレディス(↑)が参照しているもの。まずはハイランド/パワー: T…

コンピュータッドとシリンダとコボルディズム圏

コンピュータッドは図形的な対象。シリンダを作ることは意味がある。シリンダはホモトピーと関連する。写像錘とか錐体、簡易懸垂とか、色々と図形的な構成が出来る気がする。コボルディズム圏も作れるのではないか。単に、コンピュータッドの射を考えるので…

同義語・多義語の例

ステイ/メリディスの次の論文、とても良い。 Title: Logic as a distributive law Author: Mike Stay, Lucius Gregory Meredith URL: https://arxiv.org/abs/1610.02247 僕がふだん考えていることだから、問題意識が一致して分かりやすい。本論じゃないとこ…

ローヴェル・フレームワーク

代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編 の続きで、ローヴェル・セオリーを可能とするフレームワークについて。ローヴェル・セオリーローヴェル・セオリーの導入・説明では、有限集合の圏FinSetの骨格として、基数(それ自身集…

指標とモデルと意味論

昨日 代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編、次の用語を導入した。当たり前で自己説明的な言葉だと思う。 (n-)?代数(的)?定義(形式)? (n-)?定義(形式)? 同義語が: (n-)?指標 (n-)?仕様 (n-)?セオリー (n-)?型クラス (n-)?イ…

代数的定義形式とアンビエント構造

内容: 代数的定義形式 代数的定義形式の同義語群 アンビエント 定義形式のアンカリング 単位対象と格上げ 値k-射と定義形式の格上げ モデルとモデルの圏 TBD:ローヴェル・フレームワーク TBD:族と抽象と脱抽象 代数的定義形式n-圏と関連する圏論的実体〈c…

環境、引数、パラメータ

トランスフォーマーを考えると、定義体の内部で使う名前の供給源として、 名前は環境から供給される(名前は環境内のモノを参照する) 名前は引数から供給される(名前は引数内のモノを参照する) 名前はパラメータから供給される(名前はパラメータ内のモノ…

指標のモデル圏のあいだの関手

Standard MLではモロに関手(functor)と呼んでいるのだが、やり過ぎだと思うので: トランスフォーマー: 現状、これを使っている。問題は、自然変換のトランスフォーメーションと似ていること。 リダクト: インスティチューションではリダクト関手(reduc…

トランスフォーマーの操作

第一級オブジェクトとしてのトランスフォーマーを考えると: トランスフォーマーに名前を付けられる。名前無しでも扱える。 概念的には、トランスフォーマーが等しいかどうかを判定できる。現実的には無理なこともある(つうか、たいていは無理だけど)。 ト…

指標 ≠ コンピュータッド

今まで、指標はコンピュータッドの同義語としてきたが、どうも違う。その違いは指標は名前(ラベル)があること。単なるグラフとラベル付きグラフの違い。2つの指標をとると、まったく無関係とは限らない。ラベリングによって、必然的にスパン構造=貼り合わ…

ミクスチャ=ごった煮

宣言(名前のプロファイリング)と定義(束縛、名前のアタッチング)をゴッチャに混ぜて書いた形式をミクスチャと呼ぶことにする。 mixture Succ := { type X; X := int; value e: X; function succ : X->X }これはミクスチャの例。同じ名前に対して、「宣言…

入れ子とシャドーイングとモノスパンの圏

シャドーイングの問題 - 檜山正幸のキマイラ飼育記 メモ編の続き。入れ子 Σ | Δ があるとき、シャドーイングがあろうとなかろうと、Σ←Σ'→(Σ' + Δ) ができる。この事実から、一段階の入れ子はスパンで表現できることがわかる。一般のスパンではなくて、両脚が…