Projects
音MADのデータベースを作る
ユーザからデータを募集したりすることによって，音MADの体系的なデータベースを作る．
以下の目的を持って開発している．
- プラットフォームの横断
-
ニコニコ動画，Youtube，Bilibiliなどの動画/音声プラットフォームを横断して音MADを登録可能にすることによって網羅的に音MADを管理する．またそれぞれに対して統一的なメタデータを与えることによって探しやすくする．
- タグシステムの改善
-
従来の素朴なタグシステムには不満点がある．例えばタグの親子関係が陽に扱われない点や，エイリアスなどが考慮されない点などが挙げられる．そうした問題点を改善したタグシステムを作成する．
- 推薦システムの構築
-
タグシステムやユーザのいいね情報から，好きそうな音MADを推薦するシステムを作成する．
- オントロジーの構築
- 純粋な興味として，音MADのオントロジーを構築する．
以下はリンク．
- www.otomadb.com
- GitHub
- otomadb/web
- Webフロントエンド側．
- otomadb/api
- GraphQL APIとして機能するバックエンド．
- otomadb/k8s-manifests
-
Argo CDによってこのマニフェストが自宅のk8sクラスタにデプロイされる．
Lean4で様相論理を形式化する
命題論理や標準様相論理を始めとした，諸々の論理体系やその定理などをLean4で形式化する．以下の目標がある．
- 命題論理と標準様相論理の完全性定理
-
論理体系において「真である」と「証明可能である」が一致する定理のことを完全性定理という．まずはこの事実を形式化したい．
- 不完全性定理やLöbの定理などの擬似的な形式化
-
証明可能性述語を取ることが出来る，適当な条件を満たした算術の体系上では不完全性定理が成り立つ．
それらの条件，具体的にはHilbert-Bernays-Löbの導出可能性条件やその他の条件を形式化して不完全性定理やLöbの定理などを証明する．
なお目的としては後述の証明可能性論理の為に実装しているため，具体的にどのようにして「算術上で証明可能性述語を構成するのか」や「算術がそのような条件を満たすのか」という事実は形式化しない．
それらの事実のLean4による形式化はiehality/lean4-logicなどを参照．
- 証明可能性論理
-
様相を理論における証明可能性と解釈する様相論理を証明可能性論理という．証明可能性論理は不完全性定理などの性質を分析するための強力な道具となる．これらを形式化したい．
- 様相論理のシーケント計算
-
例えば，命題論理のGentzen流シーケント計算に対し，標準様相論理の各々で追加された公理を素朴に追加した計算体系や，上手く変形した規則を追加した計算体系は，
各々の論理に対して意味論的完全ではあるもののカット除去定理などの良い性質を失うということが知られている．
この問題に対して，シーケントの構造を拡張した体系などが提案されており，これらの体系では前述の良い性質を保存しながら完全である．
これらの拡張されたシーケント計算体系を形式化したい．
- 中間命題論理
-
古典命題論理と直観主義命題論理，または，直観主義命題論理と最小命題論理の間の論理は中間命題論理と言われる．それらに対する精緻化された分析をLeanによる形式化で行いたい．
- 素朴なソルバーbotとして動かす
-
命題論理をベースにしたほとんどの様相論理の体系は決定可能である事実が知られている．そのため直観主義命題論理に対するipc_botのように，ユーザーから論理式などの入力を受け取り，その式の恒真性や妥当性などを判定するbotとして動かしても理論上は計算効率などは無視すれば停止する筈である．
Leanは汎用的なプログラミング言語としても設計されているので，そのような用途にも使うことができる（出来てほしい）ので，それを確かめるため実装してみたい．
その他
細々としたもの
ここにあるものは細々としており，いくつかは開発に戻る気がないものも列挙されている．
- sno2wman.net
- このサイト．
- SnO2WMaN/infrastructures
- 自宅で実際に運用しているサーバやk8sクラスタ等の構成ファイル．
- deno2nix
-
Denoで書かれたプログラムをNixでうまく取り扱うためのユーティリティ．
Nixそのものへの情熱を失っているため，現在は特にメンテナンスはしていない．
- corepack.nix
-
Node.jsのパッケージマネージャ管理ツールであるCorepackをNixでも使うためのユーティリティ．
- All your nicovideos in Scrapbox
-
Scrapbox内で言及したニコニコ動画の動画を全て取得する．使いやすいようにAPIとして提供．
- satyxin
-
SATySFiのパッケージ解決などをNixで行うための諸々のユーティリティー．
SATySFi及びNixそのものへの情熱を失っているため，現在は特にメンテナンスはしていない．
- Incompleteness.txt
-
不完全性定理と諸々の話題についてのメモ．書き途中かつ放棄している．