Projects

ユーザからデータを募集したりすることによって，音MADの体系的なデータベースを作る． 以下の目的を持って開発している．

プラットフォームの横断

ニコニコ動画，Youtube，Bilibiliなどの動画/音声プラットフォームを横断して音MADを登録可能にすることによって網羅的に音MADを管理する．またそれぞれに対して統一的なメタデータを与えることによって探しやすくする．

タグシステムの改善

従来の素朴なタグシステムには不満点がある．例えばタグの親子関係が陽に扱われない点や，エイリアスなどが考慮されない点などが挙げられる．そうした問題点を改善したタグシステムを作成する．

推薦システムの構築

タグシステムやユーザのいいね情報から，好きそうな音MADを推薦するシステムを作成する．

オントロジーの構築

純粋な興味として，音MADのオントロジーを構築する．

以下はリンク．

1. www.otomadb.com
2. GitHub

otomadb/web

GraphQL

Next.js

Node.js

Storybook

Tailwind CSS

TypeScript

Vercel

urql

Webフロントエンド側．

otomadb/api

GraphQL

GraphQL Yoga

Neo4j

Nix

Node.js

PostgreSQL

Prisma

TypeScript

GraphQL APIとして機能するバックエンド．

otomadb/k8s-manifests

ArgoCD

Kubernetes

Argo CDによってこのマニフェストが自宅のk8sクラスタにデプロイされる．

命題論理や標準様相論理を始めとした，諸々の論理体系やその定理などをLean4で形式化する．

更新時現在では以下が形式化されている．詳しくはリンク先のリポジトリを参照のこと．

• 一般的な標準様相論理の完全性定理

また，以下の目標がある．

不完全性定理やLöbの定理などの擬似的な形式化

証明可能性述語を取ることが出来る，適当な条件を満たした算術の体系上では不完全性定理が成り立つ． それらの条件，具体的にはHilbert-Bernays-Löbの導出可能性条件やその他の条件を形式化して不完全性定理やLöbの定理などを証明する． なお目的としては後述の証明可能性論理の為に実装しているため，具体的にどのようにして「算術上で証明可能性述語を構成するのか」や「算術がそのような条件を満たすのか」という事実は形式化しない． それらの事実のLean4による形式化はiehality/lean4-logicなどを参照．

証明可能性論理

様相を理論における証明可能性と解釈する様相論理を証明可能性論理という．証明可能性論理は不完全性定理などの性質を分析するための強力な道具となる．これらを形式化したい．

様相論理のシーケント計算

例えば，命題論理のGentzen流シーケント計算に対し，標準様相論理の各々で追加された公理を素朴に追加した計算体系や，上手く変形した規則を追加した計算体系は， 各々の論理に対して意味論的完全ではあるもののカット除去定理などの良い性質を失うということが知られている． この問題に対して，シーケントの構造を拡張した体系などが提案されており，これらの体系では前述の良い性質を保存しながら完全である． これらの拡張されたシーケント計算体系を形式化したい．

中間命題論理

古典命題論理と直観主義命題論理，または，直観主義命題論理と最小命題論理の間の論理は中間命題論理と言われる．それらに対する精緻化された分析をLeanによる形式化で行いたい．

素朴なソルバーbotとして動かす

命題論理をベースにしたほとんどの様相論理の体系は決定可能である事実が知られている．そのため直観主義命題論理に対するipc_botのように，ユーザーから論理式などの入力を受け取り，その式の恒真性や妥当性などを判定するbotとして動かしても理論上は計算効率などは無視すれば停止する筈である． Leanは汎用的なプログラミング言語としても設計されているので，そのような用途にも使うことができる（出来てほしい）ので，それを確かめるため実装してみたい．

ここにあるものは細々としており，いくつかは開発に戻る気がないものも列挙されている．

sno2wman.net

Astro

Cloudflare Pages

Svelte

このサイト．

SnO2WMaN/infrastructures

ArgoCD

Kubernetes

Nix

NixOS

自宅で実際に運用しているサーバやk8sクラスタ等の構成ファイル．

deno2nix

Deno

Nix

Denoで書かれたプログラムをNixでうまく取り扱うためのユーティリティ． Nixそのものへの情熱を失っているため，現在は特にメンテナンスはしていない．

corepack.nix

Nix

Node.js

Node.jsのパッケージマネージャ管理ツールであるCorepackをNixでも使うためのユーティリティ．

All your nicovideos in Scrapbox

Deno

TypeScript

Scrapbox内で言及したニコニコ動画の動画を全て取得する．使いやすいようにAPIとして提供．

satyxin

Nix

SATySFi

SATySFiのパッケージ解決などをNixで行うための諸々のユーティリティー． SATySFi及びNixそのものへの情熱を失っているため，現在は特にメンテナンスはしていない．

Incompleteness.txt

Typst

不完全性定理と諸々の話題についてのメモ．書き途中かつ放棄している．