ハイパーインスティチューションの構文論のために、名前の理論とディヴィジョニング／プロファイリングの理論が必要。名前と記号は同義語。名前に対する概念： 有意名： 意味＝意味的割り当てが決っている名前。これは意味論的概念。 ディヴィジョン付き名：…

変換子〈substitutor | 代入子〉は、指標射〈signature morphism | base morphism〉と同義語だが、射の向きは違う。つまり、変換子はSigopの射になっている。 ML用語 インスティチューション用語 ストラクチャ S 指標 S SからTへのファンクタ TからSへの指標…

ダメさ 困ったバンドリング→ 分離分割する。 困ったエンタングルメント →絡み合い・もつれ合いをほどく。 Coqの場合は、名前が漏出する。 骨絡みの欠陥なので、修復不可能。再設計、再実装。名前管理・オーバーロード機能と構造記述機能を別に持つ。MLの型ク…

参考： MLソースを扱うとき - 檜山正幸のキマイラ飼育記 メモ編 デスクトップにIsabelle2016（少し古い）のアイコンがある。 このアイコンは C:\Installed\Isabelle2016\Isabelle2016.exe を指している。 Isabelle2016.exeの実体は、jEditをフロント、PolyML…

ハイパーインスティチューションの目指すところは、an overall framework for computing and logic だ。主要な道具は indexed/fibred/parametrized computads だ。アイディアの源泉は、hyperdoctrineとinstitution。

プログラミングとの対応 プログラミング ハイパーインスティチューション インターフェイス 指標 インターフェイスのハード実装 モデル インターフェイスのソフト実装 指標への射 インターフェイス上のプログラム 指標からの射 インターフェイスのアダプター…

言語サーバープロトコル - 檜山正幸のキマイラ飼育記 メモ編 Isabelle風の継続的同期＆チェッキングだと、もっと細かく精密な通信が必要になる。 次のことが必要。 ソース完全保存性 テキスト編集可能性 構造編集可能性 構文解析木の豊かな情報を付加して、…

2015年に、「言語処理サーバーとそのプロトコル」という記事を書いたけど、Microsoftはこの方向を追求しているね。 https://langserver.org/ The Language Server protocol のページ 言語サーバープロトコルのドキュメントは、 https://github.com/Microsoft…