プログラム意味論
記法: コ/モナド : モナドまたはコモナド A∨ : 上付きのチェックマーク(のつもり)は、文字修飾子。使い途はボールドなどと同じ。Aに対する演算子ではない。コモナドを表す文字・語への文字修飾に使う。 ベックの分配系は4種類あって、 モナド・モナド分…
関連しそうな自分のエントリー。ウヘー、我ながらいっぱいあるなー。ざっと読んでいこう。読んだら、感想を一言ずつ書いていこう。 述語論理とインデックス付き圏と限量随伴性 20170824 テンソル積の作り方 20160829 中学レベル代入計算からカリー/ハワード…
現実機械、理想機械、超越機械がある。現実機械は無視、理想機械と超越機械の実行時間を考える。 命題Pに対して、超越機械による実行時間τ(P)は、τ(P) = 0 超越機械=神 なので、あらゆる命題を瞬時に確定的に判断する。理想機械は、次の特徴を持つ。 メモリ…
関数名=関数記号=関数インデックス=エントリーポイント 関数=関数実体=関数名の意味=写像 関数定義=関数の定義体=関数のソースコード=関数のテキスト=関数の式 関数コード=コンパイルされた関数=バイナリの関数=関数のオブジェクトコード 関数…
計算的な万能性で、 選択肢1: 万能対象=万能コード領域 選択肢2: 万能対象=万能データ領域 が考えられるが、ノイマン方式の原理により コード領域=データ領域なので、通常は万能コード領域と万能データ領域は区別しない。Uが万能データ領域であることは、…
まず、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 注目…
Minimum and Optimistic Functional Language はやめて、 Multi-Objective Fragile Languate にするか。手続き的機能 while, for, 破壊的代入 とかも入れたいから。fragileの解釈は「イイカゲンでチャンとしてない」。 if -- if式 then else end find -- fin…
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-セオリーの立場からは、次は、次元や具体的状況が違うだけで同義になる。 変数状態 値割り当て 評価環境 リテラル(定数)解釈 データベース状態 データベースインスタンス 代数セオリーのモデル=代数 基本命題の真偽値割り当て なんらかの意味のモデルイ…
まず、同義語のまとめ。 指標⊆仕様=セオリー=プレゼンテーション=コンピュータッド=ポリグラフ=グラフ=箙 モデル=構造=代数=加群=表現 基本構図は: A ∈0 n-AlgD(τ, A) これの文脈は、 τ ∈0 n-Thy D ∈0 (n+1)-Thy A ∈0 (n+1)-AlgD'(τ', A') 文脈内…
C上のモナドとD上のモナドのあいだの変換を考えたい。一番有望そうなのは、弱2-関手のあいだの弱2-自然変換だろう。
だんだん思い出した:指標=インターフェイスの理論 - 檜山正幸のキマイラ飼育記 メモ編 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 }これはミクスチャの例。同じ名前に対して、「宣言…
シャドーイングの問題 - 檜山正幸のキマイラ飼育記 メモ編の続き。入れ子 Σ | Δ があるとき、シャドーイングがあろうとなかろうと、Σ←Σ'→(Σ' + Δ) ができる。この事実から、一段階の入れ子はスパンで表現できることがわかる。一般のスパンではなくて、両脚が…